OAI/AlgebraicGeometry/CharacterVarieties/Frames/PositiveCoordinates.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortSeamGrade_canonical line 13

    Source documentation

    Seam grades are independent of boundary enumeration.

    private lemma lastShortSeamGrade_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

  2. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortGeneratorValues line 37
  3. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortOldPort line 46
  4. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortBandPort line 47
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedLastShortColumns line 56

    Source documentation

    Child coordinates for the marked positive short seam.

    def markedLastShortColumns : ((i : Fin (arity q)) × Fin (D.childDim q i)) ≃
    Fin ((C).seamDim (s)) := D.cutLastColumns q w

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamDim

  6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedLastShortRows line 60

    Source documentation

    Parent coordinates for the marked positive short seam.

    def markedLastShortRows : Fin (D.rank (D.ports.facet ⟨q,none⟩)) ≃
    Fin ((C).seamDim (s)) := D.cutLastRows q w

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamDim

  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortColumnsAligned line 64

    Source documentation

    The terminal band port and the old positive port use the same seam columns.

    def LastShortColumnsAligned : Prop :=
…
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortColumns_aligned line 69
  9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortRowsAligned line 81

    Source documentation

    The terminal band port and the old positive port use the same seam rows.

    def LastShortRowsAligned : Prop :=
…
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortRows_aligned line 86
  11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortGrade line 98

    Source documentation

    The positive short seam retains the grades of the original child coordinates.

    def LastShortGrade : Prop :=
…
  12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShort_grade line 102
  13. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortCanonicalNewFrameCoordinates line 109

    Source documentation

    The unmarked endpoint frame has terminal band coordinates.

    def LastShortCanonicalNewFrameCoordinates : Prop :=
…
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortCanonicalNew_frameCoordinates line 113
  15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortNewFrameCoordinates line 129

    Source documentation

    The new endpoint frame has the terminal coordinates of the identified band.

    def LastShortNewFrameCoordinates : Prop :=
…
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortNew_frameCoordinates line 134
  17. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortOldFrameCoordinates line 149

    Source documentation

    The old endpoint frame retains its named child coordinates.

    def LastShortOldFrameCoordinates : Prop :=
…
  18. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortOld_frameCoordinates line 155
  19. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortParentCoordinates line 173

    Source documentation

    The parent transport of the positive short seam is the chosen cut matrix.

    def LastShortParentCoordinates : Prop :=
…
  20. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortParent_coordinates line 178
  21. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortChildCoordinates line 188

    Source documentation

    The ordered child inverse of the positive short seam retains its named coordinates.

    def LastShortChildCoordinates : Prop :=
…
  22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShortChild_coordinates line 194
  23. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedLastShortFlag line 211

    Source documentation

    The positive short seam preserves the framed flag equation of the original seam.

    def MarkedLastShortFlag : Prop :=
…
  24. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortLeftWordCoordinates line 221

    Source documentation

    Coordinates of the positive short seam's complete left word.

    def LastShortLeftWordCoordinates : Prop :=
…
  25. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShort_leftWordCoordinates line 230
  26. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.LastShortRightWordCoordinates line 248

    Source documentation

    Coordinates of the positive short seam's complete right word.

    def LastShortRightWordCoordinates : Prop :=
…
  27. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastShort_rightWordCoordinates line 257
  28. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedLastShortFlag_of_word_coordinates line 274
  29. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedLastShort_seamHolds line 301