OAI/AlgebraicGeometry/CharacterVarieties/Foundation/GeneratorGauge.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.MatrixIso.toUnit line 12
2. lemma OAI.IntegralCharacterVarieties.MatrixIso.unit_toUnit line 24
3. lemma OAI.IntegralCharacterVarieties.MatrixIso.toUnit_unit line 26
4. lemma OAI.IntegralCharacterVarieties.MatrixIso.unit_mul line 28
5. lemma OAI.IntegralCharacterVarieties.MatrixIso.unit_inv line 30
6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamColumnsBasis line 41

   Source documentation

   The whole ordered child fiber, retaining every old occurrence.

   def seamColumnsBasis (G : D.CircleBases (R:=R)) (s : S) :
   …

7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamParentBasis line 46
8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.port_columns_basis line 51
9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.port_parent_basis line 65
10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.gaugeGenerators line 77

    Source documentation

    These are the old generator coordinates in new boundary base frames: all side occurrences and BOTH seam ends change together.

    def gaugeGenerators (G : D.CircleBases (R:=R))
    …

11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portFrame_gauge line 86
12. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexHolds_gauge line 102
13. theorem OAI.IntegralCharacterVarieties.MatrixIso.symm_symm_eq line 117
14. theorem OAI.IntegralCharacterVarieties.MatrixIso.trans_symm_eq line 118
15. lemma OAI.IntegralCharacterVarieties.MatrixIso.block_trans line 121
16. lemma OAI.IntegralCharacterVarieties.MatrixIso.block_symm line 127
17. lemma OAI.IntegralCharacterVarieties.MatrixIso.bases_trans line 131
18. lemma OAI.IntegralCharacterVarieties.MatrixIso.unit_block line 137
19. lemma OAI.IntegralCharacterVarieties.MatrixIso.unit_linearEquiv line 144
20. lemma OAI.IntegralCharacterVarieties.MatrixExpression.Term.eval_cast_iso line 155
21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.parentWord_gauge line 173
22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.childInverse_gauge line 184
23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamLeft_gauge line 211
24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamRight_gauge line 219
25. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamColumns_grade line 227
26. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamHolds_gauge line 237

    Source documentation

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

    theorem seamHolds_gauge (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.gaugeGenerators G g)))
          (matrixUnitEquiv ((D.seamRight s).eval φ (D.gaugeGenerators G g))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag