OAI/AlgebraicGeometry/CharacterVarieties/Foundation/GaugeEquivalences.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntegralCharacterVarieties.MatrixIso.bases_symm_cancel line 12
2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideBasis_symm line 26
3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamParentBasis_symm line 28
4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamColumnsBasis_symm line 30
5. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.gaugeGenerators_inverse line 35

   Source documentation

   The coordinate gauge has a two-sided inverse on all old named side, frame and handle coordinates. Seams/vertices are never forgotten.

   theorem gaugeGenerators_inverse :
       D.gaugeGenerators (fun B => (G B).symm) (D.gaugeGenerators G g)=g := by
   …

6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.gaugeEquiv line 54

   Source documentation

   A generator-coordinate equivalence, meaningful over the full ring.

   def gaugeEquiv : ((e : D.Generator) →
         (Matrix (Fin (D.generatorRank e)) (Fin (D.generatorRank e)) A)ˣ) ≃
       ((e : D.Generator) → (Matrix (Fin (D.generatorRank e)) (Fin (D.generatorRank e)) A)ˣ) where
   …

7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerBasis_symm line 70
8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerParent_symm line 72
9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerColumns_symm line 74
10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerGaugeGenerators_inverse line 77
11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.basedCorner_inverse line 96
12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.basedCornerEquiv line 106

    Source documentation

    Full-ring bijective change of every corner frame in the solution. No vertex, quotient identification or surface equation is lost.

    def basedCornerEquiv (hG : CornerBases.Based D G) (P : D.Punctures R) :
        D.Solution P A ≃ D.Solution P A where
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CornerBases.Based