OAI/AlgebraicTopology/Cubical/Descending.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.EilenbergGanea.DescendingCube.Data line 20

   Source documentation

   Finite descending directions with literal word-length decrease. These combinatorial fields will be supplied by the checked Artin trace normal form.

   structure Data (f : A → G) where
   …

2. def OAI.EilenbergGanea.DescendingCube.Data.product line 31
3. theorem OAI.EilenbergGanea.DescendingCube.Data.product_empty line 34
4. theorem OAI.EilenbergGanea.DescendingCube.Data.product_insert line 37
5. theorem OAI.EilenbergGanea.DescendingCube.Data.product_descent line 43

   Source documentation

   Simultaneous finite descent and preservation of all untouched directions.

   theorem product_descent (g : G) (s : Finset A) (hs : s ⊆ D.desc g) :
       D.length (g * D.product g s hs) + s.card = D.length g ∧
       ∀ a ∈ D.desc g, a ∉ s → a ∈ D.desc (g * D.product g s hs) := by
   …

6. structure OAI.EilenbergGanea.DescendingCube.Data.Cell line 68
7. structure OAI.EilenbergGanea.DescendingCube.Data.Point line 73
8. abbrev OAI.EilenbergGanea.DescendingCube.Data.Coordinates line 80
9. def OAI.EilenbergGanea.DescendingCube.Data.ones line 82
10. theorem OAI.EilenbergGanea.DescendingCube.Data.mem_ones line 85
11. theorem OAI.EilenbergGanea.DescendingCube.Data.ones_subset line 88
12. def OAI.EilenbergGanea.DescendingCube.Data.normalizedCoord line 92
13. def OAI.EilenbergGanea.DescendingCube.Data.characteristic line 96

    Source documentation

    Crossing a far face removes a descent and strictly lowers the top vertex.

    def characteristic (c : D.Cell) (x : D.Coordinates c) : D.Point where
    …

14. def OAI.EilenbergGanea.DescendingCube.Data.active line 127
15. theorem OAI.EilenbergGanea.DescendingCube.Data.mem_active line 129
16. def OAI.EilenbergGanea.DescendingCube.Data.pointCell line 132
17. def OAI.EilenbergGanea.DescendingCube.Data.pointCoordinates line 135
18. theorem OAI.EilenbergGanea.DescendingCube.Data.ones_pointCoordinates line 138
19. theorem OAI.EilenbergGanea.DescendingCube.Data.characteristic_point line 145
20. abbrev OAI.EilenbergGanea.DescendingCube.Data.CubeSum line 155
21. def OAI.EilenbergGanea.DescendingCube.Data.evaluation line 157
22. theorem OAI.EilenbergGanea.DescendingCube.Data.evaluation_surjective line 159
23. instance OAI.EilenbergGanea.DescendingCube.Data.pointTopology line 163
24. theorem OAI.EilenbergGanea.DescendingCube.Data.evaluation_quotient line 166
25. theorem OAI.EilenbergGanea.DescendingCube.Data.characteristic_continuous line 168
26. theorem OAI.EilenbergGanea.DescendingCube.Data.characteristic_length line 172
27. def OAI.EilenbergGanea.DescendingCube.Data.fullCell line 183
28. def OAI.EilenbergGanea.DescendingCube.Data.fullCoord line 185
29. theorem OAI.EilenbergGanea.DescendingCube.Data.fullCoord_mem line 188
30. theorem OAI.EilenbergGanea.DescendingCube.Data.fullCoord_nonneg line 191
31. theorem OAI.EilenbergGanea.DescendingCube.Data.fullCoord_le_one line 198
32. theorem OAI.EilenbergGanea.DescendingCube.Data.fullCoord_continuous line 205
33. def OAI.EilenbergGanea.DescendingCube.Data.extendCoordinates line 211
34. theorem OAI.EilenbergGanea.DescendingCube.Data.ones_extend line 214
35. theorem OAI.EilenbergGanea.DescendingCube.Data.characteristic_extend line 226
36. def OAI.EilenbergGanea.DescendingCube.Data.radius line 241
37. theorem OAI.EilenbergGanea.DescendingCube.Data.radius_continuous line 243
38. theorem OAI.EilenbergGanea.DescendingCube.Data.le_radius line 246
39. theorem OAI.EilenbergGanea.DescendingCube.Data.radius_le line 249
40. theorem OAI.EilenbergGanea.DescendingCube.Data.radius_lt line 252
41. theorem OAI.EilenbergGanea.DescendingCube.Data.radius_nonneg line 255
42. theorem OAI.EilenbergGanea.DescendingCube.Data.radius_eq_one_iff line 258
43. def OAI.EilenbergGanea.DescendingCube.Data.deformCoordinates line 276
44. theorem OAI.EilenbergGanea.DescendingCube.Data.deformCoordinates_continuous line 286
45. theorem OAI.EilenbergGanea.DescendingCube.Data.deformCoordinates_zero line 296
46. theorem OAI.EilenbergGanea.DescendingCube.Data.deformCoordinates_fixed line 302
47. theorem OAI.EilenbergGanea.DescendingCube.Data.deformCoordinates_one_ones line 312

    Source documentation

    The time-one radial deformation reaches a far face whenever the top is not the identity. It is fixed on every far face from the outset.

    theorem deformCoordinates_one_ones (c : D.Cell) (x : D.Coordinates c)
        (hc : 0 < D.length c.top) :
        (D.ones (D.fullCell c.top) (D.deformCoordinates c x 1)).Nonempty := by
    …

48. def OAI.EilenbergGanea.DescendingCube.Data.cellDeform line 335
49. theorem OAI.EilenbergGanea.DescendingCube.Data.cellDeform_continuous line 338
50. theorem OAI.EilenbergGanea.DescendingCube.Data.cellDeform_zero line 342
51. theorem OAI.EilenbergGanea.DescendingCube.Data.cellDeform_fixed line 346
52. theorem OAI.EilenbergGanea.DescendingCube.Data.cellDeform_one_length line 350
53. def OAI.EilenbergGanea.DescendingCube.Data.farFaceCell line 361
54. def OAI.EilenbergGanea.DescendingCube.Data.farFaceCoordinates line 369
55. theorem OAI.EilenbergGanea.DescendingCube.Data.farFaceCoordinates_continuous line 372
56. theorem OAI.EilenbergGanea.DescendingCube.Data.ones_farFace line 378
57. theorem OAI.EilenbergGanea.DescendingCube.Data.characteristic_farFace line 392
58. theorem OAI.EilenbergGanea.DescendingCube.Data.farFaceCell_length line 424
59. theorem OAI.EilenbergGanea.DescendingCube.Data.fullCoord_point line 430
60. theorem OAI.EilenbergGanea.DescendingCube.Data.characteristic_top_of_ones_empty line 438
61. theorem OAI.EilenbergGanea.DescendingCube.Data.characteristic_coord_of_ones_empty line 444
62. def OAI.EilenbergGanea.DescendingCube.Data.pointDeform line 460
63. theorem OAI.EilenbergGanea.DescendingCube.Data.pointDeform_zero line 463
64. theorem OAI.EilenbergGanea.DescendingCube.Data.pointDeform_one_length line 466
65. theorem OAI.EilenbergGanea.DescendingCube.Data.cellDeform_congr line 470
66. theorem OAI.EilenbergGanea.DescendingCube.Data.pointDeform_characteristic line 487

    Source documentation

    On the open part of a cube, radial deformation in its full descending cube is independent of which zero coordinates were omitted.

    theorem pointDeform_characteristic (c : D.Cell) (x : D.Coordinates c) (t : unitInterval)
        (hx : D.ones c x = ∅) : D.pointDeform (D.characteristic c x) t = D.cellDeform c x t := by
    …

67. def OAI.EilenbergGanea.DescendingCube.Data.clip line 499
68. theorem OAI.EilenbergGanea.DescendingCube.Data.clip_continuous line 501
69. theorem OAI.EilenbergGanea.DescendingCube.Data.clip_zero line 503
70. theorem OAI.EilenbergGanea.DescendingCube.Data.clip_one line 507
71. def OAI.EilenbergGanea.DescendingCube.Data.flow line 512

    Source documentation

    Flow to word-length height r, stopping part-way across its unique top shell.

    def flow (r : ℝ≥0) (p : D.Point) : D.Point :=
    …

72. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_fixed line 526
73. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_partial line 529
74. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_lower line 537
75. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_characteristic_high line 559
76. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_characteristic_low line 577
77. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_cell_zero_continuous line 585
78. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_cell_boundary_continuous line 598
79. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_cell_glue_continuous line 631
80. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_cell_continuous line 662
81. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_continuous line 678
82. def OAI.EilenbergGanea.DescendingCube.Data.origin line 688
83. theorem OAI.EilenbergGanea.DescendingCube.Data.point_eq_origin_of_length_zero line 696
84. theorem OAI.EilenbergGanea.DescendingCube.Data.flow_zero line 706
85. def OAI.EilenbergGanea.DescendingCube.Data.contraction line 725
86. theorem OAI.EilenbergGanea.DescendingCube.Data.contraction_zero line 728
87. theorem OAI.EilenbergGanea.DescendingCube.Data.contraction_one line 731
88. theorem OAI.EilenbergGanea.DescendingCube.Data.heightTime_large line 734
89. theorem OAI.EilenbergGanea.DescendingCube.Data.contraction_cell_eventually_zero line 743
90. theorem OAI.EilenbergGanea.DescendingCube.Data.contraction_cell_continuous line 763
91. theorem OAI.EilenbergGanea.DescendingCube.Data.contraction_continuous line 785
92. theorem OAI.EilenbergGanea.DescendingCube.Data.contractibleSpace line 796

    Source documentation

    Direct radial-shell contraction; no cellular homology or Whitehead theorem is used.

    theorem contractibleSpace : ContractibleSpace D.Point := by
    …