OAI/AlgebraicGeometry/CharacterVarieties/Foundation/CornerGauge.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sourceCorner line 16

   Source documentation

   The unique outgoing boundary side at the corner containing a germ. This uses the corner involution, not the boundary-circle color.

   def sourceCorner (x : Germ S arity) : Side S arity :=
   …

2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sourceCorner_start line 19
3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sourceCorner_finish line 21
4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sourceCorner_facet line 25
5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sourceCorner_mate line 32
6. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CornerBases line 52

   Source documentation

   A independent basis at each boundary corner.

   abbrev CornerBases := (a : Side S arity) →
   …

7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerBasis line 55
8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerBasis_mate line 61
9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sourceCorner_localMate line 69
10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerVertexBases line 77

    Source documentation

    Every local vertex gets a coherent basis system without any new compatibility hypothesis.

    def cornerVertexBases (G : D.CornerBases (R:=R)) (v : V) :
    …

11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerColumns line 95

    Source documentation

    The endpoint is shared by the whole ordered child list, with its own opposite-oriented boundary corner for each child.

    def cornerColumns (s : S) (b : Bool) : MatrixIso R (Fin (D.seamDim s)) (Fin (D.seamDim s)) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerParent line 99
13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerColumns_port line 103
14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerParent_port line 117
15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerGaugeGenerators line 129

    Source documentation

    Path transport transforms from its start corner to its finish; seam frames transform at the precise endpoint, not per boundary circle.

    def cornerGaugeGenerators
        (g : (e : D.Generator) → (Matrix (Fin (D.generatorRank e)) (Fin (D.generatorRank e)) R)ˣ) :
        (e : D.Generator) → (Matrix (Fin (D.generatorRank e)) (Fin (D.generatorRank e)) R)ˣ
      | .side a => (((D.cornerBasis G (start a)).symm.trans (MatrixIso.unit (g (.side a)))).trans
          (D.cornerBasis G (finish a))).toUnit
      | .frame s b => (((D.cornerColumns G s b).symm.trans (MatrixIso.unit (g (.frame s b)))).trans
          (D.cornerParent G s b)).toUnit
      | .handle f k b => g (.handle f k b)

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso.unit

16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portFrame_cornerGauge line 138
17. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexHolds_cornerGauge line 154
18. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.parentWord_cornerGauge line 172
19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.childInverse_cornerGauge line 183
20. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamLeft_cornerGauge line 211
21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamRight_cornerGauge line 219
22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerColumns_grade line 227
23. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamHolds_cornerGauge line 237

    Source documentation

    Every regular seam equation is preserved, with the full graded identifications and opposite child orientations.

    theorem seamHolds_cornerGauge (s : S)
        (h : SameFramedFlag (D.seamGrade s)
          (matrixUnitEquiv ((D.seamLeft s).eval φ g))
          (matrixUnitEquiv ((D.seamRight s).eval φ g))) :
        SameFramedFlag (D.seamGrade s)
          (matrixUnitEquiv ((D.seamLeft s).eval φ (D.cornerGaugeGenerators G g)))
          (matrixUnitEquiv ((D.seamRight s).eval φ (D.cornerGaugeGenerators G g))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag