OAI/AlgebraicGeometry/CharacterVarieties/Foundation/BoundaryNormalization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The explicit inverse prefix product at every boundary corner.

   def normalizingBoundaryBases : D.BoundaryBases (A:=A) := fun f b i =>
   …

2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalizingCorners line 19
3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalizingCorners_based line 22
4. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalizeBoundaryGenerators line 31

   Source documentation

   This changes all side and frame coordinates, so it respects every named quotient at every vertex, not just a list of boundary conjugacy classes.

   def normalizeBoundaryGenerators := D.cornerGaugeGenerators (D.normalizingCorners φ g) g

5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalized_boundaryEdge line 33
6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalizeBoundarySolution line 47

   Source documentation

   A full solution in canonical boundary path coordinates. It is constructed from any old solution, uniformly over the full coefficient ring.

   def normalizeBoundarySolution (P : D.Punctures R) (x : D.Solution P A) : D.Solution P A :=
   …

7. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalizeBoundary_reconstruct line 52

   Source documentation

   Exact forward coverage in the original full solution variety.

   theorem normalizeBoundary_reconstruct (P : D.Punctures R) (x : D.Solution P A) :
       D.basedCornerSolution (fun a => (D.normalizingCorners (algebraMap R A) x.val.val a).symm)
         (D.basedCorner_inverse _ (D.normalizingCorners_based (algebraMap R A) x.val.val)) P
         (D.normalizeBoundarySolution P x)=x := by
   …

8. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalizeBoundarySolution_edge line 60
9. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixBasis_unique line 71

   Source documentation

   The based normalization matrices are FORCED by the edge maps. There is no extra monodromy equation hidden in the last interval.

   lemma prefixBasis_unique {n : ℕ} (hn : 0<n) (e C : Fin n → G)
       (h0 : C ⟨0,hn⟩=1)
       (hC : ∀ i : Fin n,i.val+1<n →
         C ⟨(i.val+1)%n,Nat.mod_lt _ hn⟩*e i*(C i)⁻¹=1) :
       C=prefixBasis e := by
   …

   Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixBasis

10. lemma OAI.IntegralCharacterVarieties.MatrixIso.reindex_injective line 99
11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryCornerBasis_injective line 117
12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.IsBoundaryNormalized line 125
13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalize_isBoundaryNormalized line 130
14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.normalizingCorners_unique line 136
15. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NormalizedSolution line 156

    Source documentation

    The canonical locus is a subtype of the full solution, retaining all old equations, all ordered vertices and all quotient identifications.

    abbrev NormalizedSolution (P : D.Punctures R) (A : Type) [CommRing A] [Algebra R A] :=
    …

16. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.BasedCorners line 158
17. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryChart line 163

    Source documentation

    Unique normalized full solution plus all independent based corner matrices. This is one global path-coordinate chart, not the missing cutting map.

    def boundaryChart (P : D.Punctures R) :
        D.Solution P A ≃ D.NormalizedSolution P A × D.BasedCorners A where
    …