OAI/Topology/EilenbergGanea/LevelTransport.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EilenbergGanea.LevelTransport.point line 18
2. theorem OAI.EilenbergGanea.LevelTransport.point_val line 29
3. theorem OAI.EilenbergGanea.LevelTransport.point_mem_support line 32
4. theorem OAI.EilenbergGanea.LevelTransport.point_clique line 39
5. theorem OAI.EilenbergGanea.LevelTransport.point_step line 48

   Source documentation

   Both hypotheses refer to actual reduced Artin lengths, not an assumed word metric.

   theorem point_step (g : ArtinGroup L) (x : Letter V)
       (hg : 0 < traceLength L (artinNormalTrace L g))
       (hgx : 0 < traceLength L (artinNormalTrace L (g * letterValue (artinGenerator L) x)))
       (N : ℕ) (hNg : N ≤ traceLength L (artinNormalTrace L g))
       (hNgx : N ≤ traceLength L (artinNormalTrace L (g * letterValue (artinGenerator L) x))) :
       Compatible L (point L hdim g hg) (point L hdim (g * letterValue (artinGenerator L) x) hgx) ∧
       dist (point L hdim g hg) (point L hdim (g * letterValue (artinGenerator L) x) hgx) ≤
         2 / (N+1 : ℝ) := by
   …

   Mentions: OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.LevelTransport.point

6. abbrev OAI.EilenbergGanea.LevelTransport.NegativeLevel line 84

   Source documentation

   The integral level downstairs; the action is by left multiplication by the height kernel.

   abbrev NegativeLevel (N : ℕ) := {g : ArtinGroup L // (height L g).toAdd = -(N : ℤ)}
   …

7. theorem OAI.EilenbergGanea.LevelTransport.negative_level_length line 87
8. def OAI.EilenbergGanea.LevelTransport.levelPoint line 94
9. theorem OAI.EilenbergGanea.LevelTransport.levelPoint_val line 97
10. def OAI.EilenbergGanea.LevelTransport.upperVertex line 100
11. def OAI.EilenbergGanea.LevelTransport.edgeVertex line 108
12. theorem OAI.EilenbergGanea.LevelTransport.edgeVertex_reverse line 116
13. theorem OAI.EilenbergGanea.LevelTransport.upperVertex_reverse line 123
14. theorem OAI.EilenbergGanea.LevelTransport.upperPoint_step line 129
15. def OAI.EilenbergGanea.LevelTransport.edgeLabel line 148
16. theorem OAI.EilenbergGanea.LevelTransport.edgeLabel_reverse line 153
17. theorem OAI.EilenbergGanea.LevelTransport.edgeLabel_uniform line 164
18. theorem OAI.EilenbergGanea.LevelTransport.triangle_of_short line 187

    Source documentation

    Six compatible generator pieces around a level triangle lie in one flat chart once the three edge images are uniformly short.

    theorem triangle_of_short (hf : FlatConnection L h) (hQ : GeneralPosition h Q)
        (b c d u v w : TrianglePoint V) (δ : ℝ) (hδ : 0 < δ)
        (hsmall : 4 * δ < 1 / (Fintype.card V + 1 : ℝ))
        (hb : CliquePoint L b) (hc : CliquePoint L c) (hd : CliquePoint L d)
        (hu : CliquePoint L u) (hv : CliquePoint L v) (hw : CliquePoint L w)
        (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)
        (dbu : dist b u ≤ δ) (duc : dist u c ≤ δ)
        (dcv : dist c v ≤ δ) (dvd : dist v d ≤ δ)
        (_ddw : dist d w ≤ δ) (dwb : dist w b ≤ δ) :
        edgeTransport h Q b u c * edgeTransport h Q c v d * edgeTransport h Q d w b = 1 := by
    …

19. theorem OAI.EilenbergGanea.LevelTransport.edgeLabel_triangle line 214

    Source documentation

    Every oriented three-edge loop with these actual level endpoints is flat. In particular both kinds of sections of a three-cube are covered.

    theorem edgeLabel_triangle (hf : FlatConnection L h) (hQ : GeneralPosition h Q)
        (N : ℕ) (hN : 1 < N) (hsize : 8 / (N : ℝ) < 1 / (Fintype.card V + 1 : ℝ))
        (g₀ g₁ g₂ : NegativeLevel L N) (q₀ r₀ q₁ r₁ q₂ r₂ : V)
        (e₀ : edgeVertex L N g₀ q₀ r₀ = g₁)
        (e₁ : edgeVertex L N g₁ q₁ r₁ = g₂)
        (e₂ : edgeVertex L N g₂ q₂ r₂ = g₀) :
        edgeLabel L hdim h Q N hN g₀ q₀ r₀ *
          edgeLabel L hdim h Q N hN g₁ q₁ r₁ *
          edgeLabel L hdim h Q N hN g₂ q₂ r₂ = 1 := by
    …

    Mentions: OAI.EilenbergGanea.LevelTransport.NegativeLevel, OAI.EilenbergGanea.LevelTransport.edgeVertex, OAI.EilenbergGanea.LevelTransport.edgeLabel

20. def OAI.EilenbergGanea.LevelTransport.vertexPoint line 258

    Source documentation

    A vertex of the simplex is also an honest point of its two-skeleton.

    def vertexPoint (v : V) : TrianglePoint V :=
    …

21. theorem OAI.EilenbergGanea.LevelTransport.vertexPoint_val line 268
22. theorem OAI.EilenbergGanea.LevelTransport.star_vertex line 271
23. theorem OAI.EilenbergGanea.LevelTransport.negative_powers_upper line 277
24. theorem OAI.EilenbergGanea.LevelTransport.powersPoint_star line 291

    Source documentation

    Negative commuting powers remain exactly in their two-coordinate face.

    theorem powersPoint_star {q r : V} (hqr : L.Adj q r) (n m : ℕ)
        (hg : 0 < traceLength L (artinNormalTrace L
          ((artinGenerator L q)⁻¹ ^ n * (artinGenerator L r)⁻¹ ^ m))) :
        Star L q (point L hdim ((artinGenerator L q)⁻¹ ^ n * (artinGenerator L r)⁻¹ ^ m) hg) := by
    …

    Mentions: OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.LevelTransport.point

25. theorem OAI.EilenbergGanea.LevelTransport.powersPoint_first line 306

    Source documentation

    Constant endpoint in the q-direction, stated with a concrete positive height.

    theorem powersPoint_first {q r : V} (hqr : L.Adj q r) (N : ℕ) (hN : 0 < N)
        (hg : 0 < traceLength L (artinNormalTrace L
          ((artinGenerator L q)⁻¹ ^ N * (artinGenerator L r)⁻¹ ^ 0))) :
        point L hdim ((artinGenerator L q)⁻¹ ^ N * (artinGenerator L r)⁻¹ ^ 0) hg =
          vertexPoint q := by
    …

    Mentions: OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.LevelTransport.point, OAI.EilenbergGanea.LevelTransport.vertexPoint

26. theorem OAI.EilenbergGanea.LevelTransport.powersPoint_last line 317
27. def OAI.EilenbergGanea.LevelTransport.powerVertex line 328
28. theorem OAI.EilenbergGanea.LevelTransport.powerVertex_step line 337
29. theorem OAI.EilenbergGanea.LevelTransport.powerVertex_upper line 347
30. theorem OAI.EilenbergGanea.LevelTransport.powerVertex_star line 356
31. theorem OAI.EilenbergGanea.LevelTransport.powerVertex_upper_star line 360
32. theorem OAI.EilenbergGanea.LevelTransport.powerLabel_chart line 369
33. inductive OAI.EilenbergGanea.LevelTransport.Walk line 386

    Source documentation

    Directed walks retain the chosen generator pair, including parallel edges.

    inductive Walk (N : ℕ) : NegativeLevel L N → NegativeLevel L N → Type _
      | nil (g : NegativeLevel L N) : Walk N g g
      | cons {g k : NegativeLevel L N} (q r : V) (hqr : L.Adj q r)
          (p : Walk N (edgeVertex L N g q r) k) : Walk N g k
    
    namespace Walk
    variable {L} {N : ℕ}

    Mentions: OAI.EilenbergGanea.LevelTransport.NegativeLevel, OAI.EilenbergGanea.LevelTransport.edgeVertex

34. def OAI.EilenbergGanea.LevelTransport.Walk.append line 394
35. def OAI.EilenbergGanea.LevelTransport.Walk.cast line 398
36. def OAI.EilenbergGanea.LevelTransport.walkProduct line 403
37. theorem OAI.EilenbergGanea.LevelTransport.walkProduct_nil line 407
38. theorem OAI.EilenbergGanea.LevelTransport.walkProduct_cons line 410
39. theorem OAI.EilenbergGanea.LevelTransport.walkProduct_append line 415
40. theorem OAI.EilenbergGanea.LevelTransport.walkProduct_cast line 423
41. theorem OAI.EilenbergGanea.LevelTransport.exists_powerWalk line 429

    Source documentation

    The entire subdivided edge has the exact endpoint transport, not merely a limit.

    theorem exists_powerWalk (hf : FlatConnection L h) (hQ : GeneralPosition h Q)
        (N : ℕ) (hN : 1 < N) {q r : V} (hqr : L.Adj q r) (k : ℕ) (hk : k ≤ N) :
        ∃ p : Walk L N (powerVertex L N q r 0) (powerVertex L N q r k),
          walkProduct L hdim h Q N hN p =
            chartTransport h Q q (levelPoint L hdim N (by omega) (powerVertex L N q r 0))
              (levelPoint L hdim N (by omega) (powerVertex L N q r k)) := by
    …

    Mentions: OAI.EilenbergGanea.LevelTransport.Walk, OAI.EilenbergGanea.LevelTransport.powerVertex, OAI.EilenbergGanea.LevelTransport.walkProduct, OAI.EilenbergGanea.LevelTransport.levelPoint

42. def OAI.EilenbergGanea.LevelTransport.pureVertex line 447
43. theorem OAI.EilenbergGanea.LevelTransport.powerVertex_zero line 454
44. theorem OAI.EilenbergGanea.LevelTransport.powerVertex_last line 458
45. def OAI.EilenbergGanea.LevelTransport.vertexGauge line 461
46. theorem OAI.EilenbergGanea.LevelTransport.levelPoint_power_zero line 463
47. theorem OAI.EilenbergGanea.LevelTransport.levelPoint_power_last line 471
48. theorem OAI.EilenbergGanea.LevelTransport.exists_expanded_edge line 479
49. def OAI.EilenbergGanea.LevelTransport.graphWalkProduct line 494
50. theorem OAI.EilenbergGanea.LevelTransport.exists_expanded_walk line 498
51. theorem OAI.EilenbergGanea.LevelTransport.graphWalkProduct_eq_zipWith line 514
52. theorem OAI.EilenbergGanea.LevelTransport.exists_nontrivial_level_walk line 525

    Source documentation

    A nontrivial seed holonomy survives every sufficiently translated level.

    theorem exists_nontrivial_level_walk (hf : FlatConnection L h) (hQ : GeneralPosition h Q)
        (N : ℕ) (hN : 1 < N) {q : V} (w : L.Walk q q)
        (hw : graphWalkProduct L h w ≠ 1) :
        ∃ p : Walk L N (pureVertex L N q) (pureVertex L N q),
          walkProduct L hdim h Q N hN p ≠ 1 := by
    …

    Mentions: OAI.EilenbergGanea.LevelTransport.graphWalkProduct, OAI.EilenbergGanea.LevelTransport.Walk, OAI.EilenbergGanea.LevelTransport.pureVertex, OAI.EilenbergGanea.LevelTransport.walkProduct

53. def OAI.EilenbergGanea.LevelTransport.Walk.eval line 545
54. theorem OAI.EilenbergGanea.LevelTransport.walkProduct_eq_eval line 551
55. def OAI.EilenbergGanea.SourceTransport.seedWalk line 563
56. theorem OAI.EilenbergGanea.SourceTransport.seedWalk_support line 567
57. theorem OAI.EilenbergGanea.SourceTransport.seedWalk_product_ne line 570
58. theorem OAI.EilenbergGanea.SourceTransport.source_small_labels line 576

    Source documentation

    Actual small flat transport for the fixed source level graph. There are no representation, direction-map, local-chart, or nontriviality hypotheses here.

    theorem source_small_labels (ε : ℝ) (hε : 0 < ε) :
        ∃ N : ℕ, 1 < N ∧ ∃ a : NegativeLevel seedGraph N → SeedCell → SeedCell → SU2,
          (∀ g q r, a (edgeVertex seedGraph N g q r) r q = (a g q r)⁻¹) ∧
          (∀ g q r, dist (a g q r) 1 < ε) ∧
          (∀ g₀ g₁ g₂ q₀ r₀ q₁ r₁ q₂ r₂,
            edgeVertex seedGraph N g₀ q₀ r₀ = g₁ →
            edgeVertex seedGraph N g₁ q₁ r₁ = g₂ →
            edgeVertex seedGraph N g₂ q₂ r₂ = g₀ →
            a g₀ q₀ r₀ * a g₁ q₁ r₁ * a g₂ q₂ r₂ = 1) ∧
          ∃ (g : NegativeLevel seedGraph N) (p : Walk seedGraph N g g), p.eval a ≠ 1 := by
    …

    Mentions: OAI.EilenbergGanea.SeedCell, OAI.EilenbergGanea.SU2