CW complexes

This file defines (relative) CW complexes and proves basic properties about them.

A CW complex is a topological space that is made by gluing closed disks of different dimensions together.

Main definitions

• RelCWComplex C D: the class of CW structures on a subspace C relative to a base set D of a topological space X.
• CWComplex C: an abbreviation for RelCWComplex C ∅. The class of CW structures on a subspace C of the topological space X.
• openCell n: indexed family of all open cells of dimension n.
• closedCell n: indexed family of all closed cells of dimension n.
• cellFrontier n: indexed family of the boundaries of cells of dimension n.
• skeleton C n: the n-skeleton of the (relative) CW complex C.

Main statements

• iUnion_openCell_eq_skeleton: the skeletons can also be seen as a union of open cells.
• cellFrontier_subset_finite_openCell: the edge of a cell is contained in a finite union of open cells of a lower dimension.

Implementation notes

• We use the historical definition of CW complexes, due to Whitehead: a CW complex is a collection of cells with attaching maps - all cells are subspaces of one ambient topological space. This way, we avoid having to work with a lot of different topological spaces. On the other hand, it requires the union of all cells to be closed. If that is not the case, you need to consider that union as a subspace of itself.
• The definition RelCWComplex does not require X to be a Hausdorff space. A lot of the lemmas will however require this property.
• This definition is a class to ease working with different constructions and their properties. Overall this means the being a CW complex is treated more like a property than data.
• For statements, the auxiliary construction skeletonLT is preferred over skeleton as it makes the base case of inductions easier. The statement about skeleton should then be derived from the one about skeletonLT.

References

• A. Hatcher, Algebraic Topology

class Topology.RelCWComplex {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) : Type (u + 1)

A CW complex of a topological space X relative to another subspace D is the data of its n-cells cell n i for each n : ℕ along with attaching maps that satisfy a number of properties with the most important being closure-finiteness (mapsTo) and weak topology (closed'). Note that this definition requires C and D to be closed subspaces. If C is not closed choose X to be C.

• cell (n : ℕ) : Type u

  The indexing type of the cells of dimension n.

• map (n : ℕ) (i : cell C n) : PartialEquiv (Fin n → ℝ) X

  The characteristic map of the n-cell given by the index i. This map is a bijection when restricting to ball 0 1, where we consider (Fin n → ℝ) endowed with the maximum metric.

• source_eq (n : ℕ) (i : cell C n) : (map n i).source = Metric.ball 0 1

  The source of every charactersitic map of dimension n is (ball 0 1 : Set (Fin n → ℝ)).

• continuousOn (n : ℕ) (i : cell C n) : ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)

  The characteristic maps are continuous when restricting to closedBall 0 1.

• continuousOn_symm (n : ℕ) (i : cell C n) : ContinuousOn (↑(map n i).symm) (map n i).target

  The inverse of the restriction to ball 0 1 is continuous on the image.

• pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : ℕ) × cell C n) => ↑(map ni.fst ni.snd) '' Metric.ball 0 1

  The open cells are pairwise disjoint. Use RelCWComplex.pairwiseDisjoint or RelCWComplex.disjoint_openCell_of_ne instead.

• disjointBase' (n : ℕ) (i : cell C n) : Disjoint (↑(map n i) '' Metric.ball 0 1) D

  All open cells are disjoint with the base. Use RelCWComplex.disjointBase instead.

• mapsTo (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)

  The boundary of a cell is contained in a finite union of closed cells of a lower dimension. Use RelCWComplex.cellFrontier_subset_finite_closedCell instead.

• closed' (A : Set X) (asubc : A ⊆ C) : (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) ∧ IsClosed (A ∩ D) → IsClosed A

  A CW complex has weak topology, i.e. a set A in X is closed iff its intersection with every closed cell and D is closed. Use RelCWComplex.closed instead.

• isClosedBase : IsClosed D

  The base D is closed.

• union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell C n), ↑(map n j) '' Metric.closedBall 0 1 = C

  The union of all closed cells equals C. Use RelCWComplex.union instead.

@[deprecated Topology.RelCWComplex.mapsTo (since := "2025-02-20")]

theorem Topology.RelCWComplex.mapsto {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : RelCWComplex C D] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)

Alias of Topology.RelCWComplex.mapsTo.

---

The boundary of a cell is contained in a finite union of closed cells of a lower dimension. Use RelCWComplex.cellFrontier_subset_finite_closedCell instead.

@[reducible, inline]

abbrev Topology.CWComplex {X : Type u_1} [TopologicalSpace X] (C : Set X) : Type (u_1 + 1)

Characterizing when a subspace C of a topological space X is a CW complex. Note that this requires C to be closed. If C is not closed choose X to be C.

Equations

• Topology.CWComplex C = Topology.RelCWComplex C ∅

def Topology.CWComplex.mk {X : Type u} [TopologicalSpace X] (C : Set X) (cell : ℕ → Type u) (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : ℕ) × cell n) => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo : ∀ (n : ℕ) (i : cell n), ∃ (I : (m : ℕ) → Finset (cell m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)) (closed' : ∀ A ⊆ C, (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) → IsClosed A) (union' : ⋃ (n : ℕ), ⋃ (j : cell n), ↑(map n j) '' Metric.closedBall 0 1 = C) : CWComplex C

A constructor for CWComplex.

Equations

• One or more equations did not get rendered due to their size.

def Topology.RelCWComplex.openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set X

The open n-cell given by the index i. Use this instead of map n i '' ball 0 1 whenever possible.

Equations

• Topology.RelCWComplex.openCell n i = ↑(Topology.RelCWComplex.map n i) '' Metric.ball 0 1

def Topology.RelCWComplex.closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set X

The closed n-cell given by the index i. Use this instead of map n i '' closedBall 0 1 whenever possible.

Equations

• Topology.RelCWComplex.closedCell n i = ↑(Topology.RelCWComplex.map n i) '' Metric.closedBall 0 1

def Topology.RelCWComplex.cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set X

The boundary of the n-cell given by the index i. Use this instead of map n i '' sphere 0 1 whenever possible.

Equations

• Topology.RelCWComplex.cellFrontier n i = ↑(Topology.RelCWComplex.map n i) '' Metric.sphere 0 1

theorem Topology.CWComplex.mapsTo {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)

@[deprecated Topology.CWComplex.mapsTo (since := "2025-02-20")]

theorem Topology.CWComplex.mapsto {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)

Alias of Topology.CWComplex.mapsTo.

theorem Topology.RelCWComplex.pairwiseDisjoint {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : Set.univ.PairwiseDisjoint fun (ni : (n : ℕ) × cell C n) => openCell ni.fst ni.snd

theorem Topology.RelCWComplex.disjointBase {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : Disjoint (openCell n i) D

theorem Topology.RelCWComplex.disjoint_openCell_of_ne {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n m : ℕ} {i : cell C n} {j : cell C m} (ne : ⟨n, i⟩ ≠ ⟨m, j⟩) : openCell n i ∩ openCell m j = ∅

theorem Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), cellFrontier n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

theorem Topology.CWComplex.cellFrontier_subset_finite_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), cellFrontier n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

theorem Topology.RelCWComplex.union {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : D ∪ ⋃ (n : ℕ), ⋃ (j : cell C n), closedCell n j = C

theorem Topology.CWComplex.union {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] : ⋃ (n : ℕ), ⋃ (j : cell C n), closedCell n j = C

theorem Topology.RelCWComplex.openCell_subset_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : openCell n i ⊆ closedCell n i

theorem Topology.RelCWComplex.cellFrontier_subset_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : cellFrontier n i ⊆ closedCell n i

theorem Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : cellFrontier n i ∪ openCell n i = closedCell n i

theorem Topology.RelCWComplex.map_zero_mem_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : ↑(map n i) 0 ∈ openCell n i

theorem Topology.RelCWComplex.map_zero_mem_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : ↑(map n i) 0 ∈ closedCell n i

def Topology.RelCWComplex.skeletonLT {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) : Set X

A non-standard definition of the n-skeleton of a CW complex for n ∈ ℕ ∪ {∞}. This allows the base case of induction to be about the base instead of being about the union of the base and some points. The standard skeleton is defined in terms of skeletonLT. skeletonLT is preferred in statements. You should then derive the statement about skeleton.

Equations

• Topology.RelCWComplex.skeletonLT C n = D ∪ ⋃ (m : ℕ), ⋃ (_ : ↑m < n), ⋃ (j : Topology.RelCWComplex.cell C m), Topology.RelCWComplex.closedCell m j

def Topology.RelCWComplex.skeleton {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) : Set X

The n-skeleton of a CW complex, for n ∈ ℕ ∪ {∞}. For statements use skeletonLT instead and then derive the statement about skeleton.

Equations

• Topology.RelCWComplex.skeleton C n = Topology.RelCWComplex.skeletonLT C (n + 1)

theorem Topology.RelCWComplex.skeletonLT_zero_eq_base {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : skeletonLT C 0 = D

theorem Topology.CWComplex.skeletonLT_zero_eq_empty {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] : skeletonLT C 0 = ∅

theorem Topology.RelCWComplex.isCompact_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : ℕ} {i : cell C n} : IsCompact (closedCell n i)

theorem Topology.RelCWComplex.isClosed_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} : IsClosed (closedCell n i)

theorem Topology.RelCWComplex.isCompact_cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : ℕ} {i : cell C n} : IsCompact (cellFrontier n i)

theorem Topology.RelCWComplex.isClosed_cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} : IsClosed (cellFrontier n i)

theorem Topology.RelCWComplex.closure_openCell_eq_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {n : ℕ} {j : cell C n} : closure (openCell n j) = closedCell n j

theorem Topology.RelCWComplex.closed {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] [T2Space X] (A : Set X) (asubc : A ⊆ C) : IsClosed A ↔ (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ D)

theorem Topology.CWComplex.closed {X : Type u_1} [t : TopologicalSpace X] (C : Set X) [CWComplex C] [T2Space X] (A : Set X) (asubc : A ⊆ C) : IsClosed A ↔ ∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)

@[simp]

theorem Topology.RelCWComplex.skeletonLT_top {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : skeletonLT C ⊤ = C

@[simp]

theorem Topology.RelCWComplex.skeleton_top {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : skeleton C ⊤ = C

theorem Topology.RelCWComplex.skeletonLT_mono {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) : skeletonLT C m ⊆ skeletonLT C n

theorem Topology.RelCWComplex.skeleton_mono {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) : skeleton C m ⊆ skeleton C n

theorem Topology.RelCWComplex.skeletonLT_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : ℕ∞} : skeletonLT C n ⊆ C

theorem Topology.RelCWComplex.skeleton_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : ℕ∞} : skeleton C n ⊆ C

theorem Topology.RelCWComplex.closedCell_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ skeletonLT C (↑n + 1)

theorem Topology.RelCWComplex.closedCell_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ skeleton C ↑n

theorem Topology.RelCWComplex.closedCell_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ C

theorem Topology.RelCWComplex.openCell_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ skeletonLT C (↑n + 1)

theorem Topology.RelCWComplex.openCell_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ skeleton C ↑n

theorem Topology.RelCWComplex.openCell_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ C

theorem Topology.RelCWComplex.cellFrontier_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : cellFrontier n j ⊆ skeletonLT C ↑n

theorem Topology.RelCWComplex.cellFrontier_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C (n + 1)) : cellFrontier (n + 1) j ⊆ skeleton C ↑n

theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (l : ℕ) : ⋃ (j : cell C l), cellFrontier l j ⊆ skeletonLT C ↑l

theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (l : ℕ) : ⋃ (j : cell C l), cellFrontier l j ⊆ skeleton C ↑l

theorem Topology.RelCWComplex.closedCell_zero_eq_singleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {j : cell C 0} : closedCell 0 j = {↑(map 0 j) ![]}

theorem Topology.RelCWComplex.openCell_zero_eq_singleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {j : cell C 0} : openCell 0 j = {↑(map 0 j) ![]}

theorem Topology.RelCWComplex.cellFrontier_zero_eq_empty {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {j : cell C 0} : cellFrontier 0 j = ∅

theorem Topology.RelCWComplex.base_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ∞) : D ⊆ skeletonLT C n

theorem Topology.RelCWComplex.base_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ∞) : D ⊆ skeleton C n

theorem Topology.RelCWComplex.base_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : D ⊆ C