OAI/AlgebraicGeometry/CharacterVarieties/Frames/InheritedSeams.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedSeamColumns line 17
  2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedSeamRows line 23
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutInheritedSeamColumnCoordinates line 29

    Source documentation

    Inherited port columns agree with the column coordinates of their cut seam.

    def CutInheritedSeamColumnCoordinates (b : Bool) (hs : s≠q) : Prop :=
…
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedSeamColumns_coordinates line 35
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutInheritedSeamRowCoordinates line 51

    Source documentation

    Inherited port rows agree with the row coordinates of their cut seam.

    def CutInheritedSeamRowCoordinates (b : Bool) (hs : s≠q) : Prop :=
…
  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedSeamRows_coordinates line 57
  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutInheritedSeamGrades line 69

    Source documentation

    Inherited seam columns retain the grades of their original child coordinates.

    def CutInheritedSeamGrades : Prop :=
…
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedSeamColumns_grade line 73
  9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedInheritedSeamFlags line 108

    Source documentation

    A framed flag equation on an uncut seam is retained in the marked cut diagram.

    def MarkedInheritedSeamFlags : Prop :=
…
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedInherited_seamHolds line 117