OAI/AlgebraicTopology/Cubical/PathChains.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.EilenbergGanea.PathTransport.Local line 16
2. def OAI.EilenbergGanea.PathTransport.Local.fold line 26
3. def OAI.EilenbergGanea.PathTransport.Local.Good₁ line 30
4. def OAI.EilenbergGanea.PathTransport.Local.Good₂ line 32
5. theorem OAI.EilenbergGanea.PathTransport.Local.small_comp line 36
6. theorem OAI.EilenbergGanea.PathTransport.Local.good₁_zero line 45
7. theorem OAI.EilenbergGanea.PathTransport.Local.good₂_zero line 49
8. theorem OAI.EilenbergGanea.PathTransport.Local.good₁_cut line 54
9. theorem OAI.EilenbergGanea.PathTransport.Local.good₂_cut line 68
10. theorem OAI.EilenbergGanea.PathTransport.Local.fold_small line 80
11. theorem OAI.EilenbergGanea.PathTransport.Local.fold_stable line 88
12. theorem OAI.EilenbergGanea.PathTransport.Local.good₁_eventually line 102
13. theorem OAI.EilenbergGanea.PathTransport.Local.good₂_eventually line 107
14. def OAI.EilenbergGanea.PathTransport.Local.depth line 113
15. theorem OAI.EilenbergGanea.PathTransport.Local.depth_good line 115
16. def OAI.EilenbergGanea.PathTransport.Local.transport line 118
17. theorem OAI.EilenbergGanea.PathTransport.Local.transport_eq_fold line 120
18. theorem OAI.EilenbergGanea.PathTransport.Local.transport_small line 126
19. theorem OAI.EilenbergGanea.PathTransport.Local.transport_const line 129
20. theorem OAI.EilenbergGanea.PathTransport.Local.four_squares line 138
21. theorem OAI.EilenbergGanea.PathTransport.Local.fold_square line 152
22. theorem OAI.EilenbergGanea.PathTransport.Local.transport_square line 165
23. theorem OAI.EilenbergGanea.PathTransport.Local.good₁_mono line 188
24. theorem OAI.EilenbergGanea.PathTransport.Local.transport_split line 197
25. theorem OAI.EilenbergGanea.PathTransport.Local.cut_trans_left line 207
26. theorem OAI.EilenbergGanea.PathTransport.Local.cut_trans_right line 219
27. theorem OAI.EilenbergGanea.PathTransport.Local.transport_trans line 230
28. theorem OAI.EilenbergGanea.PathTransport.Local.transport_homotopy line 235
29. def OAI.EilenbergGanea.PathTransport.Local.quotientTransport line 245
30. theorem OAI.EilenbergGanea.PathTransport.Local.quotientTransport_mk line 249
31. theorem OAI.EilenbergGanea.PathTransport.Local.quotientTransport_refl line 253
32. theorem OAI.EilenbergGanea.PathTransport.Local.quotientTransport_trans line 256
33. def OAI.EilenbergGanea.PathTransport.Local.fundamentalHom line 266

    Source documentation

    Traversal-order labels are a homomorphism to the opposite, because Mathlib's fundamental group multiplication is categorical (right path first).

    def fundamentalHom (x : X) : FundamentalGroup X x →* Gᵐᵒᵖ where
    …

34. theorem OAI.EilenbergGanea.PathTransport.Local.transport_unique line 274

    Source documentation

    Any multiplicative global path label is completely determined on a sufficiently small open-cover mesh. This is the uniqueness half of low-dimensional descent.

    theorem transport_unique (v : Cube₁ X → G)
        (hsplit : ∀ γ, v γ = v (cut₁ γ false) * v (cut₁ γ true))
        (hsmall : ∀ γ ∈ CubicalMesh.small U, v γ = l.value γ) (γ : Cube₁ X) :
        v γ = l.transport hU hcover γ := by
    …

    Mentions: OAI.EilenbergGanea.CubicalMesh.small

35. abbrev OAI.EilenbergGanea.PathTransport.PQ line 295
36. def OAI.EilenbergGanea.PathTransport.cubePath line 297
37. abbrev OAI.EilenbergGanea.PathTransport.asClass line 298
38. def OAI.EilenbergGanea.PathTransport.based line 300
39. theorem OAI.EilenbergGanea.PathTransport.based_trans line 303
40. theorem OAI.EilenbergGanea.PathTransport.based_refl line 313
41. def OAI.EilenbergGanea.PathTransport.basedPath line 320
42. theorem OAI.EilenbergGanea.PathTransport.basedPath_congr line 323
43. theorem OAI.EilenbergGanea.PathTransport.basedPath_homotopic line 331
44. theorem OAI.EilenbergGanea.PathTransport.basedPath_trans line 335
45. theorem OAI.EilenbergGanea.PathTransport.basedPath_refl line 338
46. def OAI.EilenbergGanea.PathTransport.holonomy line 340
47. theorem OAI.EilenbergGanea.PathTransport.holonomy_path line 343
48. theorem OAI.EilenbergGanea.PathTransport.holonomy_const line 345
49. def OAI.EilenbergGanea.PathTransport.halfPath₀ line 348
50. def OAI.EilenbergGanea.PathTransport.halfPath₁ line 349
51. theorem OAI.EilenbergGanea.PathTransport.holonomy_split line 351
52. def OAI.EilenbergGanea.PathTransport.bottom line 363
53. def OAI.EilenbergGanea.PathTransport.rightSide line 364
54. def OAI.EilenbergGanea.PathTransport.leftSide line 365
55. def OAI.EilenbergGanea.PathTransport.topSide line 366
56. theorem OAI.EilenbergGanea.PathTransport.square_paths line 368
57. theorem OAI.EilenbergGanea.PathTransport.holonomy_square line 374
58. def OAI.EilenbergGanea.PathTransport.holonomyLocal line 387

    Source documentation

    Actual based-loop holonomy is flat; this is derived from square homotopy in I², rather than supplied as a geometric assumption.

    def holonomyLocal {r : X} (q : ∀ x, Path r x) (U : Set (Set X)) :
        Local (G:=(FundamentalGroup X r)ᵐᵒᵖ) U where
    …

    Mentions: OAI.EilenbergGanea.PathTransport.Local

59. theorem OAI.EilenbergGanea.CubicalSingular.mayerVietoris_injective line 400

    Source documentation

    Low-dimensional Mayer–Vietoris injectivity, derived by subdivision.

    theorem mayerVietoris_injective [ContractibleSpace X]
        (U V : Set X) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = univ)
        {z : N₁ X} (hz : z ∈ L₁ (U ∩ V))
        {a b : N₂ X} (ha : a ∈ L₂ U) (hb : b ∈ L₂ V) (hda : d₂ a = z) (hdb : d₂ b = z) :
        ∃ c ∈ L₂ (U ∩ V), d₂ c = z := by
    …

    Mentions: OAI.EilenbergGanea.CubicalSingular.N₁, OAI.EilenbergGanea.CubicalSingular.L₁, OAI.EilenbergGanea.CubicalSingular.N₂, OAI.EilenbergGanea.CubicalSingular.L₂, OAI.EilenbergGanea.CubicalSingular.d₂

60. theorem OAI.EilenbergGanea.CubicalSingular.mayerVietoris_surjective line 432

    Source documentation

    The other half of the same exact sequence, with literal supported chains.

    theorem mayerVietoris_surjective [ContractibleSpace X]
        (U V : Set X) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = univ)
        {z : N₁ X} (hzU : z ∈ L₁ U) (hz : d₁ z = 0) :
        ∃ t ∈ L₁ (U ∩ V), d₁ t = 0 ∧
          (∃ b ∈ L₂ U, d₂ b = t-z) ∧ (∃ b ∈ L₂ V, d₂ b = t) := by
    …

    Mentions: OAI.EilenbergGanea.CubicalSingular.N₁, OAI.EilenbergGanea.CubicalSingular.L₁, OAI.EilenbergGanea.CubicalSingular.d₁, OAI.EilenbergGanea.CubicalSingular.L₂, OAI.EilenbergGanea.CubicalSingular.d₂

61. def OAI.EilenbergGanea.CubicalSingular.cyclesOn line 454

    Source documentation

    Cycles and boundaries are actual submodules of normalized singular chains.

    def cyclesOn (U : Set X) : Submodule ℤ (N₁ X) := L₁ U ⊓ LinearMap.ker d₁

    Mentions: OAI.EilenbergGanea.CubicalSingular.N₁, OAI.EilenbergGanea.CubicalSingular.L₁, OAI.EilenbergGanea.CubicalSingular.d₁

62. def OAI.EilenbergGanea.CubicalSingular.boundsOn line 455
63. theorem OAI.EilenbergGanea.CubicalSingular.boundsOn_le_cyclesOn line 457
64. def OAI.EilenbergGanea.CubicalSingular.boundaries line 461
65. abbrev OAI.EilenbergGanea.CubicalSingular.Homology₁ line 462
66. def OAI.EilenbergGanea.CubicalSingular.cycleInclusion line 464
67. theorem OAI.EilenbergGanea.CubicalSingular.cycleInclusion_bounds line 467
68. def OAI.EilenbergGanea.CubicalSingular.homologyInclusion line 472
69. theorem OAI.EilenbergGanea.CubicalSingular.homologyInclusion_injective line 475
70. theorem OAI.EilenbergGanea.CubicalSingular.homologyInclusion_surjective line 491
71. def OAI.EilenbergGanea.CubicalSingular.mayerVietoris_equiv line 505

    Source documentation

    No cellular theorem is assumed: this is the comparison for actual open sets in an actually contractible space, proved by finite singular subdivision.

    def mayerVietoris_equiv [ContractibleSpace X]
        (U V : Set X) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = univ)
        (hVex : ∀ z : N₁ X, z ∈ L₁ V → d₁ z = 0 → ∃ b ∈ L₂ V, d₂ b = z) :
        Homology₁ (U ∩ V) ≃ₗ[ℤ] Homology₁ U :=
    …

    Mentions: OAI.EilenbergGanea.CubicalSingular.N₁, OAI.EilenbergGanea.CubicalSingular.L₁, OAI.EilenbergGanea.CubicalSingular.d₁, OAI.EilenbergGanea.CubicalSingular.L₂, OAI.EilenbergGanea.CubicalSingular.d₂, OAI.EilenbergGanea.CubicalSingular.Homology₁

72. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_mapsTo line 518
73. theorem OAI.EilenbergGanea.CubicalSingular.pushN₂_mapsTo line 528
74. theorem OAI.EilenbergGanea.CubicalSingular.L₁_univ line 538
75. theorem OAI.EilenbergGanea.CubicalSingular.L₂_univ line 541
76. def OAI.EilenbergGanea.CubicalSingular.cycleMap line 545
77. theorem OAI.EilenbergGanea.CubicalSingular.cycleMap_bounds line 551
78. def OAI.EilenbergGanea.CubicalSingular.homologyMap line 557
79. theorem OAI.EilenbergGanea.CubicalSingular.homologyMap_mk line 561
80. def OAI.EilenbergGanea.CubicalSingular.normalizedPrism line 565
81. theorem OAI.EilenbergGanea.CubicalSingular.normalizedPrism_mk line 570
82. theorem OAI.EilenbergGanea.CubicalSingular.normalizedPrism_boundary line 573
83. theorem OAI.EilenbergGanea.CubicalSingular.normalizedPrism_support line 584
84. theorem OAI.EilenbergGanea.CubicalSingular.homologyMap_homotopic line 594
85. theorem OAI.EilenbergGanea.CubicalSingular.homologyMap_id line 609
86. theorem OAI.EilenbergGanea.CubicalSingular.homologyMap_comp line 618
87. abbrev OAI.EilenbergGanea.CubicalSingular.HomologyOne line 629
88. def OAI.EilenbergGanea.CubicalSingular.homologyOneMap line 630
89. theorem OAI.EilenbergGanea.CubicalSingular.homologyOneMap_id line 631
90. theorem OAI.EilenbergGanea.CubicalSingular.homologyOneMap_comp line 632
91. theorem OAI.EilenbergGanea.CubicalSingular.homologyOneMap_homotopic line 635
92. def OAI.EilenbergGanea.CubicalSingular.homologyOneEquiv line 639

    Source documentation

    Actual homotopy equivalences induce integral cubical H1 isomorphisms.

    def homologyOneEquiv (f : C(X,Y)) (g : C(Y,X))
        (Hgf : (g.comp f).Homotopy (ContinuousMap.id X))
        (Hfg : (f.comp g).Homotopy (ContinuousMap.id Y)) : HomologyOne X ≃ₗ[ℤ] HomologyOne Y :=
    …

    Mentions: OAI.EilenbergGanea.CubicalSingular.HomologyOne

93. abbrev OAI.EilenbergGanea.CubicalSingular.PathChains line 652
94. def OAI.EilenbergGanea.CubicalSingular.chainClass line 653
95. def OAI.EilenbergGanea.CubicalSingular.pathClass line 654
96. theorem OAI.EilenbergGanea.CubicalSingular.chainClass_boundary line 656
97. theorem OAI.EilenbergGanea.CubicalSingular.gen₁_const line 658
98. theorem OAI.EilenbergGanea.CubicalSingular.pathClass_refl line 660
99. theorem OAI.EilenbergGanea.CubicalSingular.chainClass_subdivision line 664
100. theorem OAI.EilenbergGanea.CubicalSingular.pathClass_trans line 669
101. theorem OAI.EilenbergGanea.CubicalSingular.pathClass_homotopy line 677
102. def OAI.EilenbergGanea.CubicalSingular.quotientPathClass line 691
103. theorem OAI.EilenbergGanea.CubicalSingular.quotientPathClass_mk line 693
104. theorem OAI.EilenbergGanea.CubicalSingular.quotientPathClass_trans line 695
105. theorem OAI.EilenbergGanea.CubicalSingular.quotientPathClass_refl line 700
106. theorem OAI.EilenbergGanea.CubicalSingular.quotientPathClass_symm line 702
107. def OAI.EilenbergGanea.CubicalSingular.loopChainHom line 708
108. abbrev OAI.EilenbergGanea.CubicalSingular.AbLoops line 713
109. def OAI.EilenbergGanea.CubicalSingular.loopToChains line 715
110. theorem OAI.EilenbergGanea.CubicalSingular.loopToChains_of line 718
111. def OAI.EilenbergGanea.CubicalSingular.abHolonomy line 721
112. theorem OAI.EilenbergGanea.CubicalSingular.abHolonomy_const line 723
113. def OAI.EilenbergGanea.CubicalSingular.abHolonomyRaw line 727
114. def OAI.EilenbergGanea.CubicalSingular.abHolonomyMap line 730
115. theorem OAI.EilenbergGanea.CubicalSingular.abHolonomyMap_gen line 736
116. theorem OAI.EilenbergGanea.CubicalSingular.abHolonomy_square line 739
117. theorem OAI.EilenbergGanea.CubicalSingular.abHolonomyMap_boundary line 746
118. def OAI.EilenbergGanea.CubicalSingular.chainsToLoops line 766
119. theorem OAI.EilenbergGanea.CubicalSingular.chainsToLoops_class line 770
120. theorem OAI.EilenbergGanea.CubicalSingular.chainsToLoops_path line 772
121. theorem OAI.EilenbergGanea.CubicalSingular.quotientPathClass_based line 781
122. def OAI.EilenbergGanea.CubicalSingular.anchorChains line 785
123. theorem OAI.EilenbergGanea.CubicalSingular.loopToChains_abHolonomy line 788
124. theorem OAI.EilenbergGanea.CubicalSingular.loops_chains_identity line 797
125. theorem OAI.EilenbergGanea.CubicalSingular.ab_based_loop line 812
126. theorem OAI.EilenbergGanea.CubicalSingular.chains_loops_identity line 820
127. def OAI.EilenbergGanea.CubicalSingular.homologyChainsMap line 840
128. theorem OAI.EilenbergGanea.CubicalSingular.homologyChainsMap_mk line 846
129. theorem OAI.EilenbergGanea.CubicalSingular.homologyChainsMap_injective line 849
130. def OAI.EilenbergGanea.CubicalSingular.homologyToLoops line 860
131. theorem OAI.EilenbergGanea.CubicalSingular.homologyToLoops_injective line 863
132. theorem OAI.EilenbergGanea.CubicalSingular.homologyToLoops_surjective line 874
133. def OAI.EilenbergGanea.CubicalSingular.hurewiczOne line 895

     Source documentation

     Integral degree-one Hurewicz for actual paths, with no cellular hypothesis: finite singular 1-cycles equal the abelianized topological fundamental group.

     def hurewiczOne {r : X} (q : ∀ x, Path r x) : HomologyOne X ≃ₗ[ℤ] AbLoops X r :=
     …

     Mentions: OAI.EilenbergGanea.CubicalSingular.HomologyOne, OAI.EilenbergGanea.CubicalSingular.AbLoops