OAI/Algebra/GroupRing/SphereTopology.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GroupRingTopology.Cellular.skeletonInclusion line 25
2. lemma OAI.GroupRingTopology.Cellular.deform_skeleton_succ line 29

   Source documentation

   One step of the classical cellular approximation theorem, without any local finiteness assumption on the target CW complex.

   lemma deform_skeleton_succ (n : ℕ) (f : C(K,Skeleton C (n+1)))
       (hdim : dimH (Set.univ : Set K) < n) :
       ∃ (g : C(K,Skeleton C n))
         (H : f.Homotopy ((skeletonBase n).comp g)),
         ∀ t x, (f x).1 ∈ Skeleton C n → H (t,x) = f x := by
   …

   Mentions: OAI.GroupRingTopology.Cellular.Skeleton, OAI.GroupRingTopology.Cellular.skeletonBase

3. lemma OAI.GroupRingTopology.Cellular.deform_bounded_skeleton line 57

   Source documentation

   Bounded-skeleton cellular approximation with a stationary relative set: all points initially in the target skeleton remain fixed.

   lemma deform_bounded_skeleton (d m : ℕ) (f : C(K,Skeleton C m))
       (hdim : dimH (Set.univ : Set K) < d) :
       ∃ (g : C(K,Skeleton C d))
         (H : ((skeletonInclusion m).comp f).Homotopy ((skeletonInclusion d).comp g)),
         ∀ t x, (f x).1 ∈ Skeleton C d → H (t,x) = (f x).1 := by
   …

   Mentions: OAI.GroupRingTopology.Cellular.Skeleton, OAI.GroupRingTopology.Cellular.skeletonInclusion

4. theorem OAI.GroupRingTopology.Cellular.exists_cellular_approximation line 94

   Source documentation

   Cellular approximation for arbitrary compact finite-Hausdorff-dimensional sources. Compactness bounds the traversed dimensions, not the number of cells of the whole CW complex.

   theorem exists_cellular_approximation (d : ℕ) (f : C(K,X)) (hf : ∀ x,f x ∈ C)
       (hdim : dimH (Set.univ : Set K) < d) :
       ∃ (g : C(K,Skeleton C d)) (H : f.Homotopy ((skeletonInclusion d).comp g)),
         ∀ t x, f x ∈ Skeleton C d → H (t,x) = f x := by
   …

   Mentions: OAI.GroupRingTopology.Cellular.Skeleton, OAI.GroupRingTopology.Cellular.skeletonInclusion

5. lemma OAI.GroupRingTopology.SphereTopology.fill_zero line 106
6. lemma OAI.GroupRingTopology.SphereTopology.fill_one line 114
7. def OAI.GroupRingTopology.Cellular.KillsSpheres line 132

   Source documentation

   A ghost map in one geometric degree, including unbased spheres.

   def KillsSpheres (q : C(Y,Z)) (n : ℕ) : Prop :=
   …

8. lemma OAI.GroupRingTopology.Cellular.cylinder_filling_after line 135
9. structure OAI.GroupRingTopology.Cellular.PartialHomotopy line 181
10. def OAI.GroupRingTopology.Cellular.PartialHomotopy.onSphere line 190
11. def OAI.GroupRingTopology.Cellular.PartialHomotopy.endpoints line 196
12. lemma OAI.GroupRingTopology.Cellular.PartialHomotopy.endpoints_compatible line 201
13. lemma OAI.GroupRingTopology.Cellular.PartialHomotopy.cell_extension_after line 206
14. def OAI.GroupRingTopology.Cellular.PartialHomotopy.next line 219

    Source documentation

    A single uniform ghost extends every partially constructed homotopy by a whole CW dimension, even if there are infinitely many cells in that dimension.

    def next (a : PartialHomotopy (C := C) f g n)
    …

    Mentions: OAI.GroupRingTopology.Cellular.PartialHomotopy

15. def OAI.GroupRingTopology.Cellular.PartialHomotopy.start line 249
16. def OAI.GroupRingTopology.Cellular.PartialHomotopy.toHomotopy line 261

    Source documentation

    On a whole finite-dimensional complex the final partial homotopy is an ordinary continuous homotopy, not merely cellwise data.

    def toHomotopy [CWComplex (Set.univ : Set X)] (a : PartialHomotopy (C := (Set.univ : Set X)) f g n)
    …

    Mentions: OAI.GroupRingTopology.Cellular.PartialHomotopy

17. lemma OAI.TorsionFreeZeroDivisors.FiniteDimensionalCW.skeleton_eq_univ line 283

    Source documentation

    No higher cells really means that the indicated finite skeleton is the whole space; no replacement by homology or a resolution is involved.

    lemma skeleton_eq_univ (N : ℕ)
        (hdim : ∀ m : ℕ, N ≤ m → IsEmpty (RelCWComplex.cell (Set.univ : Set X) m)) :
        Skeleton (Set.univ : Set X) N=Set.univ := by
    …

18. theorem OAI.TorsionFreeZeroDivisors.FiniteDimensionalCW.contractible_of_two_dimensional_fills line 302

    Source documentation

    A two-dimensional CW contraction uses only fillings of circles and 2-spheres: extend the contraction over actual 0-, 1-, and 2-cells. This is the needed special case of Whitehead, proved directly using cellular homotopy extension from the supplied checked support.

    theorem contractible_of_two_dimensional_fills [PathConnectedSpace X]
        (hdim : ∀ m : ℕ, 2 < m → IsEmpty (RelCWComplex.cell (Set.univ : Set X) m))
        (hcircle : ∀ a : C(SphereTopology.Sphere 2,X),SphereTopology.Extends a)
        (hsphere : ∀ a : C(SphereTopology.Sphere 3,X),SphereTopology.Extends a) :
        ContractibleSpace X := by
    …

19. def OAI.TorsionFreeZeroDivisors.PresentationTopology.pointCover line 333
20. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.pointCover_quotient line 334
21. def OAI.TorsionFreeZeroDivisors.PresentationTopology.roseAttaching line 352
22. abbrev OAI.TorsionFreeZeroDivisors.PresentationTopology.Rose line 353
23. def OAI.TorsionFreeZeroDivisors.PresentationTopology.graphProjection line 354
24. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.graphProjection_quotient line 356
25. instance OAI.TorsionFreeZeroDivisors.PresentationTopology.roseT2 line 358
26. instance OAI.TorsionFreeZeroDivisors.PresentationTopology.roseCW line 359
27. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.rose_dimension line 362
28. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.rose_finite line 365
29. instance OAI.TorsionFreeZeroDivisors.PresentationTopology.rosePathConnected line 371
30. def OAI.TorsionFreeZeroDivisors.PresentationTopology.diskAttaching line 376
31. abbrev OAI.TorsionFreeZeroDivisors.PresentationTopology.Base line 378
32. def OAI.TorsionFreeZeroDivisors.PresentationTopology.projection line 379
33. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.projection_quotient line 382
34. instance OAI.TorsionFreeZeroDivisors.PresentationTopology.baseT2 line 384
35. instance OAI.TorsionFreeZeroDivisors.PresentationTopology.baseCW line 386
36. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.base_dimension line 388
37. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.base_no_higher line 390
38. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.base_finite line 393
39. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.base_two_cell line 396
40. instance OAI.TorsionFreeZeroDivisors.PresentationTopology.basePathConnected line 400
41. def OAI.TorsionFreeZeroDivisors.PresentationTopology.coverPoint line 403
42. def OAI.TorsionFreeZeroDivisors.PresentationTopology.basePoint line 405
43. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.cover_no_higher line 406
44. def OAI.TorsionFreeZeroDivisors.PresentationTopology.fundamentalEquiv line 415
45. lemma OAI.TorsionFreeZeroDivisors.PresentationTopology.contractible_cover line 422