OAI/AlgebraicGeometry/CharacterVarieties/Foundation/BoundaryBands.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch line 15

   Source documentation

   Joining incoming germs is postcomposition of the old successor with the transposition of its two new targets. This does not identify facet labels.

   def incomingSwitch (σ : Equiv.Perm α) (x y : α) : Equiv.Perm α :=
   …

2. theorem OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch_invol line 18
3. theorem OAI.IntegralCharacterVarieties.BoundaryBand.formPerm_append line 22
4. theorem OAI.IntegralCharacterVarieties.BoundaryBand.formPerm_append_rotate line 40
5. theorem OAI.IntegralCharacterVarieties.BoundaryBand.join_cycles line 48

   Source documentation

   Exact new permutation, with an arbitrary untouched successor factor.

   theorem join_cycles (x y : α) (L M : List α) (ρ : Equiv.Perm α)
       (h : ((x::L)++(y::M)).Nodup) :
       incomingSwitch ((x::L).formPerm*(y::M).formPerm*ρ) x y=
         (((x::L)++(y::M)).formPerm)*ρ := by
   …

   Mentions: OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch

6. theorem OAI.IntegralCharacterVarieties.BoundaryBand.split_cycle line 57

   Source documentation

   The inverse operation splits one old boundary circle into precisely the specified two circles; this is not merely a change in the numerical count.

   theorem split_cycle (x y : α) (L M : List α) (ρ : Equiv.Perm α)
       (h : ((x::L)++(y::M)).Nodup) :
       incomingSwitch ((((x::L)++(y::M)).formPerm)*ρ) x y=
         (x::L).formPerm*(y::M).formPerm*ρ := by
   …

   Mentions: OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch

7. theorem OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch_exact line 65

   Source documentation

   The band changes exactly the two indicated incoming germs and nothing else. Repeated incidences of a facet remain separate α values.

   theorem incomingSwitch_exact (σ : Equiv.Perm α) (x y z : α) :
       incomingSwitch σ x y z=
         if σ z=x then y else if σ z=y then x else σ z := by
   …

   Mentions: OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch

8. def OAI.IntegralCharacterVarieties.BoundaryBand.word line 74

   Source documentation

   Same right-to-left convention as Diagram.boundaryWord.

   def word (h : α → G) (L : List α) : G := (L.map h).reverse.prod
   …

9. theorem OAI.IntegralCharacterVarieties.BoundaryBand.word_nil line 77
10. theorem OAI.IntegralCharacterVarieties.BoundaryBand.word_cons line 79
11. theorem OAI.IntegralCharacterVarieties.BoundaryBand.word_append line 82
12. def OAI.IntegralCharacterVarieties.BoundaryBand.joinEdges line 87

    Source documentation

    The same band transports change only its two first departing edges; all old side occurrences elsewhere retain their precise old matrix.

    def joinEdges (h : α → G) (x y : α) (t : G) (z : α) : G :=
    …

13. theorem OAI.IntegralCharacterVarieties.BoundaryBand.word_eq_of_agree line 91
14. theorem OAI.IntegralCharacterVarieties.BoundaryBand.joinEdges_left line 97
15. theorem OAI.IntegralCharacterVarieties.BoundaryBand.joinEdges_right line 113
16. theorem OAI.IntegralCharacterVarieties.BoundaryBand.joined_word line 132

    Source documentation

    In the joined positive cyclic word, the two edge changes give exactLY the band word used by SurfaceSurgery, not an unproved holonomy input.

    theorem joined_word (h : α → G) (x y : α) (t : G) (L M : List α)
        (hn : ((x::L)++(y::M)).Nodup) :
        word (joinEdges h x y t) ((y::M)++(x::L))=
          word h (x::L)*t*word h (y::M)*t⁻¹ := by
    …

    Mentions: OAI.IntegralCharacterVarieties.BoundaryBand.word, OAI.IntegralCharacterVarieties.BoundaryBand.joinEdges

17. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.BoundaryCircle line 146
18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySides line 148
19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySides_nodup line 151
20. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySides_ne_nil line 157
21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySides_disjoint line 163
22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySides_append_nodup line 173
23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySides_successor line 178
24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySides_agree line 187
25. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.remainingSuccessor line 195

    Source documentation

    Remove the two old circle factors. Unlike an arbitrary factor, this one will be proved to fix every occurrence on either selected circle.

    def remainingSuccessor (B C : D.BoundaryCircle) : Equiv.Perm (Side S arity) :=
    …

26. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundary_factorization line 199
27. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.remainingSuccessor_fixes line 204
28. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.old_boundary_join line 224

    Source documentation

    Old Diagram boundary successor after attaching a strip between these two circles. The resulting joined circle retains all old occurrence labels exactly once.

    theorem old_boundary_join (B C : D.BoundaryCircle) (hBC : B≠C)
        (x y : Side S arity) (L M : List (Side S arity))
        (hB : D.boundarySides B=x::L) (hC : D.boundarySides C=y::M) :
        incomingSwitch D.ports.vertexAssembly.corners.boundaryNext x y=
          (((x::L)++(y::M)).formPerm)*D.remainingSuccessor B C := by
    …

29. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryValue line 240

    Source documentation

    Exact old edge matrix viewed in the chosen facet fiber. Outside that facet it is irrelevant and set to 1; no old edge in that facet is replaced.

    def boundaryValue (f : F) (a : Side S arity) :
        (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ :=
    …

30. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.eval_rebase line 245
31. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryValue_at line 251
32. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_boundary_word line 257
33. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.old_same_facet_band line 265

    Source documentation

    Join the two selected old circles whenever their based surface-word order is explicitly recorded. The new word is DERIVED from changed old side matrices, and the new handle is constructed from the same band transport t.

    theorem old_same_facet_band (f : F) (b c : Fin (D.boundaryCount f)) (hbc : b≠c)
        (x y : Side S arity) (L M : List (Side S arity))
        (hb : D.boundarySides ⟨f,b⟩=x::L) (hc : D.boundarySides ⟨f,c⟩=y::M)
        (T : List (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ)
        (horder : D.evaluatedBoundaries P g f=
          word (D.boundaryValue P g f) (x::L)::word (D.boundaryValue P g f) (y::M)::T)
        (t : (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ) :
        incomingSwitch D.ports.vertexAssembly.corners.boundaryNext x y=
          (((y::M)++(x::L)).formPerm)*D.remainingSuccessor ⟨f,b⟩ ⟨f,c⟩ ∧
        surfaceProduct (conjugateHandles t (D.evaluatedHandles P g f)++
          [(t,word (D.boundaryValue P g f) (x::L))])
          (word (joinEdges (D.boundaryValue P g f) x y t) ((y::M)++(x::L))::
    …

34. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.ofFn_two line 290
35. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.old_first_two_band line 300

    Source documentation

    The cyclic bags below are the original first two boundary occurrence circles.

    theorem old_first_two_band (f : F) (hn : 2≤D.boundaryCount f)
        (t : (Matrix (Fin (D.rank f)) (Fin (D.rank f)) A)ˣ) :
        ∃ (x y : Side S arity) (L M : List (Side S arity)),
          D.boundarySides ⟨f,⟨0,by omega⟩⟩=x::L ∧
          D.boundarySides ⟨f,⟨1,by omega⟩⟩=y::M ∧
          incomingSwitch D.ports.vertexAssembly.corners.boundaryNext x y=
            (((y::M)++(x::L)).formPerm)*D.remainingSuccessor ⟨f,⟨0,by omega⟩⟩ ⟨f,⟨1,by omega⟩⟩ ∧
          surfaceProduct (conjugateHandles t (D.evaluatedHandles P g f)++
            [(t,word (D.boundaryValue P g f) (x::L))])
            (word (joinEdges (D.boundaryValue P g f) x y t) ((y::M)++(x::L))::
              conjugateBoundaries t ((D.evaluatedBoundaries P g f).drop 2))=
            scalarUnit (D.rank f) (D.diskScalar P f) ∧
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit