The image of a CW complex under a closed embedding

Let f : X → Y be a closed embedding and let C be a CW complex relative to D in X. Then f '' C is a CW complex relative to f '' D in Y (Topology.IsClosedEmbedding.relCWComplex), with the same cells (Topology.IsClosedEmbedding.relCWComplexCellEquiv) and the characteristic maps of C followed by f (Topology.IsClosedEmbedding.coe_map_relCWComplex). For an absolute CW complex, the base is f '' ∅ = ∅, and Topology.RelCWComplex.toCWComplex turns the result into an absolute CW complex.

This is how a CW structure on a space X is read inside a larger space containing X as a closed subspace, for instance the target of a relative CW complex built on X, where it serves as the base. The images are given as sets C' and D' with equations f '' C = C' and f '' D = D', because the base of a relative CW complex is determined by the complex, and the image of Set.univ is the range of f only up to Set.image_univ.

The two spaces lie in a common universe, since the cells of a CW complex are indexed by types in the universe of its ambient space.

The axioms transfer because f is a homeomorphism onto its image: the inverse of a characteristic map on its open cell is continuous because f is an embedding, and the weak topology transfers because f is a closed map.

References

• A. Hatcher, Algebraic Topology, Chapter 0 and the Appendix, for CW complexes and their subcomplexes as closed subspaces.

@[instance_reducible]

noncomputable def Topology.IsClosedEmbedding.relCWComplex {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) {C D : Set X} [RelCWComplex C D] {C' D' : Set Y} (hC : f '' C = C') (hD : f '' D = D') : RelCWComplex C' D'

The image of a relative CW complex under a closed embedding. If f is a closed embedding and C is a CW complex relative to D, then C' = f '' C is a CW complex relative to D' = f '' D, with the cells of C and their characteristic maps followed by f.

def Topology.IsClosedEmbedding.relCWComplexCellEquiv {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) {C D : Set X} [RelCWComplex C D] {C' D' : Set Y} (hC : f '' C = C') (hD : f '' D = D') (n : ℕ) : RelCWComplex.cell C' n ≃ RelCWComplex.cell C n

The cells of the image of C under a closed embedding are the cells of C.

@[simp]

theorem Topology.IsClosedEmbedding.coe_map_relCWComplex {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) {C D : Set X} [RelCWComplex C D] {C' D' : Set Y} (hC : f '' C = C') (hD : f '' D = D') (n : ℕ) (i : RelCWComplex.cell C' n) : ↑(RelCWComplex.map n i) = f ∘ ↑(RelCWComplex.map n ((hf.relCWComplexCellEquiv hC hD n) i))

The characteristic maps of the image of C under a closed embedding f are those of C followed by f.

@[simp]

theorem Topology.IsClosedEmbedding.openCell_relCWComplex {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) {C D : Set X} [RelCWComplex C D] {C' D' : Set Y} (hC : f '' C = C') (hD : f '' D = D') (n : ℕ) (i : RelCWComplex.cell C' n) : RelCWComplex.openCell n i = f '' RelCWComplex.openCell n ((hf.relCWComplexCellEquiv hC hD n) i)

The open cells of the image of C under f are the images of the open cells of C.

@[simp]

theorem Topology.IsClosedEmbedding.closedCell_relCWComplex {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) {C D : Set X} [RelCWComplex C D] {C' D' : Set Y} (hC : f '' C = C') (hD : f '' D = D') (n : ℕ) (i : RelCWComplex.cell C' n) : RelCWComplex.closedCell n i = f '' RelCWComplex.closedCell n ((hf.relCWComplexCellEquiv hC hD n) i)

The closed cells of the image of C under f are the images of the closed cells of C.

@[simp]

theorem Topology.IsClosedEmbedding.cellFrontier_relCWComplex {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) {C D : Set X} [RelCWComplex C D] {C' D' : Set Y} (hC : f '' C = C') (hD : f '' D = D') (n : ℕ) (i : RelCWComplex.cell C' n) : RelCWComplex.cellFrontier n i = f '' RelCWComplex.cellFrontier n ((hf.relCWComplexCellEquiv hC hD n) i)

The boundaries of the cells of the image of C under f are the images of the boundaries of the cells of C.