OAI/AlgebraicGeometry/CharacterVarieties/Frames/MirrorCoordinates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.transportFrames_coordinateComposition line 11
  2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorActualColumns line 37
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorActualRows line 40
  4. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutMirrorFrameCoordinates line 46

    Source documentation

    Equality of the transported and aligned mirror frames in the original port coordinates.

    def CutMirrorFrameCoordinates [Fintype I] (old : D.PortFrames (R:=K))
…
  5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirror_frameCoordinates line 53
  6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorColumnCoordinates line 69

    Source documentation

    The child label and the coordinate within that child at a mirror port.

    def cutMirrorColumnCoordinates (i : I) : ℕ × ℕ :=
…
  7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorActualColumns_childEnumeration line 75
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutMirrorActualColumns_value line 82
  9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.shortSignatureMatch line 98
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.shortPlusSignature line 102
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.shortMinusSignature line 109
  12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutShortSeam line 119
  13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutShortSeam_arity line 120
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutShortSideRank line 130
  15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.shortSeamSideValues line 141

    Source documentation

    The side value of a short seam, in the coordinate labels of the original seam.

    def shortSeamSideValues (b : Bool) (i : Option (Fin (arity q))) :
    (Matrix (Fin (D.rank (D.ports.facet ⟨q,i⟩)))
      (Fin (D.rank (D.ports.facet ⟨q,i⟩))) R)ˣ :=
…
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_short line 148
  17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_mirror_parent line 155
  18. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_mirror_child line 159
  19. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.columnsAt line 173
  20. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rowsAt line 175