OAI/AlgebraicGeometry/CharacterVarieties/Cutting/BoundarySurgery.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Boundary circuits and their noncommutative words under finite splicing.

This formalizes the band reconstruction for filtered surface local systems in Integral points on character varieties of curves.

  1. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.parentSurgery line 18
  2. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.childSurgery line 20
  3. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.positiveRelabel_child line 23
  4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.positiveRelabel_cut line 32
  5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.rewire_boundary_unchanged line 45

    Source documentation

    Actual successor in UNCHANGED positive-port side coordinates. Parents are postcomposed and children are precomposed. Omitting this distinction incorrectly assigns the old child monodromy to a new identity short side.

    lemma rewire_boundary_unchanged (a : Side W.Seam W.seamArity) :
    ((W.rewire C hC).assemble (fun _ => ()) (fun _=>rfl)).vertexAssembly.corners.boundaryNext a=
      W.parentSurgery C (((W.assemble (fun _ => ()) (fun _=>rfl)).vertexAssembly.corners.boundaryNext)
        (W.childSurgery C hC a)) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.assemble

  6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.parentSurgery_number line 53
  7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.childSurgery_number line 58
  8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.parentSurgery_fixed line 64
  9. def OAI.IntegralCharacterVarieties.BoundarySurgery.pairSwap line 79
  10. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.pairSwap_same line 82
  11. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.pairSwap_other line 86
  12. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.pairSwap_product line 92
  13. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.pairSwap_product_away line 108
  14. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.childPair line 122
  15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.swap_arity line 137
  16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.childPair_number line 148
  17. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.childSurgery_swap line 153
  18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.childSurgery_mul line 210
  19. def OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord line 229
  20. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord_add line 232
  21. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.splice_word_prefix line 248
  22. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.splice_cycleWord line 259

    Source documentation

    Ordered boundary word under literal oriented-end splicing. The proof retains the entire cyclic order, not only the number of boundary components.

    lemma splice_cycleWord (u : α → G) :
    cycleWord (Equiv.swap x y*N) u x (s.card+t.card)=
      cycleWord N u y t.card*cycleWord N u x s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord

  23. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord_one_on line 269
  24. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.splice_cycleWord_identity line 282

    Source documentation

    A full identity-transport strip disk inserted into an old circuit leaves its based monodromy unchanged. This is the exact full-ring word step required by the lower-strip cut; noncommutative old coefficients remain arbitrary.

    lemma splice_cycleWord_identity (u : α → G) (hu : ∀ z∈t,u z=1) :
    cycleWord (Equiv.swap x y*N) u x (s.card+t.card)=cycleWord N u x s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord

  25. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord_zero line 293
  26. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord_one line 295
  27. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_pow_shift line 298
  28. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_isCycle line 310
  29. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_pow_lt line 315
  30. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_word_prefix line 321
  31. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_return line 330
  32. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_cycleWord_identity line 341

    Source documentation

    In CHILD-side coordinates the cut precomposes the old successor; the identity strip is inserted AFTER the old weighted side. This retains the exact based monodromy, and does not move its weight onto the new short occurrence.

    lemma preSplice_cycleWord_identity (u : α → G) (hu : ∀ z∈t,u z=1) :
    cycleWord (N*Equiv.swap x y) u x (s.card+t.card)=cycleWord N u x s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord

  33. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.pow_eq_on line 364
  34. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.isCycleOn_eqOn line 372
  35. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_away line 386
  36. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord_eqOn line 394
  37. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.tripleSplice_isCycle line 409
  38. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.tripleSplice_cycleWord_identity line 422

    Source documentation

    The whole three-port cut inserts BOTH distinct contacted strips. This is not inferred from ranks, equal facet labels, or a one-strip approximation.

    lemma tripleSplice_cycleWord_identity (u : α → G)
    (hut : ∀ a∈t,u a=1) (huv : ∀ a∈v,u a=1) :
    cycleWord (N*(Equiv.swap x z*Equiv.swap x y)) u x (s.card+v.card+t.card)=
      cycleWord N u x s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord

  39. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord_rotate line 441
  40. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_cycleWord_allBases line 457

    Source documentation

    Identity-strip insertion preserves the based word at EVERY old occurrence, not only at the short-side contact chosen to describe the surgery.

    lemma preSplice_cycleWord_allBases (u : α → G) (hu : ∀ z∈t,u z=1)
    (a : α) (ha : a∈s) :
    cycleWord (N*Equiv.swap x y) u a (s.card+t.card)=cycleWord N u a s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord

  41. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSplice_word_allBases_card line 480
  42. def OAI.IntegralCharacterVarieties.BoundarySurgery.preSpliceFamily line 494

    Source documentation

    Insert a finite family of separate doubled strips AFTER their old child occurrences. Several old contacts may lie on the same old boundary circle.

    noncomputable def preSpliceFamily (N : Equiv.Perm α) (x y : ι → α) : List ι → Equiv.Perm α
  | [] => N
  | i::is => preSpliceFamily (N*Equiv.swap (x i) (y i)) x y is
  43. def OAI.IntegralCharacterVarieties.BoundarySurgery.attachedCircle line 498
  44. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSpliceFamily_cycle line 504

    Source documentation

    The full old circle, with every contacted identity strip, remains ONE actual cycle, and its word is preserved at EVERY old based occurrence.

    lemma preSpliceFamily_cycle (N : Equiv.Perm α) (s : Finset α) (x y : ι → α)
    (t : ι → Finset α) (is : List ι)
    (hs : N.IsCycleOn (s : Set α))
    (ht : ∀ i∈is,N.IsCycleOn (t i : Set α))
    (hx : ∀ i∈is,x i∈s) (hy : ∀ i∈is,y i∈t i)
    (hst : ∀ i∈is,Disjoint s (t i))
    (htt : is.Pairwise (fun i j => Disjoint (t i) (t j)))
    (u : α → G) (hu : ∀ i∈is,∀ z∈t i,u z=1) :
    (preSpliceFamily N x y is).IsCycleOn (attachedCircle s t is : Set α) ∧
    ∀ a∈s,cycleWord (preSpliceFamily N x y is) u a (attachedCircle s t is).card=
      cycleWord N u a s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.BoundarySurgery.preSpliceFamily, OAI.IntegralCharacterVarieties.BoundarySurgery.attachedCircle, OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord

  45. def OAI.IntegralCharacterVarieties.BoundarySurgery.attachedCircleOn line 539
  46. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSpliceFamily_cycleOn line 546

    Source documentation

    This is the version for the whole actual seam. Contacts on other old circles are retained in the surgery, rather than being assumed absent.

    lemma preSpliceFamily_cycleOn (N : Equiv.Perm α) (s : Finset α) (x y : ι → α)
    (t : ι → Finset α) (is : List ι)
    (hs : N.IsCycleOn (s : Set α))
    (ht : ∀ i∈is,N.IsCycleOn (t i : Set α))
    (hy : ∀ i∈is,y i∈t i)
    (hst : ∀ i∈is,Disjoint s (t i))
    (hxt : ∀ i∈is,∀ j∈is,x i∉t j)
    (htt : is.Pairwise (fun i j => Disjoint (t i) (t j)))
    (u : α → G) (hu : ∀ i∈is,∀ z∈t i,u z=1) :
    (preSpliceFamily N x y is).IsCycleOn (attachedCircleOn s x t is : Set α) ∧
    ∀ a∈s,cycleWord (preSpliceFamily N x y is) u a (attachedCircleOn s x t is).card=
      cycleWord N u a s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.BoundarySurgery.preSpliceFamily, OAI.IntegralCharacterVarieties.BoundarySurgery.attachedCircleOn, OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord

  47. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.swap_irrel line 602
  48. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSpliceFamily_product line 607
  49. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSpliceFamily_append line 614
  50. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.tripleContacts line 625
  51. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.tripleOld line 629
  52. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.tripleNew line 630
  53. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.tripleContacts_nodup line 635
  54. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.childSurgery_triple line 647
  55. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.triple_preSplice line 660
  56. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftPerm_swaps line 676
  57. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.embedding_pow line 692
  58. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.embedding_isCycle line 699
  59. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.embedding_cycleWord line 717