OAI/AlgebraicGeometry/CharacterVarieties/Frames/MirrorSeamCoordinates.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutMirrorLastOutputAttached line 24

    Source documentation

    The final mirror output belongs to the final end of the short mirror seam.

    def CutMirrorLastOutputAttached : Prop :=
…
  2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorLastOutput_attach line 30
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorSeamColumns line 34
  4. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorSeamRows line 40
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutMirrorSeamColumnsCoordinates line 51

    Source documentation

    Mirror column coordinates agree with the short-seam enumeration.

    def CutMirrorSeamColumnsCoordinates : Prop :=
…
  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorSeamColumns_coordinates line 61
  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutMirrorSeamRowsCoordinates line 74

    Source documentation

    Mirror row coordinates agree with the short-seam enumeration.

    def CutMirrorSeamRowsCoordinates : Prop :=
…
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorSeamRows_coordinates line 82
  9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutMirrorSeamGrade line 91

    Source documentation

    The short mirror seam grading is the original child index.

    def CutMirrorSeamGrade : Prop :=
…
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorSeamColumns_grade line 95
  11. lemma OAI.IntegralCharacterVarieties.MatrixIso.blockUnitOne_linear line 107
  12. lemma OAI.IntegralCharacterVarieties.MatrixIso.cutInnerUnit_linear line 122
  13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorParentWord_coordinates line 136

    Source documentation

    Parent coordinates for values induced by ports and side transports.

    private lemma mirrorParentWord_coordinates
    {F S V R K : Type} {arity : S → ℕ} [CommRing R] [Field K]
    (D : Diagram F S V arity) (s : S) (φ : R →+* K)
    (frames : D.PortFrames (R:=K)) (side : D.SideValues (R:=K))
…

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram

  14. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorInnerTransport line 168
  15. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorShortGeneratorValues line 175
  16. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorFirstFrameCoordinates line 184

    Source documentation

    The initial mirror frame has the first coordinates of the identified band.

    def MirrorFirstFrameCoordinates : Prop :=
…
  17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorFirst_frameCoordinates line 189
  18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorLastFrameCoordinates line 218

    Source documentation

    The terminal mirror frame has the last coordinates of the identified band.

    def MirrorLastFrameCoordinates : Prop :=
…
  19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorLast_frameCoordinates line 223
  20. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorParentCoordinates line 252

    Source documentation

    The mirror parent word has the coordinates of the conjugated cut transport.

    def MirrorParentCoordinates : Prop :=
…
  21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorParent_coordinates line 258
  22. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorChildCoordinates line 270

    Source documentation

    The inverse child word of the mirror short seam acts as the identity.

    def MirrorChildCoordinates : Prop :=
…
  23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorChild_coordinates line 277