OAI/AlgebraicTopology/CWComplex/CellularPaths.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EilenbergGanea.CubicalSingular.homologyOneMap_const line 14
2. def OAI.EilenbergGanea.CubicalSingular.fiberInclusion line 26
3. def OAI.EilenbergGanea.CubicalSingular.fiberProjection line 27
4. theorem OAI.EilenbergGanea.CubicalSingular.fiberProjection_inclusion line 36
5. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_fiber_cube line 42
6. def OAI.EilenbergGanea.CubicalSingular.sigmaHomologyBasisMap line 71
7. theorem OAI.EilenbergGanea.CubicalSingular.sigmaHomologyBasis_coeff line 74
8. theorem OAI.EilenbergGanea.CubicalSingular.sigmaHomologyBasis_injective line 88
9. theorem OAI.EilenbergGanea.CubicalSingular.finite_fiber_decomposition line 93
10. theorem OAI.EilenbergGanea.CubicalSingular.sigmaHomologyBasis_surjective line 117
11. def OAI.EilenbergGanea.CubicalSingular.sigmaHomologyBasis line 144

    Source documentation

    The integral H1 basis of an arbitrary disjoint union of copies of a space with H1=Z; all chains and decompositions have genuinely finite support.

    def sigmaHomologyBasis : (J →₀ ℤ) ≃ₗ[ℤ] HomologyOne (Σ _ : J,Y) :=
    …

    Mentions: OAI.EilenbergGanea.CubicalSingular.HomologyOne

12. structure OAI.EilenbergGanea.PathTransport.TwoPotential line 154
13. def OAI.EilenbergGanea.PathTransport.TwoPotential.value line 163
14. theorem OAI.EilenbergGanea.PathTransport.TwoPotential.value_left line 166
15. theorem OAI.EilenbergGanea.PathTransport.TwoPotential.value_right line 169
16. theorem OAI.EilenbergGanea.PathTransport.TwoPotential.value_const line 176
17. theorem OAI.EilenbergGanea.PathTransport.TwoPotential.small_either line 180
18. def OAI.EilenbergGanea.PathTransport.TwoPotential.system line 188
19. theorem OAI.EilenbergGanea.PathTransport.TwoPotential.cover_open line 218
20. theorem OAI.EilenbergGanea.PathTransport.TwoPotential.cover_univ line 224
21. def OAI.EilenbergGanea.PathTransport.TwoPotential.transport line 227
22. theorem OAI.EilenbergGanea.PathTransport.TwoPotential.transport_left line 230
23. theorem OAI.EilenbergGanea.PathTransport.TwoPotential.transport_right line 236
24. def OAI.EilenbergGanea.ForestCover.ThinPaths line 250

    Source documentation

    Every path component is simply connected; no connectedness is imposed.

    def ThinPaths (Y : Type*) [TopologicalSpace Y] : Prop :=
    …

25. def OAI.EilenbergGanea.ForestCover.componentRoot line 253
26. def OAI.EilenbergGanea.ForestCover.componentStem line 255
27. theorem OAI.EilenbergGanea.ForestCover.componentRoot_eq line 258
28. def OAI.EilenbergGanea.ForestCover.potential line 263
29. theorem OAI.EilenbergGanea.ForestCover.potential_path line 266
30. def OAI.EilenbergGanea.ForestCover.inclusion line 280
31. def OAI.EilenbergGanea.ForestCover.gauge line 282
32. def OAI.EilenbergGanea.ForestCover.overlapValue line 286
33. theorem OAI.EilenbergGanea.ForestCover.overlapValue_path line 290
34. def OAI.EilenbergGanea.ForestCover.evaluation line 306
35. def OAI.EilenbergGanea.ForestCover.rightLabel line 310
36. theorem OAI.EilenbergGanea.ForestCover.rightLabel_overlap line 313
37. def OAI.EilenbergGanea.ForestCover.labels line 316
38. def OAI.EilenbergGanea.PathTransport.liftCube line 336
39. structure OAI.EilenbergGanea.PathTransport.LeftPotential line 339
40. def OAI.EilenbergGanea.PathTransport.LeftPotential.value line 348
41. theorem OAI.EilenbergGanea.PathTransport.LeftPotential.value_left line 351
42. theorem OAI.EilenbergGanea.PathTransport.LeftPotential.value_right line 354
43. def OAI.EilenbergGanea.PathTransport.LeftPotential.system line 361
44. theorem OAI.EilenbergGanea.PathTransport.LeftPotential.transport_left line 397
45. theorem OAI.EilenbergGanea.PathTransport.basedPath_symm line 405
46. def OAI.EilenbergGanea.PathTransport.capInclusion line 413
47. def OAI.EilenbergGanea.PathTransport.KillsOverlap line 415
48. theorem OAI.EilenbergGanea.PathTransport.overlap_potential_path line 417
49. def OAI.EilenbergGanea.PathTransport.overlapPotential line 432
50. theorem OAI.EilenbergGanea.PathTransport.overlapPotential_cap line 435
51. def OAI.EilenbergGanea.PathTransport.patched line 438
52. theorem OAI.EilenbergGanea.PathTransport.kernel_killed line 447

    Source documentation

    The actual finite-grid van-Kampen kernel inclusion, obtained by extending all representations annihilating overlap loops. No presentation axiom is used.

    theorem kernel_killed (hU : IsOpen U) (hV : IsOpen V) (hc : U ∪ V = univ)
        (hk : KillsOverlap (V:=V) q ρ) (p : Path r r)
    …

    Mentions: OAI.EilenbergGanea.PathTransport.KillsOverlap

53. def OAI.EilenbergGanea.PathTransport.basedHom line 468
54. theorem OAI.EilenbergGanea.PathTransport.basedHom_loop line 479
55. theorem OAI.EilenbergGanea.PathTransport.kills_loops_of_root line 483

    Source documentation

    Conjugation transfers annihilation of based loops to every base point.

    theorem kills_loops_of_root [PathConnectedSpace Y] (f : C(Y,X)) (y₀ : Y)
        (ρ : (FundamentalGroup X r)ᵐᵒᵖ →* G)
        (h : ∀ p : Path y₀ y₀, ρ (basedPath q (p.map f.continuous)) = 1)
        {y : Y} (p : Path y y) : ρ (basedPath q (p.map f.continuous)) = 1 := by
    …

    Mentions: OAI.EilenbergGanea.PathTransport.basedPath

56. theorem OAI.EilenbergGanea.CWCollar.kills_annulus_loops line 502
57. theorem OAI.EilenbergGanea.PathTransport.kills_sigma_loops line 524

    Source documentation

    A loop in a disjoint union stays in one actual component.

    theorem kills_sigma_loops (f : C((Σ _ : J,Y),X)) (y₀ : Y)
        (ρ : (FundamentalGroup X r)ᵐᵒᵖ →* G)
        (hk : ∀ (j : J) (y : Y) (p : Path y y),
          ρ (basedPath q (p.map (f.comp (fiberInclusion j)).continuous)) = 1)
        {z : (Σ _ : J,Y)} (p : Path z z) : ρ (basedPath q (p.map f.continuous)) = 1 := by
    …

    Mentions: OAI.EilenbergGanea.PathTransport.basedPath

58. theorem OAI.EilenbergGanea.PathTransport.map_basedPath_eq_one line 548

    Source documentation

    A loop which becomes null after a map also has trivial based holonomy.

    theorem map_basedPath_eq_one (f : C(X,Y)) {x : X} (p : Path x x)
        (hp : (p.map f.continuous).Homotopic (Path.refl (f x))) :
        (FundamentalGroup.map f r).op (basedPath q p) = 1 := by
    …

    Mentions: OAI.EilenbergGanea.PathTransport.basedPath

59. def OAI.EilenbergGanea.CWCollar.Attachment.annulusMap line 566
60. def OAI.EilenbergGanea.CWCollar.Attachment.annulusRelator line 569
61. theorem OAI.EilenbergGanea.CWCollar.Attachment.killsOverlap_of_relators line 572
62. theorem OAI.EilenbergGanea.CWCollar.Attachment.annulus_normalClosure line 586

    Source documentation

    The exact ordinary attachment kernel, with one genuine annular relator per attached2-cell. The forward inclusion uses the finite-grid patching proof.

    theorem annulus_normalClosure (hthin : ForestCover.ThinPaths a.inner) :
        ((FundamentalGroup.map (⟨Subtype.val,continuous_subtype_val⟩ : C(a.outer,X)) r).op).ker =
          Subgroup.normalClosure (Set.range (a.annulusRelator q y₀)) := by
    …

    Mentions: OAI.EilenbergGanea.ForestCover.ThinPaths, OAI.EilenbergGanea.CWCollar.Attachment.q

63. def OAI.EilenbergGanea.CubicalSingular.sigmaCenter line 628
64. def OAI.EilenbergGanea.CubicalSingular.sigmaContraction line 630
65. def OAI.EilenbergGanea.CubicalSingular.sigmaCollapse line 634
66. def OAI.EilenbergGanea.CubicalSingular.sigmaHomotopy line 639
67. theorem OAI.EilenbergGanea.CubicalSingular.push_sigmaCollapse_zero line 653
68. theorem OAI.EilenbergGanea.CubicalSingular.exact₁_sigma_contractible line 674

    Source documentation

    Disjoint unions of contractible components have zero integral cubical H1; no finiteness of the component index is used.

    theorem exact₁_sigma_contractible [∀ j, ContractibleSpace (Y j)]
        (z : N₁ (Σ j,Y j)) (hz : d₁ z = 0) : ∃ b : N₂ (Σ j,Y j), d₂ b = z := by
    …

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

69. theorem OAI.EilenbergGanea.CubicalSingular.exact₁_on_of_exact line 685
70. theorem OAI.EilenbergGanea.CubicalSingular.exact₁_homeomorph line 698
71. def OAI.EilenbergGanea.CubicalSingular.subspaceHomologyMap line 708
72. theorem OAI.EilenbergGanea.CubicalSingular.subspaceHomologyMap_injective line 711
73. theorem OAI.EilenbergGanea.CubicalSingular.subspaceHomologyMap_surjective line 728
74. def OAI.EilenbergGanea.CubicalSingular.subspaceHomologyEquiv line 745

    Source documentation

    Supported homology is the actual singular homology of the subspace.

    def subspaceHomologyEquiv (U : Set X) : HomologyOne U ≃ₗ[ℤ] Homology₁ U :=
    …

    Mentions: OAI.EilenbergGanea.CubicalSingular.HomologyOne, OAI.EilenbergGanea.CubicalSingular.Homology₁

75. def OAI.EilenbergGanea.CWCollar.openDiskHomeomorph line 755
76. instance OAI.EilenbergGanea.CWCollar.openDiskContractible line 763
77. theorem OAI.EilenbergGanea.CWCollar.Attachment.inner_exact line 770
78. theorem OAI.EilenbergGanea.CWCollar.Attachment.inner_supported_exact line 773
79. def OAI.EilenbergGanea.CWCollar.Attachment.outerHomologyEquiv line 776
80. def OAI.EilenbergGanea.CWCollar.Attachment.attachingHomologyEquiv line 785

    Source documentation

    The top-cell collar comparison in a contractible ordinary attachment is an actual integral H1 isomorphism, proved from singular subdivision.

    def attachingHomologyEquiv [ContractibleSpace X] :
        HomologyOne (a.outer ∩ a.inner : Set X) ≃ₗ[ℤ] HomologyOne a.lower :=
    …

81. theorem OAI.EilenbergGanea.CWCollar.homologyOneMap_loop line 799
82. def OAI.EilenbergGanea.CWCollar.Attachment.outerCapHomologyEquiv line 811
83. theorem OAI.EilenbergGanea.CWCollar.Attachment.outerCapHomologyEquiv_apply line 817
84. def OAI.EilenbergGanea.CWCollar.Attachment.annularBasis line 832
85. theorem OAI.EilenbergGanea.CWCollar.Attachment.annularBasis_single line 840

    Source documentation

    Each basis vector is precisely the singular class of its lifted annulus.

    theorem annularBasis_single [ContractibleSpace X] (y₀ : Annulus 2) (j : J) :
        a.annularBasis y₀ (Finsupp.single j 1) = loopHomology ((annulusGenerator y₀).map (a.annulusMap j).continuous) := by
    …

    Mentions: OAI.EilenbergGanea.CWCollar.Annulus, OAI.EilenbergGanea.CWCollar.loopHomology, OAI.EilenbergGanea.CWCollar.annulusGenerator

86. def OAI.EilenbergGanea.PathTransport.Local.map line 859
87. theorem OAI.EilenbergGanea.PathTransport.Local.map_transport line 865
88. theorem OAI.EilenbergGanea.ForestCover.eval_rightLabel line 879
89. def OAI.EilenbergGanea.ForestCover.gauged line 887
90. theorem OAI.EilenbergGanea.ForestCover.gauged_split line 890
91. theorem OAI.EilenbergGanea.ForestCover.small_potential line 897
92. theorem OAI.EilenbergGanea.ForestCover.gauged_small line 904
93. theorem OAI.EilenbergGanea.ForestCover.eval_transport line 921
94. theorem OAI.EilenbergGanea.ForestCover.holonomy_loop_injective line 928
95. theorem OAI.EilenbergGanea.ForestCover.isFree_fundamentalGroup line 938

    Source documentation

    A genuine two-open-set cover by spaces with simply connected components has a free fundamental group. This includes graphs with arbitrary cell sets.

    theorem isFree_fundamentalGroup (hUo : IsOpen U) (hVo : IsOpen V) (hc : U ∪ V = univ) :
        IsFreeGroup (FundamentalGroup X r) := by
    …

96. theorem OAI.EilenbergGanea.ForestCover.thin_of_domination line 968
97. theorem OAI.EilenbergGanea.ForestCover.thin_discrete line 982
98. theorem OAI.EilenbergGanea.ForestCover.thin_homeomorph line 990
99. theorem OAI.EilenbergGanea.ForestCover.thin_sigma_contractible line 1003
100. theorem OAI.EilenbergGanea.ForestCover.thin_outer line 1010
101. theorem OAI.EilenbergGanea.ForestCover.thin_inner line 1013
102. theorem OAI.EilenbergGanea.ForestCover.isFree_attachment line 1018

     Source documentation

     Fundamental groups of arbitrary ordinary graph attachments are free.

     theorem isFree_attachment (a : Attachment X J 1) [DiscreteTopology a.lower]
         {r : X} (q : ∀ x, Path r x) : IsFreeGroup (FundamentalGroup X r) :=
     …

103. abbrev OAI.EilenbergGanea.CWSubspace.Cell line 1029
104. def OAI.EilenbergGanea.CWSubspace.characteristic line 1031
105. abbrev OAI.EilenbergGanea.CWSubspace.CellDisks line 1036
106. def OAI.EilenbergGanea.CWSubspace.diskSum line 1037
107. theorem OAI.EilenbergGanea.CWSubspace.diskSum_continuous line 1040
108. theorem OAI.EilenbergGanea.CWSubspace.diskSum_surjective line 1044
109. theorem OAI.EilenbergGanea.CWSubspace.diskSum_quotient line 1051
110. def OAI.EilenbergGanea.CWSubspace.lower line 1075
111. theorem OAI.EilenbergGanea.CWSubspace.characteristic_lower line 1077
112. def OAI.EilenbergGanea.CWSubspace.topSum line 1083
113. theorem OAI.EilenbergGanea.CWSubspace.topSum_continuous line 1086
114. theorem OAI.EilenbergGanea.CWSubspace.topSum_surjective line 1089
115. theorem OAI.EilenbergGanea.CWSubspace.topSum_quotient line 1102
116. def OAI.EilenbergGanea.CWSubspace.attachment line 1121
117. theorem OAI.EilenbergGanea.CWSubspace.discrete_dim_zero line 1156

     Source documentation

     The ordinary zero-skeleton is discrete without any cardinality restriction.

     theorem discrete_dim_zero (hd : ∀ k, 0 < k → IsEmpty (Cell C k)) : DiscreteTopology C := by
     …

     Mentions: OAI.EilenbergGanea.CWSubspace.Cell

118. def OAI.EilenbergGanea.CWSubspace.lowerHomeomorph line 1176
119. theorem OAI.EilenbergGanea.CWSubspace.discrete_lower_one line 1184
120. theorem OAI.EilenbergGanea.ForestCover.isFree_ordinary_graph line 1204

     Source documentation

     Arbitrary ordinary one-dimensional CW spaces have free fundamental groups.

     theorem isFree_ordinary_graph (hd : ∀ k, 1 < k → IsEmpty (Cell C k))
         {r : C} (q : ∀ x, Path r x) : IsFreeGroup (FundamentalGroup C r) := by
     …