OAI/AlgebraicGeometry/CharacterVarieties/Foundation/SurfaceSurgery.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.SurfaceSurgery.comm line 12
2. def OAI.IntegralCharacterVarieties.SurfaceSurgery.handleProduct line 14
3. def OAI.IntegralCharacterVarieties.SurfaceSurgery.surfaceProduct line 16
4. def OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugate line 18
5. def OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateHandles line 20
6. def OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateBoundaries line 23
7. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.handleProduct_nil line 25
8. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.handleProduct_cons line 26
9. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.handleProduct_append line 28
10. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugate_one line 32
11. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugate_mul line 33
12. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugate_inv line 35
13. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugate_comm line 37
14. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.handleProduct_conjugate line 41
15. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.boundaryProduct_conjugate line 47
16. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.split_boundary_word line 55

    Source documentation

    Cutting the boundary at the two band feet results in two positive boundary words. The t and inverse t are adjacent band transports.

    theorem split_boundary_word (H : List (G × G)) (C D : List G) (a b t : G) :
        surfaceProduct H (C++[a*t,t⁻¹*b]++D)=surfaceProduct H (C++[a*b]++D) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.surfaceProduct

17. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.join_same_boundary_word line 61

    Source documentation

    Joining two boundary circles of the same facet creates THIS additional handle. A provisional unchanged-genus declaration would be incorrect.

    theorem join_same_boundary_word (H : List (G × G)) (C : List G) (a b t : G) :
        surfaceProduct (conjugateHandles t H++[(t,a)])
          ((a*t*b*t⁻¹)::conjugateBoundaries t C)=
          conjugate t (surfaceProduct H (a::b::C)) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.surfaceProduct, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateHandles, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateBoundaries, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugate

18. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.join_same_relation line 72

    Source documentation

    If the old puncture word is central, no new puncture is introduced.

    theorem join_same_relation (H : List (G × G)) (C : List G) (a b t z : G)
        (hold : surfaceProduct H (a::b::C)=z) (hz : Commute t z) :
        surfaceProduct (conjugateHandles t H++[(t,a)])
          ((a*t*b*t⁻¹)::conjugateBoundaries t C)=z := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.surfaceProduct, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateHandles, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateBoundaries

19. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.join_distinct_boundary_word line 82

    Source documentation

    Attachment between different components: choose the first joining circle last on its facet and the second joining circle first on its facet. Old handles on the second facet are transported along an explicit based path.

    theorem join_distinct_boundary_word (H J : List (G × G)) (C D : List G) (a b t : G) :
        surfaceProduct (H++conjugateHandles (C.prod*a*t) J)
          (C++[a*t*b*t⁻¹]++conjugateBoundaries t D)=
          surfaceProduct H (C++[a]) * conjugate t (surfaceProduct J (b::D)) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.surfaceProduct, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateHandles, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateBoundaries, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugate

20. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.join_distinct_relation line 93

    Source documentation

    Full scalar puncture products of the two old facets multiply. In application these z's are products of scalar units extracted from Diagram.Solution.

    theorem join_distinct_relation (H J : List (G × G)) (C D : List G) (a b t z w : G)
        (hH : surfaceProduct H (C++[a])=z) (hJ : surfaceProduct J (b::D)=w)
        (hw : Commute t w) :
        surfaceProduct (H++conjugateHandles (C.prod*a*t) J)
          (C++[a*t*b*t⁻¹]++conjugateBoundaries t D)=z*w := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.surfaceProduct, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateHandles, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateBoundaries

21. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.interchange_boundary_word line 102
22. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.join_same_topology line 107

    Source documentation

    Exact genus and boundary counts of the self-attachment.

    theorem join_same_topology (H : List (G × G)) (C : List G) (a b t : G) :
        (conjugateHandles t H++[(t,a)]).length=H.length+1 ∧
        ((a*t*b*t⁻¹)::conjugateBoundaries t C).length+1=(a::b::C).length := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateHandles, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateBoundaries

23. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.join_distinct_topology line 113

    Source documentation

    Exact genus and boundary counts for attaching different facets.

    theorem join_distinct_topology (H J : List (G × G)) (C D : List G) (a b t : G) :
        (H++conjugateHandles (C.prod*a*t) J).length=H.length+J.length ∧
        (C++[a*t*b*t⁻¹]++conjugateBoundaries t D).length+1=
          (C++[a]).length+(b::D).length := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateHandles, OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateBoundaries

24. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.join_handles_natural line 122

    Source documentation

    All formulas use the same full-ring units under base change. Nothing in these word maps inverts a determinant outside the original general linear group.

    theorem join_handles_natural {G' : Type*} [Group G'] (φ : G →* G')
        (H : List (G × G)) (t : G) :
        (conjugateHandles t H).map (fun p => (φ p.1,φ p.2))=
          conjugateHandles (φ t) (H.map (fun p => (φ p.1,φ p.2))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.conjugateHandles

25. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.evaluatedHandles line 136
26. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.evaluatedBoundaries line 140
27. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_word_relation line 145

    Source documentation

    All old handle and boundary transports, extracted from the full original solution, satisfy precisely the relation used by the surface surgery formulas.

    theorem actual_word_relation (f : F) :
        surfaceProduct (D.evaluatedHandles P g f) (D.evaluatedBoundaries P g f)=
          scalarUnit (D.rank f) (D.diskScalar P f) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit

28. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit_mul line 154
29. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit_commute line 157
30. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_split_boundary line 165

    Source documentation

    Splitting a circle of an old full solution preserves its prescribed puncture product with the two explicitly constructed band transports.

    theorem actual_split_boundary (f : F)
        (C E : List (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ)
        (a b t : (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ)
        (hB : D.evaluatedBoundaries P g f=C++[a*b]++E) :
        surfaceProduct (D.evaluatedHandles P g f) (C++[a*t,t⁻¹*b]++E)=
          scalarUnit (D.rank f) (D.diskScalar P f) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit

31. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_join_same line 175

    Source documentation

    The handle appearing when TWO old boundary circles are joined is produced from g and t.

    theorem actual_join_same (f : F)
        (C : List (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ)
        (a b t : (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ)
        (hB : D.evaluatedBoundaries P g f=a::b::C) :
        surfaceProduct (conjugateHandles t (D.evaluatedHandles P g f)++[(t,a)])
          ((a*t*b*t⁻¹)::conjugateBoundaries t C)=
          scalarUnit (D.rank f) (D.diskScalar P f) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit

32. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit line 188

    Source documentation

    Equal-rank fibers may be based on different original facets.

    def rebaseUnit {m n : ℕ} (h : m=n) :
        (Matrix (Fin m) (Fin m) A)ˣ ≃* (Matrix (Fin n) (Fin n) A)ˣ := by
    …

33. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit_scalar line 193
34. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_join_distinct line 199

    Source documentation

    Direct two-facet attachment uses all handles of both old facets and the product of their COMPLETE prescribed puncture scalars. This works in the original base ring A, in particular a full integer ring.

    theorem actual_join_distinct (f k : F) (h : D.rank k=D.rank f)
        (C E : List (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ)
        (a b t : (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ)
        (hF : D.evaluatedBoundaries P g f=C++[a])
        (hK : (D.evaluatedBoundaries P g k).map (rebaseUnit h)=b::E) :
        surfaceProduct (D.evaluatedHandles P g f++conjugateHandles (C.prod*a*t)
            ((D.evaluatedHandles P g k).map (fun p => (rebaseUnit h p.1,rebaseUnit h p.2))))
          (C++[a*t*b*t⁻¹]++conjugateBoundaries t E)=
          scalarUnit (D.rank f) (D.diskScalar P f * D.diskScalar P k) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit, OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit