The open cells of a categorical relative CW complex #
Mathlib's categorical relative CW complex c : TopCat.RelativeCWComplex f, for a morphism
f : X ⟶ Y of TopCat, presents Y as the colimit of a sequence of spaces c.F.obj n, each
obtained from the previous one by attaching n-disks along their boundary spheres. A cell γ of
c comes with its inclusion γ.ι : 𝔻 γ.j ⟶ Y, and its open cell is the image under γ.ι of
the open disk, the complement of the boundary sphere. This file proves, for the open cells of c
and the range of f, the properties that the axioms of a classical Topology.RelCWComplex on Y
relative to the range of f ask of open cells individually:
γ.ιrestricts to an embedding of the open disk intoY(TopCat.RelativeCWComplex.isEmbedding_domRestrict_cells_ι);- distinct open cells are disjoint (
TopCat.RelativeCWComplex.disjoint_image_cells_ι), and every open cell is disjoint from the range off(TopCat.RelativeCWComplex.disjoint_range_image_cells_ι); - the image of
c.F.obj ninYis the range offtogether with the open cells of dimension less thann(TopCat.RelativeCWComplex.range_incl_app_eq_union_iUnion_image_cells_ι), or equivalently together with the closed cells of dimension less thann(TopCat.RelativeCWComplex.range_incl_app_eq_union_iUnion_range_cells_ι), soYis the disjoint union of the range offand all open cells (TopCat.RelativeCWComplex.range_union_iUnion_image_cells_ι).
The two remaining axioms, that the boundary of a cell meets only finitely many cells of lower
dimension and that Y carries the weak topology of its closed cells, concern how closed cells meet
and are not treated here.
These come from the corresponding statements for a single step of attaching cells in TopCat
(HomotopicalAlgebra.AttachCells.isOpenEmbedding_domRestrict_cell,
HomotopicalAlgebra.AttachCells.disjoint_image_cell,
HomotopicalAlgebra.AttachCells.compl_range_eq_iUnion_image_cell), which in turn come from the
behaviour of pushouts and coproducts in TopCat on complements of ranges
(TauCeti.Topology.Category.TopCat.OpenEmbedding), together with the closed embedding of each
stage into Y (TopCat.RelativeCWComplex.isClosedEmbedding_incl_app).
References #
- A. Hatcher, Algebraic Topology, Appendix, on the topology of cell complexes.
- R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990, for the categorical definition.
When cells are attached in TopCat, the complement of the old space in the new one is the
union of the images of the interiors of the cells, the complements of the ranges of the basic
cells.
When cells are attached in TopCat, the images of the interiors of distinct cells are
disjoint.
When cells are attached in TopCat along basic cells with closed ranges, each cell restricts
to an open embedding on its interior, the complement of the range of its basic cell.
In a relative CW complex, the inclusion of a cell restricts to an embedding of the open disk, the complement of the boundary sphere.
In a relative CW complex, the open cell of γ is disjoint from the image of every stage up to
the one where γ is attached.
In a relative CW complex, every open cell is disjoint from the range of the complex.
In a relative CW complex, distinct cells have disjoint open cells.
In a relative CW complex, the image of the n-th stage is the range of the complex together
with the open cells of dimension less than n.
In a relative CW complex, the image of the n-th stage is the range of the complex together
with the closed cells of dimension less than n.
A relative CW complex f : X ⟶ Y covers Y by the range of f and the open cells.