Disjoint unions of CW complexes

An arbitrary disjoint union of relative CW complexes is a relative CW complex, with one cell for each cell in each summand. Its characteristic maps are the original maps followed by the summand inclusions. Closure-finiteness stays within a single summand, and the weak topology follows from the coproduct topology. Neither local finiteness nor a separation assumption is required.

The absolute construction is an instance. In particular, disjoint unions of spaces with CW structures again carry CW structures. This allows componentwise constructions of CW models to be assembled without a connectedness hypothesis.

References

• A. Hatcher, Algebraic Topology, Chapter 0 and the Appendix (CW complexes).

The characteristic maps reuse IsClosedEmbedding.relCWComplex for each summand.

@[instance_reducible]

noncomputable def Topology.RelCWComplex.sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C D : (i : ι) → Set (X i)) [(i : ι) → RelCWComplex (C i) (D i)] : RelCWComplex (Set.univ.sigma C) (Set.univ.sigma D)

The relative CW structure on a disjoint union. Cells retain their summand index. This is not an instance, since the base of a relative CW structure is an output parameter.

noncomputable def Topology.RelCWComplex.sigmaCellEquiv {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C D : (i : ι) → Set (X i)) [(i : ι) → RelCWComplex (C i) (D i)] (n : ℕ) : cell (Set.univ.sigma C) n ≃ (i : ι) × cell (C i) n

The cells of a disjoint union are the cells of its summands, with their summand indices.

@[simp]

theorem Topology.RelCWComplex.coe_map_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C D : (i : ι) → Set (X i)) [(i : ι) → RelCWComplex (C i) (D i)] (n : ℕ) (i : ι) (j : cell (C i) n) : ↑(map n ((sigmaCellEquiv C D n).symm ⟨i, j⟩)) = Sigma.mk i ∘ ↑(map n j)

A characteristic map in a disjoint union is followed by its summand inclusion.

@[simp]

theorem Topology.RelCWComplex.openCell_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C D : (i : ι) → Set (X i)) [(i : ι) → RelCWComplex (C i) (D i)] (n : ℕ) (i : ι) (j : cell (C i) n) : openCell n ((sigmaCellEquiv C D n).symm ⟨i, j⟩) = Sigma.mk i '' openCell n j

Open cells in the disjoint union are images of open cells in the summands.

@[simp]

theorem Topology.RelCWComplex.closedCell_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C D : (i : ι) → Set (X i)) [(i : ι) → RelCWComplex (C i) (D i)] (n : ℕ) (i : ι) (j : cell (C i) n) : closedCell n ((sigmaCellEquiv C D n).symm ⟨i, j⟩) = Sigma.mk i '' closedCell n j

Closed cells in the disjoint union are images of closed cells in the summands.

@[simp]

theorem Topology.RelCWComplex.cellFrontier_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C D : (i : ι) → Set (X i)) [(i : ι) → RelCWComplex (C i) (D i)] (n : ℕ) (i : ι) (j : cell (C i) n) : cellFrontier n ((sigmaCellEquiv C D n).symm ⟨i, j⟩) = Sigma.mk i '' cellFrontier n j

Cell frontiers in the disjoint union are images of frontiers in the summands.

@[instance_reducible]

noncomputable instance Topology.CWComplex.sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C : (i : ι) → Set (X i)) [(i : ι) → CWComplex (C i)] : CWComplex (Set.univ.sigma C)

An arbitrary disjoint union of CW complexes is a CW complex.

noncomputable def Topology.CWComplex.sigmaCellEquiv {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C : (i : ι) → Set (X i)) [(i : ι) → CWComplex (C i)] (n : ℕ) : cell (Set.univ.sigma C) n ≃ (i : ι) × cell (C i) n

Cells in the absolute disjoint union retain their summand index.

@[simp]

theorem Topology.CWComplex.coe_map_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C : (i : ι) → Set (X i)) [(i : ι) → CWComplex (C i)] (n : ℕ) (i : ι) (j : cell (C i) n) : ↑(map n ((sigmaCellEquiv C n).symm ⟨i, j⟩)) = Sigma.mk i ∘ ↑(map n j)

Absolute characteristic maps are followed by the summand inclusion.

@[simp]

theorem Topology.CWComplex.openCell_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C : (i : ι) → Set (X i)) [(i : ι) → CWComplex (C i)] (n : ℕ) (i : ι) (j : cell (C i) n) : openCell n ((sigmaCellEquiv C n).symm ⟨i, j⟩) = Sigma.mk i '' openCell n j

Absolute open cells are the summand images of the original open cells.

@[simp]

theorem Topology.CWComplex.closedCell_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C : (i : ι) → Set (X i)) [(i : ι) → CWComplex (C i)] (n : ℕ) (i : ι) (j : cell (C i) n) : closedCell n ((sigmaCellEquiv C n).symm ⟨i, j⟩) = Sigma.mk i '' closedCell n j

Absolute closed cells are the summand images of the original closed cells.

@[simp]

theorem Topology.CWComplex.cellFrontier_sigma {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (C : (i : ι) → Set (X i)) [(i : ι) → CWComplex (C i)] (n : ℕ) (i : ι) (j : cell (C i) n) : cellFrontier n ((sigmaCellEquiv C n).symm ⟨i, j⟩) = Sigma.mk i '' cellFrontier n j

Absolute cell frontiers are the summand images of the original frontiers.

@[instance_reducible]

noncomputable instance Topology.CWComplex.sigmaUniv {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → CWComplex Set.univ] : CWComplex Set.univ

A disjoint union of spaces with CW structures has a CW structure on the whole space.

noncomputable def Topology.CWComplex.sigmaUnivCellEquiv {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → CWComplex Set.univ] (n : ℕ) : cell Set.univ n ≃ (i : ι) × cell Set.univ n

Cells in the whole-space disjoint union retain their summand index.

@[simp]

theorem Topology.CWComplex.coe_map_sigmaUniv {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → CWComplex Set.univ] (n : ℕ) (i : ι) (j : cell Set.univ n) : ↑(map n ((sigmaUnivCellEquiv n).symm ⟨i, j⟩)) = Sigma.mk i ∘ ↑(map n j)

Whole-space characteristic maps are followed by the summand inclusion.

@[simp]

theorem Topology.CWComplex.openCell_sigmaUniv {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → CWComplex Set.univ] (n : ℕ) (i : ι) (j : cell Set.univ n) : openCell n ((sigmaUnivCellEquiv n).symm ⟨i, j⟩) = Sigma.mk i '' openCell n j

Whole-space open cells are the summand images of the original open cells.

@[simp]

theorem Topology.CWComplex.closedCell_sigmaUniv {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → CWComplex Set.univ] (n : ℕ) (i : ι) (j : cell Set.univ n) : closedCell n ((sigmaUnivCellEquiv n).symm ⟨i, j⟩) = Sigma.mk i '' closedCell n j

Whole-space closed cells are the summand images of the original closed cells.

@[simp]

theorem Topology.CWComplex.cellFrontier_sigmaUniv {ι : Type u} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → CWComplex Set.univ] (n : ℕ) (i : ι) (j : cell Set.univ n) : cellFrontier n ((sigmaUnivCellEquiv n).symm ⟨i, j⟩) = Sigma.mk i '' cellFrontier n j

Whole-space cell frontiers are the summand images of the original frontiers.