refactor(peps): split insertion coefficient realizations

Author: Sirui Lu

TNLean.lean

@@ -382,6 +382,7 @@ import TNLean.PEPS.NormalSquarePEPSBlocking
 import TNLean.PEPS.NormalEdgeBlockingMargins
 import TNLean.PEPS.IdentityInsertion
 import TNLean.PEPS.InsertionRealization
+import TNLean.PEPS.InsertionCoefficientRealization
 import TNLean.PEPS.InsertionAlgebra
 import TNLean.PEPS.LocalGauge
 import TNLean.PEPS.TensorFactorScalar

TNLean/PEPS/InsertionAlgebra.lean

@@ -1,6 +1,6 @@
 import TNLean.PEPS.EdgeMiddlePhysical
 import TNLean.PEPS.IdentityInsertion
-import TNLean.PEPS.InsertionRealization
+import TNLean.PEPS.InsertionCoefficientRealization
 import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.LinearAlgebra.Matrix.Reindex
 
@@ -23,7 +23,7 @@ namespace PEPS
 variable {V : Type*} [Fintype V] [LinearOrder V]
 variable {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ}
 
-/-! ### The state-operator bridge
+/-! ### State and endpoint-operator comparison
 
 The realization sums appearing in `edgeInsertedCoeff_eq_sum_left_physicalRealization`
 and `edgeInsertedCoeff_eq_sum_right_physicalRealization` are rewritten as weighted
@@ -207,8 +207,8 @@ theorem edgeRealizationSum_right_eq_sum_edgeBlockedCoeff (A : Tensor G d) (e : E
           rw [Function.update_of_ne (edgeLeft_ne_edgeRight e)]
 
 /-- Equality of PEPS states transfers the left realization sum between the two tensor
-families. The bridge rewrites both sides as weighted sums of the edge-blocked
-coefficient, and `SameState.edgeBlockedCoeff_eq` matches them termwise.
+families. Both sides are weighted sums of the edge-blocked coefficient, and
+`SameState.edgeBlockedCoeff_eq` matches them termwise.
 
 Source: arXiv:1804.04964, Section 3, lines 1010--1036 of
 `Papers/1804.04964/paper_normal.tex` (the two PEPS represent the same state before
@@ -684,15 +684,15 @@ theorem edgeTransferMatrix_edgeInsertedCoeff (A B : Tensor G d) (e : Edge G)
 
 /-! ### Injectivity of the edge-inserted coefficient and the algebra equivalence
 
-The transfer map carries an algebra structure, but packaging it as an
-`AlgEquiv` requires the inserted coefficient to determine the inserted matrix:
+The transfer map carries an algebra structure. To obtain an algebra
+isomorphism, the inserted coefficient must determine the inserted matrix:
 two matrices giving the same edge-inserted coefficient at every physical
 configuration are equal (`edgeInsertedCoeff_injective`). This is the
 inverse-direction content of the resonate inversion behind
 `physical_to_virtual_insertion`. Together with the coefficient identity it
 supplies `map_one` (`edgeTransferMatrix_one`), the algebra homomorphism
 (`edgeTransferAlgHom`), the two-sided inverse from the symmetric construction
-(`edgeTransferAlgHom_comp_self`), and the packaged equivalence
+(`edgeTransferAlgHom_comp_self`), and the algebra equivalence
 (`edgeTransferAlgEquiv`).
 
 Source: arXiv:1804.04964, Section 3, Lemma inj_isomorph, lines 254--582 of
@@ -947,7 +947,7 @@ Injectivity of the edge-inserted coefficient in the inserted matrix
 (`edgeInsertedCoeff_injective`) supplies identity-preservation
 (`edgeTransferMatrix_one`); the symmetric construction with the two families
 exchanged supplies the two-sided inverse (`edgeTransferAlgHom_comp_self`),
-packaging the transfer map as the algebra equivalence `edgeTransferAlgEquiv`. -/
+giving the algebra equivalence `edgeTransferAlgEquiv`. -/
 theorem isEdgeBlockedInsertionAlgebraIsomorphism
     (A B : Tensor G d) (e : Edge G)
     (hA : EdgeBlockedThreeSiteInjective (G := G) A e)

TNLean/PEPS/InsertionCoefficientRealization.lean

@@ -0,0 +1,200 @@
+import TNLean.PEPS.InsertionRealization
+
+/-!
+# Coefficient realizations for edge virtual insertions
+
+This file records the coefficient-level consequences of endpoint physical
+realization. A physical realization of a virtual matrix insertion at either
+endpoint reproduces the full edge-inserted PEPS coefficient. These formulas are
+the endpoint \(X \mapsto O_1,O_2\) part used in the edge-blocked insertion
+algebra comparison.
+
+Source: arXiv:1804.04964, Section 3, Lemma \(\mathrm{inj\_isomorph}\), lines
+254--582 of `Papers/1804.04964/paper_normal.tex`.
+-/
+
+namespace TNLean
+namespace PEPS
+
+variable {V : Type*} [Fintype V] [LinearOrder V]
+variable {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ}
+
+/-- The left-endpoint physical realization of a virtual matrix insertion
+reproduces the full inserted-edge coefficient.
+
+This is the coefficient-level part of the local \(X \mapsto O_1,O_2\) step in
+Lemma \(\mathrm{inj\_isomorph}\) of arXiv:1804.04964, Section 3, in the
+left-endpoint orientation. Since the ordinary edge boundary supplies the right
+distinguished-edge index, the left endpoint realizes \(M^{\mathsf T}\), so that
+the resulting inserted-edge coefficient has matrix coefficient
+\(M_{\mathrm{left},\mathrm{right}}\). -/
+theorem edgeInsertedCoeff_eq_sum_left_physicalRealization (A : Tensor G d)
+    (e : Edge G) (σ : V → Fin d)
+    (M : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ)
+    (O₁ : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ))
+    (hO₁ : ∀ c : LocalVirtualConfig A e.1.1 → ℂ,
+      O₁ (localTensorMap A e.1.1 c) =
+        localTensorMap A e.1.1
+          (localIncidentMatrixOp A (edgeLeftIncident (G := G) e) M.transpose c)) :
+    edgeInsertedCoeff (G := G) A e σ M =
+      ∑ β : EdgeBoundaryConfig (G := G) A e,
+        O₁ (A.component e.1.1 (edgeLeftLocalConfig (G := G) A e β)) (σ e.1.1) *
+          edgeOpenMiddleWeight (G := G) A e σ β.leftResidual β.rightResidual *
+          A.component e.1.2 (edgeRightLocalConfig (G := G) A e β) (σ e.1.2) := by
+  classical
+  let φ := edgeBoundaryLeftIndexEquivInsertedBoundaryConfig (G := G) A e
+  let F : EdgeInsertedBoundaryConfig (G := G) A e → ℂ := fun β =>
+    A.component e.1.1 (edgeInsertedLeftLocalConfig (G := G) A e β) (σ e.1.1) *
+      M β.leftEdgeIndex β.rightEdgeIndex *
+      edgeOpenMiddleWeight (G := G) A e σ β.leftResidual β.rightResidual *
+      A.component e.1.2 (edgeInsertedRightLocalConfig (G := G) A e β) (σ e.1.2)
+  have hLeft :
+      ∀ β : EdgeBoundaryConfig (G := G) A e,
+        O₁ (A.component e.1.1 (edgeLeftLocalConfig (G := G) A e β)) (σ e.1.1) =
+          ∑ y : Fin (A.bondDim e),
+            M y β.edgeIndex *
+              A.component e.1.1
+                (edgeInsertedLeftLocalConfig (G := G) A e
+                  { leftEdgeIndex := y
+                    rightEdgeIndex := β.edgeIndex
+                    leftResidual := β.leftResidual
+                    rightResidual := β.rightResidual })
+                (σ e.1.1) := by
+    intro β
+    have h := congrFun
+      (hO₁ (Pi.single (edgeLeftLocalConfig (G := G) A e β) (1 : ℂ))) (σ e.1.1)
+    rw [localTensorMap_apply_single] at h
+    have hTensor := congrFun
+      (localTensorMap_localIncidentMatrixOp_single (G := G) A
+        (edgeLeftIncident (G := G) e) M.transpose β.edgeIndex β.leftResidual) (σ e.1.1)
+    simpa [edgeLeftLocalConfig, edgeInsertedLeftLocalConfig, Matrix.transpose_apply]
+      using h.trans hTensor
+  calc
+    edgeInsertedCoeff (G := G) A e σ M = ∑ β : EdgeInsertedBoundaryConfig (G := G) A e,
+        F β := by
+      rfl
+    _ = ∑ x : (Σ β : EdgeBoundaryConfig (G := G) A e, Fin (A.bondDim e)),
+        F (φ x) := by
+      exact (φ.sum_comp F).symm
+    _ = ∑ β : EdgeBoundaryConfig (G := G) A e,
+        ∑ y : Fin (A.bondDim e), F (φ ⟨β, y⟩) := by
+      exact Fintype.sum_sigma' (fun β y => F (φ ⟨β, y⟩))
+    _ = ∑ β : EdgeBoundaryConfig (G := G) A e,
+        O₁ (A.component e.1.1 (edgeLeftLocalConfig (G := G) A e β)) (σ e.1.1) *
+          edgeOpenMiddleWeight (G := G) A e σ β.leftResidual β.rightResidual *
+          A.component e.1.2 (edgeRightLocalConfig (G := G) A e β) (σ e.1.2) := by
+      refine Finset.sum_congr rfl ?_
+      intro β _
+      rw [hLeft β]
+      simp [F, φ, edgeBoundaryLeftIndexEquivInsertedBoundaryConfig, Finset.mul_sum,
+        mul_assoc, mul_left_comm, mul_comm]
+
+/-- The right-endpoint physical realization of a virtual matrix insertion
+reproduces the full inserted-edge coefficient.
+
+This is the coefficient-level part of the local \(X \mapsto O_1,O_2\) step in
+Lemma \(\mathrm{inj\_isomorph}\) of arXiv:1804.04964, Section 3, in the
+right-endpoint orientation. The ordinary edge boundary provides the left
+distinguished-edge index, while the right physical action supplies the
+independent right distinguished-edge index of the inserted-edge coefficient. -/
+theorem edgeInsertedCoeff_eq_sum_right_physicalRealization (A : Tensor G d)
+    (e : Edge G) (σ : V → Fin d)
+    (M : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ)
+    (O₂ : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ))
+    (hO₂ : ∀ c : LocalVirtualConfig A e.1.2 → ℂ,
+      O₂ (localTensorMap A e.1.2 c) =
+        localTensorMap A e.1.2
+          (localIncidentMatrixOp A (edgeRightIncident (G := G) e) M c)) :
+    edgeInsertedCoeff (G := G) A e σ M =
+      ∑ β : EdgeBoundaryConfig (G := G) A e,
+        A.component e.1.1 (edgeLeftLocalConfig (G := G) A e β) (σ e.1.1) *
+          edgeOpenMiddleWeight (G := G) A e σ β.leftResidual β.rightResidual *
+          O₂ (A.component e.1.2 (edgeRightLocalConfig (G := G) A e β)) (σ e.1.2) := by
+  classical
+  let φ := edgeBoundaryRightIndexEquivInsertedBoundaryConfig (G := G) A e
+  let F : EdgeInsertedBoundaryConfig (G := G) A e → ℂ := fun β =>
+    A.component e.1.1 (edgeInsertedLeftLocalConfig (G := G) A e β) (σ e.1.1) *
+      M β.leftEdgeIndex β.rightEdgeIndex *
+      edgeOpenMiddleWeight (G := G) A e σ β.leftResidual β.rightResidual *
+      A.component e.1.2 (edgeInsertedRightLocalConfig (G := G) A e β) (σ e.1.2)
+  have hRight :
+      ∀ β : EdgeBoundaryConfig (G := G) A e,
+        O₂ (A.component e.1.2 (edgeRightLocalConfig (G := G) A e β)) (σ e.1.2) =
+          ∑ y : Fin (A.bondDim e),
+            M β.edgeIndex y *
+              A.component e.1.2
+                (edgeInsertedRightLocalConfig (G := G) A e
+                  { leftEdgeIndex := β.edgeIndex
+                    rightEdgeIndex := y
+                    leftResidual := β.leftResidual
+                    rightResidual := β.rightResidual })
+                (σ e.1.2) := by
+    intro β
+    have h := congrFun
+      (hO₂ (Pi.single (edgeRightLocalConfig (G := G) A e β) (1 : ℂ))) (σ e.1.2)
+    rw [localTensorMap_apply_single] at h
+    have hTensor := congrFun
+      (localTensorMap_localIncidentMatrixOp_single (G := G) A
+        (edgeRightIncident (G := G) e) M β.edgeIndex β.rightResidual) (σ e.1.2)
+    simpa [edgeRightLocalConfig, edgeInsertedRightLocalConfig] using h.trans hTensor
+  calc
+    edgeInsertedCoeff (G := G) A e σ M = ∑ β : EdgeInsertedBoundaryConfig (G := G) A e,
+        F β := by
+      rfl
+    _ = ∑ x : (Σ β : EdgeBoundaryConfig (G := G) A e, Fin (A.bondDim e)),
+        F (φ x) := by
+      exact (φ.sum_comp F).symm
+    _ = ∑ β : EdgeBoundaryConfig (G := G) A e,
+        ∑ y : Fin (A.bondDim e), F (φ ⟨β, y⟩) := by
+      exact Fintype.sum_sigma' (fun β y => F (φ ⟨β, y⟩))
+    _ = ∑ β : EdgeBoundaryConfig (G := G) A e,
+        A.component e.1.1 (edgeLeftLocalConfig (G := G) A e β) (σ e.1.1) *
+          edgeOpenMiddleWeight (G := G) A e σ β.leftResidual β.rightResidual *
+          O₂ (A.component e.1.2 (edgeRightLocalConfig (G := G) A e β)) (σ e.1.2) := by
+      refine Finset.sum_congr rfl ?_
+      intro β _
+      rw [hRight β]
+      simp [F, φ, edgeBoundaryRightIndexEquivInsertedBoundaryConfig, Finset.mul_sum,
+        mul_assoc, mul_left_comm, mul_comm]
+
+/-- Vertex injectivity realizes an inserted edge matrix by physical operators at
+the two endpoint tensors.
+
+For an inserted matrix \(M\), the left endpoint realizes \(M^{\mathsf T}\) and
+the right endpoint realizes \(M\). Both physical realizations give the same
+inserted-edge coefficient after the edge-centered three-site decomposition. -/
+theorem edgeInsertedCoeff_endpointPhysicalRealization (A : Tensor G d)
+    (hA : IsVertexInjective A) (e : Edge G) (σ : V → Fin d)
+    (M : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ) :
+    (∃ O₁ : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ),
+      (∀ c : LocalVirtualConfig A e.1.1 → ℂ,
+        O₁ (localTensorMap A e.1.1 c) =
+          localTensorMap A e.1.1
+            (localIncidentMatrixOp A (edgeLeftIncident (G := G) e) M.transpose c)) ∧
+      edgeInsertedCoeff (G := G) A e σ M =
+        ∑ β : EdgeBoundaryConfig (G := G) A e,
+          O₁ (A.component e.1.1 (edgeLeftLocalConfig (G := G) A e β)) (σ e.1.1) *
+            edgeOpenMiddleWeight (G := G) A e σ β.leftResidual β.rightResidual *
+            A.component e.1.2 (edgeRightLocalConfig (G := G) A e β) (σ e.1.2)) ∧
+    (∃ O₂ : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ),
+      (∀ c : LocalVirtualConfig A e.1.2 → ℂ,
+        O₂ (localTensorMap A e.1.2 c) =
+          localTensorMap A e.1.2
+            (localIncidentMatrixOp A (edgeRightIncident (G := G) e) M c)) ∧
+      edgeInsertedCoeff (G := G) A e σ M =
+        ∑ β : EdgeBoundaryConfig (G := G) A e,
+          A.component e.1.1 (edgeLeftLocalConfig (G := G) A e β) (σ e.1.1) *
+            edgeOpenMiddleWeight (G := G) A e σ β.leftResidual β.rightResidual *
+            O₂ (A.component e.1.2 (edgeRightLocalConfig (G := G) A e β)) (σ e.1.2)) := by
+  constructor
+  · obtain ⟨O₁, hO₁⟩ := localIncidentMatrixOp_physicalRealization
+      (A := A) hA (edgeLeftIncident (G := G) e) M.transpose
+    exact ⟨O₁, hO₁, edgeInsertedCoeff_eq_sum_left_physicalRealization
+      (G := G) A e σ M O₁ hO₁⟩
+  · obtain ⟨O₂, hO₂⟩ := localIncidentMatrixOp_physicalRealization
+      (A := A) hA (edgeRightIncident (G := G) e) M
+    exact ⟨O₂, hO₂, edgeInsertedCoeff_eq_sum_right_physicalRealization
+      (G := G) A e σ M O₂ hO₂⟩
+
+end PEPS
+end TNLean