MirrorSeams.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorSeamGrade_canonical line 11
Source documentation
Seam grades are independent of boundary enumeration.
```
private lemma mirrorSeamGrade_canonical {F S V : Type} {arity : S → ℕ}
    [Finite S] (D : Diagram F S V arity) (s : S) (i : Fin (D.seamDim s)) :
    D.seamGrade s i=
      (SurfacePresentation.fromPorts D.ports D.rank D.genus D.seamRank).seamGrade s i := rfl
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram, OAI.IntegralCharacterVarieties.SurfacePresentation.fromPorts, OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamGrade
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedMirrorColumns line 31
Source documentation
Column coordinates of the marked short mirror seam.
```
def markedMirrorColumns : ((i : Fin (arity q)) × Fin (D.childDim q i)) ≃
    Fin ((C).seamDim (D.cutShortSeam q w.shape true)) := D.cutMirrorSeamColumns q w
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamDim
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedMirrorRows line 35
Source documentation
Row coordinates of the marked short mirror seam.
```
def markedMirrorRows : Fin (D.rank (D.ports.facet ⟨q,none⟩)) ≃
    Fin ((C).seamDim (D.cutShortSeam q w.shape true)) := D.cutMirrorSeamRows q w
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamDim
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedMirrorGrade line 39
Source documentation
The marked short mirror seam has the original child-index grading.
```
def MarkedMirrorGrade : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedMirror_grade line 44
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedMirrorShortFlags line 51
Source documentation
The short mirror seam satisfies the framed flag equation.
```
def MarkedMirrorShortFlags : Prop :=
…
```
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorLeftWordCoordinates line 62
Source documentation
Coordinates of the complete left word of the short mirror seam.
```
def MirrorLeftWordCoordinates : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorLeft_wordCoordinates line 71
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorRightWordCoordinates line 89
Source documentation
Coordinates of the complete right word of the short mirror seam.
```
def MirrorRightWordCoordinates : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorRight_wordCoordinates line 98
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedMirrorShortFlags_of_wordCoordinates line 116
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedMirrorShort_seamHolds line 151