SeamCoordinates.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues_coordinates line 15

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.common_portColumnIndex line 38

Source documentation

Matching local coordinates agree as seam matrix coordinates.

lemma common_portColumnIndex
    (p u : LocalPort V D.ports.kind) (s : S) (b c : Bool)
    (hp : D.ports.attach p=(s,b)) (hu : D.ports.attach u=(s,c))
    (h : (D.ports.attach p).1=(D.ports.attach u).1)
    (e : α ≃ (D.vertexRanks p.1).Columns p.2)
    (eu : α ≃ (D.vertexRanks u.1).Columns u.2)
    (hm : e.trans (D.portColumnMatch p u h)=eu) :
    (eu.trans (D.portColumnIndex u)).trans
      (finCongr (congrArg D.seamDim (congrArg Prod.fst hu)))=
    (e.trans (D.portColumnIndex p)).trans
      (finCongr (congrArg D.seamDim (congrArg Prod.fst hp))) := by
…

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.common_portRowIndex line 55

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.port_coordinates_blockIndex line 73

Source documentation

Child and within-child coordinate identities determine the ordered block-index equivalence.

lemma port_coordinates_blockIndex {m : ℕ} (d : Fin m → ℕ)
    (p : LocalPort V D.ports.kind) (s : S) (b : Bool)
    (hp : D.ports.attach p=(s,b))
    (c : Fin m ≃ Fin (arity s))
    (hc : ∀ i,d i=D.childDim s (c i))
    (e : ((i : Fin m) × Fin (d i)) ≃ (D.vertexRanks p.1).Columns p.2)
    (hi : ∀ i,((D.ports.kind p.1).childEnumeration p.2 (e i).1).val=(c i.1).val)
    (hj : ∀ i,(e i).2.val=i.2.val) :
    (e.trans (D.portColumnIndex p)).trans
      (finCongr (congrArg D.seamDim (congrArg Prod.fst hp)))=
      (Equiv.sigmaCongr c (fun i=>finCongr (hc i))).trans
        (blockIndex (D.childDim s)).symm := by
…

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamGrade_common line 98
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastOldPort line 125
Source documentation
The old positive port in the refined cut diagram.
```
def cutLastOldPort :
    LocalPort (V ⊕ (Fin (w.shape.atomicBand.length+1) ⊕ Fin (w.shape.atomicBand.length+1)))
      (C).ports.kind :=
…
```
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastColumns line 132
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastRows line 135
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastColumns_block line 139
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastRows_finCongr line 164
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutLastColumns_grade line 172