OAI/Topology/EilenbergGanea/SmallHolonomy.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EilenbergGanea.su2_distance_square line 16

   Source documentation

   Squared chord length on the unit-quaternion sphere.

   theorem su2_distance_square (a : SU2) :
       ‖(a : ℍ) - 1‖ ^ 2 = 2 - 2 * (a : ℍ).re := by
   …

   Mentions: OAI.EilenbergGanea.SU2

2. def OAI.EilenbergGanea.arcBlend line 26
3. theorem OAI.EilenbergGanea.arcBlend_norm_le line 29
4. theorem OAI.EilenbergGanea.small_unit_re line 39
5. theorem OAI.EilenbergGanea.arcBlend_re_le line 45
6. theorem OAI.EilenbergGanea.arcBlend_ne_zero line 53
7. def OAI.EilenbergGanea.smallQuaternionArc line 61

   Source documentation

   A globally smooth path that remains in the closed chord ball of its endpoint, avoiding any branch choice of a quaternion logarithm.

   def smallQuaternionArc (a : SU2) (t : ℝ) : SU2 := normalizeQuaternion (arcBlend a t)

   Mentions: OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.normalizeQuaternion, OAI.EilenbergGanea.arcBlend

8. theorem OAI.EilenbergGanea.smallQuaternionArc_zero line 63
9. theorem OAI.EilenbergGanea.smallQuaternionArc_one line 66
10. theorem OAI.EilenbergGanea.smallQuaternionArc_smooth line 69
11. theorem OAI.EilenbergGanea.smallQuaternionArc_distance line 77
12. def OAI.EilenbergGanea.selectedAlphabet line 100

    Source documentation

    The selected unknowns remain separate from coefficients, even when two letters have the same image in the group quotient.

    def selectedAlphabet (σ : Fin m ↪ E) (e : E) : E ⊕ Fin m := by
    …

13. theorem OAI.EilenbergGanea.selectedAlphabet_selected line 104
14. theorem OAI.EilenbergGanea.selectedAlphabet_other line 111
15. def OAI.EilenbergGanea.selectedWord line 116
16. def OAI.EilenbergGanea.selectedLabel line 119
17. theorem OAI.EilenbergGanea.selectedLabel_selected line 122
18. theorem OAI.EilenbergGanea.selectedLabel_other line 126
19. theorem OAI.EilenbergGanea.selectedWord_eval line 131
20. theorem OAI.EilenbergGanea.selectedWord_exponents line 142
21. theorem OAI.EilenbergGanea.selected_word_sublevel_solvable line 160

    Source documentation

    Solve a finite, full-rank system while keeping every unselected label fixed. The distinguished sublevel condition is the actual isolated root condition, not a nonsingularity assumption on the roots.

    theorem selected_word_sublevel_solvable [DecidableEq E]
        (σ : Fin m ↪ E) (w : Fin m → FreeGroup E) (ρ : Fin d → FreeGroup E)
        (a : ℝ → E → SU2) (ha : ∀ e, ContDiff ℝ ∞ (fun t => (a t e : ℍ)))
        (ha0 : ∀ e, a 0 e = 1)
        (hB : Matrix.det (fun i j => wordExponents (w i) (σ j)) ≠ 0)
        (δ : ℝ) (hδ : 0 < δ)
        (hiso : ∀ t ∈ Icc (0 : ℝ) 1, ∀ x : Fin m → SU2,
          (∀ i, FreeGroup.lift (selectedLabel σ (a t) x) (w i) = 1) →
          ‖(fun i => (FreeGroup.lift (selectedLabel σ (a t) x) (ρ i) : ℍ)) - 1‖ ≠ δ) :
        ∃ b : E → SU2,
          (∀ e, (∀ i, σ i ≠ e) → b e = a 1 e) ∧
          (∀ i, FreeGroup.lift b (w i) = 1) ∧
    …

    Mentions: OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.wordExponents, OAI.EilenbergGanea.selectedLabel

22. def OAI.EilenbergGanea.labelLift line 197
23. def OAI.EilenbergGanea.wordValue line 201
24. def OAI.EilenbergGanea.pathProduct line 203
25. theorem OAI.EilenbergGanea.labelLift_right line 206
26. theorem OAI.EilenbergGanea.pathProduct_one line 215
27. theorem OAI.EilenbergGanea.pathProduct_of line 217
28. theorem OAI.EilenbergGanea.pathProduct_mul line 219
29. theorem OAI.EilenbergGanea.pathProduct_inv line 223
30. theorem OAI.EilenbergGanea.pathProduct_conjugate_loop line 228
31. theorem OAI.EilenbergGanea.pathProduct_continuous line 235
32. theorem OAI.EilenbergGanea.pathProduct_finite_locations line 252

    Source documentation

    The set of vertices inspected by a word is finite, independently of the label values. No countability hypothesis on the alphabet is needed.

    theorem pathProduct_finite_locations (v : S → Γ) (w : FreeGroup S) (g : Γ) :
        ∃ P : Finset Γ, ∀ a b : Γ → S → H,
          (∀ p ∈ P, ∀ s, a p s = b p s) → pathProduct v a w g = pathProduct v b w g := by
    …

    Mentions: OAI.EilenbergGanea.pathProduct

33. theorem OAI.EilenbergGanea.pathProduct_pullback line 271

    Source documentation

    Evaluation commutes with pullback of a labeling along a group quotient, including when different alphabet letters have the same image.

    theorem pathProduct_pullback {D : Type*} [Group D] (q : Γ →* D)
        (v : S → Γ) (a : D → S → H) (w : FreeGroup S) (g : Γ) :
        pathProduct v (fun p s => a (q p) s) w g = pathProduct (fun s => q (v s)) a w (q g) := by
    …

    Mentions: OAI.EilenbergGanea.pathProduct

34. theorem OAI.EilenbergGanea.pathProduct_trivial_of_relators line 291

    Source documentation

    Once every final relator has trivial transport at every vertex, normal closure gives trivial transport on every null word, not just on a finite collection of test loops.

     theorem pathProduct_trivial_of_relators (v : S → Γ) (a : Γ → S → H)
        (R : Set (FreeGroup S)) (hR : R ⊆ (wordValue v).ker)
        (hp : (wordValue v).ker = Subgroup.normalClosure R)
        (ha : ∀ r ∈ R, ∀ g, pathProduct v a r g = 1)
        (w : FreeGroup S) (hw : wordValue v w = 1) (g : Γ) : pathProduct v a w g = 1 := by
    …

    Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.pathProduct

35. def OAI.EilenbergGanea.pathChain line 311
36. theorem OAI.EilenbergGanea.pathChain_one line 314
37. theorem OAI.EilenbergGanea.pathChain_of line 316
38. theorem OAI.EilenbergGanea.pathChain_mul line 318
39. theorem OAI.EilenbergGanea.pathChain_inv line 321
40. theorem OAI.EilenbergGanea.pathChain_conjugate line 324
41. abbrev OAI.EilenbergGanea.NormalFactor line 332
42. def OAI.EilenbergGanea.normalFactorWord line 334
43. def OAI.EilenbergGanea.normalFactorCount line 337
44. def OAI.EilenbergGanea.relatorChainMap line 340
45. theorem OAI.EilenbergGanea.normalFactor_value line 344
46. theorem OAI.EilenbergGanea.pathChain_normalFactor line 350
47. theorem OAI.EilenbergGanea.pathChain_normalProduct line 359
48. theorem OAI.EilenbergGanea.exact_translated_relator_counts line 372

    Source documentation

    The coefficient identity is an equality in the full free abelian group of translated indexed relators. Injectivity is sufficient; no finiteness of the relator or generator types is assumed.

     theorem exact_translated_relator_counts (v : S → Γ) (r : R → FreeGroup S)
        (hr : ∀ i, wordValue v (r i) = 1) (hinj : Function.Injective (relatorChainMap v r))
        (z : FreeGroup S) (ρ : R) (hchain : pathChain v z 1 = pathChain v (r ρ) 1)
        (l : List (NormalFactor S R)) (he : z = (l.map (normalFactorWord r)).prod) :
        (l.map (fun f => normalFactorCount v f 1)).sum = Finsupp.single (1,ρ) 1 := by
    …

    Mentions: OAI.EilenbergGanea.wordValue, OAI.EilenbergGanea.relatorChainMap, OAI.EilenbergGanea.pathChain, OAI.EilenbergGanea.NormalFactor, OAI.EilenbergGanea.normalFactorWord, OAI.EilenbergGanea.normalFactorCount

49. def OAI.EilenbergGanea.mergeLabels line 390
50. theorem OAI.EilenbergGanea.mergeLabels_continuous line 394
51. theorem OAI.EilenbergGanea.copy_labels_on_finite_set line 407

    Source documentation

    Copy arbitrary prescribed labels to a finite quotient solely on the finite set of vertices currently being tested. This does not assert that the original labeling is periodic or descends to a single quotient.

     theorem copy_labels_on_finite_set {D : Type*} [Group D] (q : Γ →* D)
        (P : Finset Γ) (hq : Set.InjOn q (P : Set Γ)) (a : Γ → S → H)
        (Allowed : H → Prop) (h1 : Allowed 1) (ha : ∀ g s, Allowed (a g s)) :
        ∃ aF : D → S → H, (∀ d s, Allowed (aF d s)) ∧ ∀ p ∈ P, ∀ s, aF (q p) s = a p s := by
    …

52. theorem OAI.EilenbergGanea.compact_labeling_from_finite_quotients line 428

    Source documentation

    Tychonoff compactness for all extra generators, with the original labels fixed. The finite-quotient premise is exactly the separate finite solvability obligation, not a periodicity assumption on the prescribed assignment.

     theorem compact_labeling_from_finite_quotients [Group.ResiduallyFinite Γ]
        [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H]
        (v : S ⊕ T → Γ) (a : Γ → S → H) (w : I → FreeGroup (S ⊕ T)) (g : I → Γ)
        (K : I → Set H) (hK : ∀ i, IsClosed (K i))
        (Allowed : H → Prop) (h1 : Allowed 1) (ha : ∀ g s, Allowed (a g s))
        (hsolve : ∀ (N : FiniteIndexNormalSubgroup Γ) (J : Finset I)
          (aF : (Γ ⧸ N.toSubgroup) → S → H), (∀ d s, Allowed (aF d s)) →
          ∃ bF : (Γ ⧸ N.toSubgroup) → T → H, ∀ i ∈ J, ∀ d,
            pathProduct (fun s => QuotientGroup.mk' N.toSubgroup (v s))
              (mergeLabels aF bF) (w i) d ∈ K i) :
        ∃ b : Γ → T → H, ∀ i, pathProduct v (mergeLabels a b) (w i) (g i) ∈ K i := by
    …

    Mentions: OAI.EilenbergGanea.pathProduct, OAI.EilenbergGanea.mergeLabels

53. theorem OAI.EilenbergGanea.su2_norm line 473
54. theorem OAI.EilenbergGanea.unit_product_linearization line 481

    Source documentation

    The two elementary estimates needed for the presentation argument, with constants independent of the Cayley graph or any finite quotient.

    theorem unit_product_linearization (l : List ℍ) (h : ℝ) (hh : 0 ≤ h)
        (hu : ∀ a ∈ l, ‖a‖ = 1) (hb : ∀ a ∈ l, ‖a - 1‖ ≤ h) :
        ‖l.prod - 1‖ ≤ l.length * h ∧
        ‖l.prod - 1 - (l.map (fun a => a - 1)).sum‖ ≤ (l.length : ℝ)^2 * h^2 := by
    …

55. theorem OAI.EilenbergGanea.quaternion_commutator_bound line 511
56. theorem OAI.EilenbergGanea.su2_conjugation_error line 519
57. theorem OAI.EilenbergGanea.su2_inverse_distance line 529
58. theorem OAI.EilenbergGanea.su2_inverse_linearization line 535
59. theorem OAI.EilenbergGanea.unit_product_with_linear_models line 546

    Source documentation

    Replacing each displacement by its linear model introduces only the sum of the errors. Combined with exact signed counts, this avoids any choice of an ordering of the relator indices (which can be uncountable).

    theorem unit_product_with_linear_models {I : Type*} (l : List I)
        (f : I → SU2) (v : I → ℍ) (h D : ℝ) (hh : 0 ≤ h)
        (hb : ∀ i ∈ l, ‖(f i : ℍ) - 1‖ ≤ h)
        (he : ∀ i ∈ l, ‖(f i : ℍ) - 1 - v i‖ ≤ D) :
        ‖((l.map (fun i => (f i : ℍ))).prod - 1) - (l.map v).sum‖ ≤
          (l.length : ℝ)^2 * h^2 + l.length * D := by
    …

    Mentions: OAI.EilenbergGanea.SU2

60. theorem OAI.EilenbergGanea.su2_conjugation_distance line 580
61. def OAI.EilenbergGanea.signedUnit line 588
62. def OAI.EilenbergGanea.signedDisplacement line 589
63. theorem OAI.EilenbergGanea.signedUnit_distance line 591
64. theorem OAI.EilenbergGanea.signedUnit_error line 595
65. theorem OAI.EilenbergGanea.conjugated_signedUnit_error line 603
66. abbrev OAI.EilenbergGanea.RelatorFactor line 620
67. def OAI.EilenbergGanea.relatorFactorValue line 622
68. def OAI.EilenbergGanea.relatorSignedCounts line 625
69. theorem OAI.EilenbergGanea.relator_linear_models line 628
70. theorem OAI.EilenbergGanea.relator_product_quadratic line 643

    Source documentation

    Exact translated counts cancel the full linear term; the remaining bound is quadratic. The index set is arbitrary, not necessarily countable.

    theorem relator_product_quadratic {I : Type*} (l : List (RelatorFactor I)) (x : I → SU2)
        (i₀ : I) (hc : relatorSignedCounts l = Finsupp.single i₀ 1)
        (h ε K : ℝ) (hh : 0 ≤ h) (hε : 0 ≤ ε) (hK : 0 ≤ K)
        (hb : ∀ r ∈ l, ‖(x r.2.1 : ℍ) - 1‖ ≤ h)
        (ha : ∀ r ∈ l, ‖(r.1 : ℍ) - 1‖ ≤ K * (ε + h)) :
        ‖(l.map (fun r => (relatorFactorValue x r : ℍ))).prod - (x i₀ : ℍ)‖ ≤
          ((l.length : ℝ)^2 + l.length + 2 * l.length * K) * (ε + h) * h := by
    …

    Mentions: OAI.EilenbergGanea.RelatorFactor, OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.relatorSignedCounts, OAI.EilenbergGanea.relatorFactorValue

71. def OAI.EilenbergGanea.familySize line 671

    Source documentation

    A uniform size for an arbitrary family, normalized to zero for an empty index set. This is a real supremum, not an attained maximum.

    def familySize {I : Type*} (f : I → ℝ) : ℝ := sSup (Set.range f ∪ {0})

72. theorem OAI.EilenbergGanea.familySize_nonneg line 673
73. theorem OAI.EilenbergGanea.le_familySize line 678
74. theorem OAI.EilenbergGanea.familySize_le line 681
75. theorem OAI.EilenbergGanea.familySize_ne_threshold line 690

    Source documentation

    The source no-threshold-crossing argument does not assume attainment of its supremum.

     theorem familySize_ne_threshold {I : Type*} (f : I → ℝ)
        (hf : BddAbove (Set.range f)) (C δ η ε : ℝ)
        (hδ : 0 < δ) (hC : 0 ≤ C) (_hη : 0 ≤ η) (hε : 0 ≤ ε) (hεη : ε ≤ η)
        (hc₁ : C * (δ + η) < 1/2) (hc₂ : C * η < δ/2)
        (hbound : ∀ i, f i ≤ C * ε + C * (familySize f + ε) * familySize f) :
        familySize f ≠ δ := by
    …

    Mentions: OAI.EilenbergGanea.familySize

76. theorem OAI.EilenbergGanea.familySize_contraction line 706

    Source documentation

    Uniform contraction of all residual errors. This handles even an uncountable family and does not replace the supremum by a maximum.

     theorem familySize_contraction {I : Type*} (f : I → ℝ)
        (hf : ∀ i, 0 ≤ f i) (δ C η : ℝ) (hδ : 0 ≤ δ) (hC : 0 ≤ C) (hη : 0 ≤ η)
        (hb : ∀ i, f i ≤ δ) (hc : C * (δ + η) < 1)
        (he : ∀ i, f i ≤ C * (familySize f + η) * familySize f) : ∀ i, f i = 0 := by
    …

    Mentions: OAI.EilenbergGanea.familySize

77. theorem OAI.EilenbergGanea.small_thresholds_exist line 724