OAI/Topology/EilenbergGanea/UnitaryWords.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.EilenbergGanea.SU2 line 18
2. theorem OAI.EilenbergGanea.quaternion_mem_unitary_iff line 20
3. instance OAI.EilenbergGanea.su2_compactSpace line 30
4. def OAI.EilenbergGanea.circleQuaternion line 38
5. theorem OAI.EilenbergGanea.circleQuaternion_coe line 48
6. theorem OAI.EilenbergGanea.circleQuaternion_injective line 51
7. theorem OAI.EilenbergGanea.circleQuaternion_continuous line 58
8. def OAI.EilenbergGanea.wordMap line 62
9. def OAI.EilenbergGanea.exponentMatrix line 65
10. def OAI.EilenbergGanea.normalizeQuaternion line 74

    Source documentation

    Radial normalization is only used on nonzero quaternions. The harmless value at zero makes it a total function without changing that domain.

    def normalizeQuaternion (q : ℍ) : SU2 := by
    …

    Mentions: OAI.EilenbergGanea.SU2

11. theorem OAI.EilenbergGanea.normalizeQuaternion_coe_of_ne_zero line 81
12. theorem OAI.EilenbergGanea.normalizeQuaternion_coe_contDiffAt line 84
13. theorem OAI.EilenbergGanea.normalizeQuaternion_continuousAt line 92
14. theorem OAI.EilenbergGanea.normalizeQuaternion_unitary line 96
15. theorem OAI.EilenbergGanea.freeGroup_lift_coe_contDiffAt line 104

    Source documentation

    Smoothness of coefficient-free word evaluation follows directly by induction, using quaternion conjugation for unitary inverses.

    theorem freeGroup_lift_coe_contDiffAt {D ι : Type*}
        [NormedAddCommGroup D] [NormedSpace ℝ D] (w : FreeGroup ι)
        (a : D) (x : D → ι → SU2)
        (hx : ∀ i, ContDiffAt ℝ ∞ (fun z => (x z i : ℍ)) a) :
        ContDiffAt ℝ ∞ (fun z => ((FreeGroup.lift (x z) w : SU2) : ℍ)) a := by
    …

    Mentions: OAI.EilenbergGanea.SU2

16. def OAI.EilenbergGanea.radialWordMap line 122
17. theorem OAI.EilenbergGanea.radialWordMap_norm line 126
18. theorem OAI.EilenbergGanea.radialWordMap_contDiffAt line 132
19. theorem OAI.EilenbergGanea.radialWordMap_eq_one_iff line 140
20. def OAI.EilenbergGanea.radialCutoff line 160

    Source documentation

    A conjugation-invariant smooth cutoff, zero near coordinate hyperplanes and one near the unit quaternion locus.

    def radialCutoff {m : ℕ} (x : Fin m → ℍ) : ℝ :=
    …

21. def OAI.EilenbergGanea.smoothRadialWordMap line 163
22. theorem OAI.EilenbergGanea.radialCutoff_contDiff line 166
23. theorem OAI.EilenbergGanea.radialCutoff_nonneg line 173
24. theorem OAI.EilenbergGanea.radialCutoff_le_one line 176
25. theorem OAI.EilenbergGanea.radialCutoff_eq_one line 180
26. theorem OAI.EilenbergGanea.radialCutoff_eventually_zero line 187
27. theorem OAI.EilenbergGanea.radialCutoff_eventually_one line 196
28. theorem OAI.EilenbergGanea.smoothRadialWordMap_contDiff line 206
29. theorem OAI.EilenbergGanea.smoothRadialWordMap_eq_one_iff line 218
30. theorem OAI.EilenbergGanea.smoothRadialWordMap_eventuallyEq line 235
31. def OAI.EilenbergGanea.splitComplex line 247
32. def OAI.EilenbergGanea.radialAngularLinear line 255
33. theorem OAI.EilenbergGanea.radialAngularLinear_apply line 260
34. theorem OAI.EilenbergGanea.radialAngularLinear_det line 263
35. def OAI.EilenbergGanea.complexPolarChart line 274
36. def OAI.EilenbergGanea.complexRadialTorus line 276
37. theorem OAI.EilenbergGanea.normalize_complex_mul_exp line 279
38. theorem OAI.EilenbergGanea.complexRadialTorus_chart line 290
39. def OAI.EilenbergGanea.complexDiagonal line 313

    Source documentation

    The real derivative of multiplication by a unit complex tuple has determinant one.

    def complexDiagonal (x : n → ℂ) : (n → ℂ) →L[ℝ] (n → ℂ) :=
    …

40. theorem OAI.EilenbergGanea.complexDiagonal_apply line 316
41. theorem OAI.EilenbergGanea.complexDiagonal_det line 319
42. theorem OAI.EilenbergGanea.complexPolarChart_hasFDerivAt line 327
43. theorem OAI.EilenbergGanea.exp_radialAngularLinear_hasFDerivAt line 341
44. theorem OAI.EilenbergGanea.complexRadialTorus_differentiableAt line 349
45. theorem OAI.EilenbergGanea.complexRadialTorus_det line 367

    Source documentation

    At every torus root, the radial extension has exactly determinant det B. The extra radial coordinates contribute the identity, not an additional sign.

    theorem complexRadialTorus_det (B : Matrix n n ℤ) (x : n → ℂ)
        (hx : ∀ i, ‖x i‖ = 1) (hroot : ∀ i, ∏ j, x j ^ B i j = 1) :
        (fderiv ℝ (complexRadialTorus B) x).det = (B.det : ℝ) := by
    …

    Mentions: OAI.EilenbergGanea.complexRadialTorus

46. def OAI.EilenbergGanea.wordExponents line 391
47. theorem OAI.EilenbergGanea.wordExponents_one line 395
48. theorem OAI.EilenbergGanea.wordExponents_of line 398
49. theorem OAI.EilenbergGanea.wordExponents_inv line 402
50. theorem OAI.EilenbergGanea.wordExponents_mul line 406
51. theorem OAI.EilenbergGanea.freeGroup_lift_commutative line 410
52. def OAI.EilenbergGanea.quaternionCoordinates line 424
53. theorem OAI.EilenbergGanea.quaternionCoordinates_apply line 432
54. theorem OAI.EilenbergGanea.quaternionCoordinates_ofComplex line 435
55. theorem OAI.EilenbergGanea.norm_quaternion_ofComplex line 439
56. def OAI.EilenbergGanea.quaternionTupleCoordinates line 445
57. theorem OAI.EilenbergGanea.quaternionTupleCoordinates_fixed line 456
58. theorem OAI.EilenbergGanea.quaternionTupleCoordinates_symm_fixed line 462
59. def OAI.EilenbergGanea.normalizeCircle line 467

    Source documentation

    Circle normalization chosen compatibly with quaternion normalization.

    def normalizeCircle (z : ℂ) : Circle := by
    …

60. theorem OAI.EilenbergGanea.normalizeCircle_coe_of_ne_zero line 471
61. theorem OAI.EilenbergGanea.normalizeQuaternion_ofComplex line 474
62. theorem OAI.EilenbergGanea.wordMap_circleQuaternion line 491
63. theorem OAI.EilenbergGanea.radialWordMap_fixed line 504
64. theorem OAI.EilenbergGanea.quaternionCoordinates_conjComplex line 521
65. theorem OAI.EilenbergGanea.quaternionCoordinates_conjCircle line 528
66. def OAI.EilenbergGanea.quaternionConjugate line 534

    Source documentation

    Ambient conjugation, compatible with the group operation on unit quaternions.

    def quaternionConjugate (a : SU2) (q : ℍ) : ℍ := (a : ℍ) * q * star (a : ℍ)

    Mentions: OAI.EilenbergGanea.SU2

67. theorem OAI.EilenbergGanea.quaternionConjugate_norm line 536
68. theorem OAI.EilenbergGanea.quaternionConjugate_zero line 541
69. theorem OAI.EilenbergGanea.quaternionConjugate_one line 544
70. theorem OAI.EilenbergGanea.quaternionConjugate_smul line 547
71. theorem OAI.EilenbergGanea.quaternionConjugate_coe line 551
72. theorem OAI.EilenbergGanea.normalizeQuaternion_conjugate line 554
73. theorem OAI.EilenbergGanea.wordMap_conjugation line 567
74. theorem OAI.EilenbergGanea.radialWordMap_conjugation line 580
75. theorem OAI.EilenbergGanea.smoothRadialWordMap_conjugation line 588
76. theorem OAI.EilenbergGanea.complex_root_of_unity_norm line 601
77. theorem OAI.EilenbergGanea.rootsOfUnity_isPGroup line 606
78. theorem OAI.EilenbergGanea.rootsOfUnity_exists_nonreal line 611
79. theorem OAI.EilenbergGanea.circle_exists_square_root line 633
80. def OAI.EilenbergGanea.splitWordMap line 648
81. theorem OAI.EilenbergGanea.splitWordMap_contDiff line 652
82. theorem OAI.EilenbergGanea.quaternionTupleCoordinates_conjCircle line 657
83. theorem OAI.EilenbergGanea.splitWordMap_rotation line 670
84. theorem OAI.EilenbergGanea.splitWordMap_fixed_eventually line 691
85. theorem OAI.EilenbergGanea.splitWordMap_fixed_det line 710
86. theorem OAI.EilenbergGanea.splitWordMap_zero_iff line 726
87. theorem OAI.EilenbergGanea.splitWordMap_fixed_zero_iff line 738
88. theorem OAI.EilenbergGanea.splitWordMap_fixed_one line 759
89. theorem OAI.EilenbergGanea.zpow_finite_sum line 771
90. def OAI.EilenbergGanea.torusMap line 778
91. theorem OAI.EilenbergGanea.torusMap_comp line 782
92. theorem OAI.EilenbergGanea.torusMap_det_one line 793
93. theorem OAI.EilenbergGanea.torusMap_kernel_pow_det line 798
94. theorem OAI.EilenbergGanea.circle_finite_pow_roots line 804
95. theorem OAI.EilenbergGanea.torusMap_finite_kernel line 816
96. theorem OAI.EilenbergGanea.splitWordMap_fixed_finite line 828
97. theorem OAI.EilenbergGanea.word_exists_regularization_nonzero_count line 854

    Source documentation

    The signed-root noncancellation for the actual ambient quaternion word map, with no regularity assumed of the original word map.

    theorem word_exists_regularization_nonzero_count {m : ℕ}
        (w : Fin m → FreeGroup (Fin m)) (hB : (exponentMatrix w).det ≠ 0)
        (K : Set ((Fin m → ℂ) × (Fin m → ℂ))) (hK : IsCompact K)
        (hKi : ∀ z : ℂ, ‖z‖ = 1 → ∀ q ∈ K, (q.1, z • q.2) ∈ K)
        (h1 : (1, 0) ∈ K)
        (L : Set ((Fin m → ℂ) × (Fin m → ℂ))) (hL : IsCompact L) (hKL : K ⊆ L)
        (ε : ℝ) (hε : 0 < ε) :
        ∃ g : ((Fin m → ℂ) × (Fin m → ℂ)) → ((Fin m → ℂ) × (Fin m → ℂ)),
          ContDiff ℝ ∞ g ∧ (∀ q ∈ L, ‖g q - splitWordMap w q‖ < ε) ∧
          ∃ s : Finset ((Fin m → ℂ) × (Fin m → ℂ)),
            (∀ q, q ∈ s ↔ q ∈ K ∧ g q = 0) ∧
            (∀ q ∈ s, (fderiv ℝ g q).det ≠ 0) ∧
    …

    Mentions: OAI.EilenbergGanea.exponentMatrix, OAI.EilenbergGanea.splitWordMap