feat(peps): per-edge gauge family from the insertion isomorphism (toward gaugeConsistency) #2403
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,140 @@ | ||
| import TNLean.PEPS.Blocking | ||
| import TNLean.PEPS.InsertionAlgebra | ||
| import TNLean.PEPS.EdgeGaugeExtraction | ||
| import TNLean.PEPS.EdgeMiddlePhysical | ||
| import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs | ||
|
|
||
| /-! | ||
| # Per-edge gauge family for injective PEPS | ||
|
|
||
| This file records the per-edge content of the injective PEPS Fundamental | ||
| Theorem (arXiv:1804.04964, Section 3) into one global gauge family. | ||
|
|
||
| For each edge `e`, blocking a vertex-injective PEPS around `e` gives a three-site | ||
| injective chain. Comparing two PEPS that generate the same state then yields, via | ||
| `isEdgeBlockedInsertionAlgebraIsomorphism` (#1367), an algebra isomorphism `Φ_e` | ||
| between the two bond matrix algebras whose inserted edge coefficients agree. | ||
| Skolem--Noether (`edgeGaugeFromInsertionAlgebraIsomorphism`) realizes each `Φ_e` | ||
| as conjugation by an invertible bond matrix. Transporting these matrices back to | ||
| the first tensor's bonds across the bond-dimension equality gives a single | ||
| gauge family `X` and records, edgewise, both the inserted-coefficient identity | ||
| and the conjugation form of `Φ_e`. | ||
|
|
||
| This is the construction used in the gauge-consistency theorem; the remaining | ||
| cross-edge passage to the per-vertex gauge formula is recorded in | ||
| the fundamental-theorem module and in | ||
| `docs/paper-gaps/peps_injective_ft_section3_route.tex`. | ||
| -/ | ||
|
|
||
| open scoped BigOperators Matrix | ||
|
|
||
| namespace TNLean | ||
| namespace PEPS | ||
|
|
||
| variable {V : Type*} [Fintype V] [LinearOrder V] | ||
| variable {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} | ||
|
|
||
| /-- Transport an invertible matrix across an equality of finite index sizes. -/ | ||
| noncomputable def glReindex {m n : ℕ} (h : m = n) : | ||
| GL (Fin m) ℂ ≃* GL (Fin n) ℂ := | ||
| Units.mapEquiv (Matrix.reindexAlgEquiv ℂ ℂ (finCongr h)).toRingEquiv.toMulEquiv | ||
|
|
||
| /-- The matrix of a transported invertible matrix is the reindexed matrix. -/ | ||
| theorem glReindex_coe {m n : ℕ} (h : m = n) (Z : GL (Fin m) ℂ) : | ||
| (↑(glReindex h Z) : Matrix (Fin n) (Fin n) ℂ) = | ||
| Matrix.reindexAlgEquiv ℂ ℂ (finCongr h) (↑Z : Matrix (Fin m) (Fin m) ℂ) := | ||
| rfl | ||
|
|
||
| /-- Reindexing back and forth across an index-size equality is the identity. -/ | ||
| theorem reindexAlgEquiv_finCongr_symm_round {m n : ℕ} (h h' : m = n) | ||
|
Check warning on line 49 in TNLean/PEPS/EdgeGaugeFamily.lean
|
||
| (N : Matrix (Fin n) (Fin n) ℂ) : | ||
| Matrix.reindexAlgEquiv ℂ ℂ (finCongr h) | ||
| (Matrix.reindexAlgEquiv ℂ ℂ (finCongr h'.symm) N) = N := by | ||
|
There was a problem hiding this comment. ℹ️ Advisory (modularity). |
||
| subst h | ||
| simp | ||
|
|
||
| /-- **Per-edge gauge family from the edge-blocked insertion algebra | ||
| isomorphisms.** | ||
|
|
||
| For each edge `e`, blocking `A` and `B` around `e` gives three-site injective | ||
| chains (`IsVertexInjective.edgeBlockedThreeSiteInjective`, using the positive | ||
| bond dimensions), and `isEdgeBlockedInsertionAlgebraIsomorphism` (#1367) supplies | ||
| an algebra isomorphism `Φ_e` between the bond matrix algebras whose inserted | ||
| coefficients match. The finite-dimensional algebra step | ||
| `edgeGaugeFromInsertionAlgebraIsomorphism` (Skolem--Noether) realizes each `Φ_e` | ||
| as conjugation by an invertible bond matrix on the `B`-side. Transporting those | ||
| matrices back to the \(A\)-side bonds across the bond-dimension equality gives | ||
| a single global gauge family, and records, edgewise, both the inserted-coefficient identity and | ||
| that `Φ_e` is conjugation by `X_e`. | ||
|
|
||
| This records the per-edge content of the source proof up to the point where the | ||
| edge gauges are produced. The remaining work in gauge consistency is the | ||
| cross-edge passage to the per-vertex formula \(B_v = X\cdot A_v\), which | ||
| the source obtains from the post-absorption insertion identity | ||
| (`eq:inj_equal_edge`) and the one-vertex-versus-complement comparison; both of | ||
| those steps are tracked separately (see | ||
| `docs/paper-gaps/peps_injective_ft_section3_route.tex`). | ||
|
|
||
| Source: arXiv:1804.04964, Section 3, lines 560--586. -/ | ||
| theorem exists_edgeGaugeFamily (A B : Tensor G d) | ||
| (hA : IsVertexInjective A) (hB : IsVertexInjective B) | ||
| (hAB : SameState A B) | ||
| (hDim : A.bondDim = B.bondDim) | ||
| (hpos : ∀ e : Edge G, 0 < A.bondDim e) : | ||
|
claude[bot] marked this conversation as resolved.
|
||
| ∃ X : (e : Edge G) → GL (Fin (A.bondDim e)) ℂ, | ||
| ∀ e : Edge G, | ||
| ∃ Φ : | ||
| Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ ≃ₐ[ℂ] | ||
| Matrix (Fin (B.bondDim e)) (Fin (B.bondDim e)) ℂ, | ||
| (∀ (σ : V → Fin d) | ||
| (M : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ), | ||
| edgeInsertedCoeff (G := G) A e σ M = | ||
| edgeInsertedCoeff (G := G) B e σ (Φ M)) ∧ | ||
| ∀ M : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ, | ||
| Φ M = | ||
| Matrix.reindexAlgEquiv ℂ ℂ (finCongr (congr_fun hDim e)) | ||
| ((↑(X e) : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ) * M * | ||
| (↑(X e)⁻¹ : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ)) := by | ||
| classical | ||
| have hposB : ∀ e : Edge G, 0 < B.bondDim e := by | ||
| intro e; rw [← congr_fun hDim e]; exact hpos e | ||
| have hAblk : ∀ e : Edge G, EdgeBlockedThreeSiteInjective (G := G) A e := | ||
| fun e => hA.edgeBlockedThreeSiteInjective hpos e | ||
| have hBblk : ∀ e : Edge G, EdgeBlockedThreeSiteInjective (G := G) B e := | ||
| fun e => hB.edgeBlockedThreeSiteInjective hposB e | ||
| have hiso : ∀ e : Edge G, IsEdgeBlockedInsertionAlgebraIsomorphism (G := G) A B e := | ||
| fun e => | ||
| isEdgeBlockedInsertionAlgebraIsomorphism A B e (hAblk e) (hBblk e) hAB hpos hposB | ||
| choose Φ hΦcoeff using fun e => (hiso e) | ||
| -- Skolem--Noether: each edge algebra equivalence is conjugation by an | ||
| -- invertible matrix on the second tensor's bond. | ||
| choose hEdge Z hZ using | ||
| fun e => edgeGaugeFromInsertionAlgebraIsomorphism A B e (Φ e) | ||
| -- Transport each edge gauge back to the first tensor's bond. | ||
| refine ⟨fun e => glReindex (hEdge e).symm (Z e), fun e => ⟨Φ e, hΦcoeff e, ?_⟩⟩ | ||
| intro M | ||
| rw [hZ e] | ||
| -- Both sides reindex the inserted matrix from the first bond to the second | ||
| -- bond, conjugated by the edge gauge. | ||
| have hXcoe : | ||
| (↑(glReindex (hEdge e).symm (Z e)) : | ||
| Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ) = | ||
| Matrix.reindexAlgEquiv ℂ ℂ (finCongr (hEdge e).symm) | ||
| (↑(Z e) : Matrix (Fin (B.bondDim e)) (Fin (B.bondDim e)) ℂ) := | ||
| glReindex_coe (hEdge e).symm (Z e) | ||
| have hXinvcoe : | ||
| (↑(glReindex (hEdge e).symm (Z e))⁻¹ : | ||
| Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ) = | ||
| Matrix.reindexAlgEquiv ℂ ℂ (finCongr (hEdge e).symm) | ||
| (↑(Z e)⁻¹ : Matrix (Fin (B.bondDim e)) (Fin (B.bondDim e)) ℂ) := by | ||
| rw [← map_inv, glReindex_coe] | ||
| rw [hXcoe, hXinvcoe] | ||
| have hProofEq : congr_fun hDim e = hEdge e := Subsingleton.elim _ _ | ||
| rw [hProofEq] | ||
| -- The reindexing equivalence is multiplicative; push it through products, and | ||
| -- the inverse-index transport cancels against the outer reindex. | ||
| simp only [map_mul, | ||
|
claude[bot] marked this conversation as resolved.
|
||
| reindexAlgEquiv_finCongr_symm_round (hEdge e) (hEdge e)] | ||
|
|
||
| end PEPS | ||
| end TNLean | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
B §1 — "fundamental-theorem module" is organizational/implementation language.
Line 25 of the module docstring reads:
"Module" here refers to the Lean source file
TNLean/PEPS/FundamentalTheorem.lean— an organizational unit of the Lean build system, not a mathematical object. Per §1 ofdocs/prose_style.md, implementation language ("module", "file", Lean namespace paths) should not appear in docstrings; the mathematical content should be named instead.Suggested replacement (one possibility):
("the proof of the fundamental theorem" names the mathematical content without naming the Lean module.)