OAI/AlgebraicGeometry/CharacterVarieties/Seams/MarkedSeams.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Internal seams of a marked cut

Original, reflected, and transverse branches retain their framed seam equations when the boundary enumeration is marked.

  1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedOriginalSeams line 34

    Source documentation

    The original internal seams satisfy their framed flag equations for every handle value.

    def MarkedOriginalSeams : Prop :=
…
  2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedOriginal_seamHolds line 42
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedMirrorSeams line 58

    Source documentation

    The reflected internal seams satisfy their framed flag equations for every handle value.

    def MarkedMirrorSeams : Prop :=
…
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedMirror_seamHolds line 66
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedPositiveBranchSeams line 82

    Source documentation

    The positive transverse seams satisfy their framed flag equations for every handle value.

    def MarkedPositiveBranchSeams : Prop :=
…
  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedPositiveBranch_seamHolds line 90
  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedNegativeBranchSeams line 106

    Source documentation

    The negative transverse seams satisfy their framed flag equations for every handle value.

    def MarkedNegativeBranchSeams : Prop :=
…
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedNegativeBranch_seamHolds line 114