FirstShortSeam.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The first short seam

Port coordinates transport the old negative framed flag to the first short seam of a marked cut.

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.transportFirstFrames_coordinates line 18
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstOldFrameCoordinates line 46
Source documentation
The old negative port frame has the original named seam coordinates.
```
def FirstOldFrameCoordinates : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirst_old_frameCoordinates line 50
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstNewFrameCoordinates line 61
Source documentation
The first new port frame has the coordinates of the identified band.
```
def FirstNewFrameCoordinates : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirst_new_frameCoordinates line 64
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstSeamGrade line 71
Source documentation
The first short seam uses the grade of the original child index.
```
def FirstSeamGrade : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirst_grade line 75
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstLocalFrameFlag line 87
Source documentation
The local frames at the first short seam determine the same graded flag.
```
def FirstLocalFrameFlag : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirst_localFrameFlag line 94
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandValues_first_one line 126
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FirstShortSideValuesTrivial line 157
Source documentation
All side values at the first short seam are the identity.
```
def FirstShortSideValuesTrivial : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_first line 162

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.trivialSides_seamHolds_of_flag line 181

Source documentation

Equality of the framed flags gives the first short seam equation.

lemma trivialSides_seamHolds_of_flag (s : S)
    (hp : g (.side ⟨s,none⟩)=1)
    (hc : ∀ i,g (.side ⟨s,some i⟩)=1)
    (hf : SameFramedFlag (D.seamGrade s)
      (matrixUnitEquiv (g (.frame s false)))
      (matrixUnitEquiv (g (.frame s true)))) :
    SameFramedFlag (D.seamGrade s)
      (matrixUnitEquiv ((D.seamLeft s).eval φ g))
      (matrixUnitEquiv ((D.seamRight s).eval φ g)) := by
…

Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedFirstShortFlag line 228
Source documentation
The first short seam inherits the old negative framed flag for every handle value.
```
def MarkedFirstShortFlag : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedFirstShort_seamHolds line 237