OAI/Algebra/GroupRing/Cellular.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Classical cellular lifting and its geometric foundations. No classifying-space existence or Hurewicz theorem is assumed.

  1. lemma OAI.GroupRingTopology.Cellular.closedCell_subset_finite_openCells line 18

    Source documentation

    Closure finiteness in terms of a single finite list of open cells.

    lemma closedCell_subset_finite_openCells (n : ℕ) (i : RelCWComplex.cell C n) :
    ∃ I : Finset (Σ m, RelCWComplex.cell C m),
      CWComplex.closedCell n i ⊆ ⋃ p ∈ I, CWComplex.openCell p.1 p.2 := by
…
  2. lemma OAI.GroupRingTopology.Cellular.cellSelection_closed line 37

    Source documentation

    Any selection of at most one point from each open cell has all its subsets closed. This is the closure-finite weak-topology argument behind compactness.

    lemma cellSelection_closed {I : Type u} (c : I → Σ n, RelCWComplex.cell C n)
    (hc : Function.Injective c) (x : I → X)
    (hx : ∀ i, x i ∈ CWComplex.openCell (c i).1 (c i).2) (S : Set X)
    (hS : S ⊆ Set.range x) : IsClosed S := by
…
  3. theorem OAI.GroupRingTopology.Cellular.compact_finitely_many_cells line 63

    Source documentation

    A compact part of a CW complex can meet only finitely many open cells.

    theorem compact_finitely_many_cells {K : Set X} (hK : IsCompact K) :
    {p : Σ n, RelCWComplex.cell C n | (K ∩ CWComplex.openCell p.1 p.2).Nonempty}.Finite := by
…
  4. theorem OAI.GroupRingTopology.Cellular.compact_bounded_skeleton line 88

    Source documentation

    Compact maps cannot run out through infinitely many dimensions.

    theorem compact_bounded_skeleton {K : Set X} (hK : IsCompact K) (hKC : K ⊆ C) :
    ∃ n : ℕ, K ⊆ CWComplex.skeletonLT C n := by
…
  5. theorem OAI.GroupRingTopology.Cellular.compactMap_bounded_skeleton line 108

    Source documentation

    The bounded-skeleton property in its map form, used for spheres and disks.

    theorem compactMap_bounded_skeleton {A : Type*} [TopologicalSpace A] [CompactSpace A]
    (f : C(A,X)) (hf : ∀ a, f a ∈ C) :
    ∃ n : ℕ, ∀ a, f a ∈ CWComplex.skeletonLT C n := by
…
  6. lemma OAI.GroupRingTopology.Simplicial.compact_bounded_vertices line 123
  7. abbrev OAI.GroupRingTopology.SphereTopology.Disk line 145
  8. abbrev OAI.GroupRingTopology.SphereTopology.Sphere line 146
  9. def OAI.GroupRingTopology.SphereTopology.boundary line 148
  10. lemma OAI.GroupRingTopology.SphereTopology.sphere_norm line 151
  11. lemma OAI.GroupRingTopology.SphereTopology.disk_norm line 153
  12. def OAI.GroupRingTopology.SphereTopology.cone line 156
  13. lemma OAI.GroupRingTopology.SphereTopology.cone_norm line 164
  14. lemma OAI.GroupRingTopology.SphereTopology.cone_surjective line 167
  15. lemma OAI.GroupRingTopology.SphereTopology.cone_quotient line 180
  16. def OAI.GroupRingTopology.SphereTopology.Extends line 185
  17. lemma OAI.GroupRingTopology.SphereTopology.extends_of_nullhomotopic line 187
  18. lemma OAI.GroupRingTopology.SphereTopology.nullhomotopic_of_extends line 213
  19. lemma OAI.GroupRingTopology.SphereTopology.extends_of_homotopy line 229
  20. lemma OAI.GroupRingTopology.SphereTopology.sphere_nonempty line 234
  21. abbrev OAI.GroupRingTopology.Cellular.Disk line 246
  22. abbrev OAI.GroupRingTopology.Cellular.Sphere line 247
  23. def OAI.GroupRingTopology.Cellular.boundary line 249
  24. lemma OAI.GroupRingTopology.Cellular.continuous_boundary line 252
  25. def OAI.GroupRingTopology.Cellular.characteristic line 259

    Source documentation

    A characteristic map on its closed disk.

    def characteristic (n : ℕ) (i : RelCWComplex.cell C n) : C(Disk n, X) :=
…

    Mentions: OAI.GroupRingTopology.Cellular.Disk

  26. lemma OAI.GroupRingTopology.Cellular.range_characteristic line 263
  27. lemma OAI.GroupRingTopology.Cellular.continuousOn_iff_characteristic line 272

    Source documentation

    The weak topology is genuinely final with respect to closed characteristic maps; no finiteness or local-finiteness hypothesis is needed.

    lemma continuousOn_iff_characteristic {Y : Type v} [TopologicalSpace Y] (f : X → Y) :
    ContinuousOn f C ↔ ∀ n (i : RelCWComplex.cell C n),
      Continuous (f ∘ characteristic n i) := by
…

    Mentions: OAI.GroupRingTopology.Cellular.characteristic

  28. abbrev OAI.GroupRingTopology.Cellular.Skeleton line 300
  29. lemma OAI.GroupRingTopology.Cellular.skeleton_mono line 303
  30. lemma OAI.GroupRingTopology.Cellular.sphere_mem_skeleton line 307
  31. lemma OAI.GroupRingTopology.Cellular.characteristic_mem_skeleton line 311
  32. lemma OAI.GroupRingTopology.Cellular.openCell_not_skeleton line 317
  33. structure OAI.GroupRingTopology.Cellular.PartialLift line 324

    Source documentation

    A continuous partial lift on the (n-1)-skeleton, represented by a total function only to avoid transported subtype terms. Values outside the skeleton carry no condition and are never used.

    structure PartialLift {E : Type v} {B : Type w} [TopologicalSpace E] [TopologicalSpace B]
    (p : C(E,B)) (f : C(X,B)) (n : ℕ) where
…
  34. def OAI.GroupRingTopology.Cellular.DiskRLP line 331

    Source documentation

    The concrete disk-boundary right lifting property.

    def DiskRLP {E : Type v} {B : Type w} [TopologicalSpace E] [TopologicalSpace B]
    (p : C(E,B)) : Prop :=
…
  35. def OAI.GroupRingTopology.Cellular.attachValue line 340

    Source documentation

    Glue the old skeleton map to a prescribed disk map on each new cell.

    noncomputable def attachValue (a : X → E) (e : ∀ _ : RelCWComplex.cell C n, C(Disk n,E))
    (x : X) : E := by
…

    Mentions: OAI.GroupRingTopology.Cellular.Disk

  36. lemma OAI.GroupRingTopology.Cellular.attachValue_old line 350
  37. lemma OAI.GroupRingTopology.Cellular.attachValue_interior line 355
  38. lemma OAI.GroupRingTopology.Cellular.attachValue_characteristic line 382
  39. lemma OAI.GroupRingTopology.Cellular.attachValue_continuous line 395