OAI/Topology/EilenbergGanea/AffineTransport.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EilenbergGanea.AffineTransport.exists_avoid_subspaces line 15

   Source documentation

   A finite family of proper quaternion subspaces cannot cover ℍ.

   theorem exists_avoid_subspaces {I : Type*} [Finite I]
       (p : I → Submodule ℝ ℍ) (hp : ∀ i, p i ≠ ⊤) :
       ∃ q : ℍ, ∀ i, q ∉ p i := by
   …

2. theorem OAI.EilenbergGanea.AffineTransport.exists_triangle_general_position line 31

   Source documentation

   Simultaneous general position for finitely many local quaternion gauges. Different vertices may use different invertible linear transformations in each chart. No flatness or topology is assumed in this finite-dimensional lemma.

   theorem exists_triangle_general_position {A V : Type*} [Finite A] [Fintype V]
       (T : A → V → ℍ ≃ₗ[ℝ] ℍ) :
       ∃ q : V → ℍ, ∀ a (s : Finset V), s.card ≤ 3 →
         LinearIndepOn ℝ (fun v => T a v (q v)) (s : Set V) := by
   …

3. theorem OAI.EilenbergGanea.AffineTransport.unit_norm line 120
4. def OAI.EilenbergGanea.AffineTransport.leftLinearEquiv line 123
5. theorem OAI.EilenbergGanea.AffineTransport.leftLinearEquiv_apply line 131
6. theorem OAI.EilenbergGanea.AffineTransport.normalize_left line 134
7. def OAI.EilenbergGanea.AffineTransport.coordinateSimplex line 146
8. def OAI.EilenbergGanea.AffineTransport.face line 150

   Source documentation

   Closed coordinate face of the standard simplex.

   def face (s : Finset V) : Set (V → ℝ) :=
   …

9. def OAI.EilenbergGanea.AffineTransport.triangleSet line 154

   Source documentation

   The whole two-skeleton of a finite standard simplex.

   def triangleSet : Set (V → ℝ) :=
   …

10. abbrev OAI.EilenbergGanea.AffineTransport.TrianglePoint line 157
11. theorem OAI.EilenbergGanea.AffineTransport.mem_triangleSet line 159
12. theorem OAI.EilenbergGanea.AffineTransport.isClosed_face_support line 164
13. theorem OAI.EilenbergGanea.AffineTransport.isCompact_face line 172
14. theorem OAI.EilenbergGanea.AffineTransport.isCompact_triangleSet line 181
15. instance OAI.EilenbergGanea.AffineTransport.(instance at line 184) line 184
16. theorem OAI.EilenbergGanea.AffineTransport.point_simplex line 187
17. theorem OAI.EilenbergGanea.AffineTransport.point_exists_nonzero line 191
18. def OAI.EilenbergGanea.AffineTransport.rawGauge line 199
19. def OAI.EilenbergGanea.AffineTransport.GeneralPosition line 201
20. theorem OAI.EilenbergGanea.AffineTransport.exists_generalPosition line 204
21. theorem OAI.EilenbergGanea.AffineTransport.rawGauge_ne_zero line 208
22. def OAI.EilenbergGanea.AffineTransport.gauge line 228
23. theorem OAI.EilenbergGanea.AffineTransport.continuous_rawGauge line 230
24. theorem OAI.EilenbergGanea.AffineTransport.continuous_gauge line 233
25. theorem OAI.EilenbergGanea.AffineTransport.gauges_uniform line 241

    Source documentation

    Uniform modulus over all charts, including across the edges of all simplices.

    theorem gauges_uniform (hq : GeneralPosition h q) {ε : ℝ} (hε : 0 < ε) :
        ∃ δ > 0, ∀ b c : TrianglePoint V, dist b c < δ →
          ∀ a, dist (gauge h q a b) (gauge h q a c) < ε := by
    …

    Mentions: OAI.EilenbergGanea.AffineTransport.GeneralPosition, OAI.EilenbergGanea.AffineTransport.TrianglePoint, OAI.EilenbergGanea.AffineTransport.gauge

26. theorem OAI.EilenbergGanea.AffineTransport.unitary_dist_left line 254
27. theorem OAI.EilenbergGanea.AffineTransport.unitary_dist_inv_mul_one line 258
28. theorem OAI.EilenbergGanea.AffineTransport.unitary_dist_mul_one_le line 262
29. def OAI.EilenbergGanea.AffineTransport.Related line 274
30. theorem OAI.EilenbergGanea.AffineTransport.Related.refl line 277
31. theorem OAI.EilenbergGanea.AffineTransport.Related.symm line 280
32. def OAI.EilenbergGanea.AffineTransport.Star line 285
33. def OAI.EilenbergGanea.AffineTransport.CliquePoint line 288
34. def OAI.EilenbergGanea.AffineTransport.Compatible line 291
35. def OAI.EilenbergGanea.AffineTransport.root line 295
36. theorem OAI.EilenbergGanea.AffineTransport.root_mem line 297
37. def OAI.EilenbergGanea.AffineTransport.FlatConnection line 302
38. theorem OAI.EilenbergGanea.AffineTransport.rawGauge_transition line 305
39. theorem OAI.EilenbergGanea.AffineTransport.gauge_transition line 316
40. def OAI.EilenbergGanea.AffineTransport.chartTransport line 324
41. def OAI.EilenbergGanea.AffineTransport.transport line 327
42. theorem OAI.EilenbergGanea.AffineTransport.transport_chart line 329
43. theorem OAI.EilenbergGanea.AffineTransport.compatible_symm line 341
44. theorem OAI.EilenbergGanea.AffineTransport.transport_reverse line 344
45. theorem OAI.EilenbergGanea.AffineTransport.chartTransport_trans line 353
46. theorem OAI.EilenbergGanea.AffineTransport.exists_large_coordinate line 358
47. theorem OAI.EilenbergGanea.AffineTransport.nearby_star line 369
48. theorem OAI.EilenbergGanea.AffineTransport.chartTransport_dist line 379
49. theorem OAI.EilenbergGanea.AffineTransport.transport_uniform line 383
50. def OAI.EilenbergGanea.AffineTransport.edgeTransport line 389

    Source documentation

    Two compatible pieces, rather than a chosen homotopy class of paths, suffice.

    def edgeTransport (b c d : TrianglePoint V) : SU2 := transport h q b c * transport h q c d

    Mentions: OAI.EilenbergGanea.AffineTransport.TrianglePoint, OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.AffineTransport.transport

51. theorem OAI.EilenbergGanea.AffineTransport.edgeTransport_chart line 391
52. theorem OAI.EilenbergGanea.AffineTransport.edgeTransport_reverse line 398
53. theorem OAI.EilenbergGanea.AffineTransport.edgeTransport_uniform line 404
54. theorem OAI.EilenbergGanea.AffineTransport.edgeTransport_triangle line 416

    Source documentation

    All three edge images in one chart have exactly trivial triangle holonomy.

    theorem edgeTransport_triangle (hf : FlatConnection L h) (hq : GeneralPosition h q)
        (b c d u v w : TrianglePoint V) {a : V}
        (hbu : Compatible L b u) (huc : Compatible L u c)
        (hcv : Compatible L c v) (hvd : Compatible L v d)
        (hdw : Compatible L d w) (hwb : Compatible L w b)
        (hab : Star L a b) (hac : Star L a c) (had : Star L a d)
        (hau : Star L a u) (hav : Star L a v) (haw : Star L a w) :
        edgeTransport h q b u c * edgeTransport h q c v d * edgeTransport h q d w b = 1 := by
    …

    Mentions: OAI.EilenbergGanea.AffineTransport.FlatConnection, OAI.EilenbergGanea.AffineTransport.GeneralPosition, OAI.EilenbergGanea.AffineTransport.TrianglePoint, OAI.EilenbergGanea.AffineTransport.Compatible, OAI.EilenbergGanea.AffineTransport.Star, OAI.EilenbergGanea.AffineTransport.edgeTransport

55. theorem OAI.EilenbergGanea.AffineTransport.nearby_family_chart line 431

    Source documentation

    A uniform local chart for any finite or infinite family of nearby clique points.

    theorem nearby_family_chart {I : Type*} (b : TrianglePoint V) (c : I → TrianglePoint V)
        (hc : ∀ i, CliquePoint L (c i))
        (hbc : ∀ i, dist b (c i) < 1 / (Fintype.card V + 1 : ℝ)) :
        ∃ a, ∀ i, Star L a (c i) := by
    …

    Mentions: OAI.EilenbergGanea.AffineTransport.TrianglePoint, OAI.EilenbergGanea.AffineTransport.CliquePoint, OAI.EilenbergGanea.AffineTransport.Star