Composing relative CW complexes

Let C be a CW complex relative to D, and let D in turn be a CW complex relative to E, in a Hausdorff space. Then C is a CW complex relative to E (TauCeti.relCWComplexTrans), whose n-cells are the n-cells of D together with the n-cells of C, with their characteristic maps (TauCeti.relCWComplexTransCellEquiv). Taking E = ∅ and passing to an absolute CW complex with Topology.RelCWComplex.toCWComplex, a complex built by attaching cells to a CW complex is a CW complex.

One compatibility condition between the two structures is needed. The boundary of an n-cell of C must lie in finitely many cells of dimension less than n, so the part of it in D must lie in the skeleton skeletonLT D n. This is the only hypothesis. It holds, for instance, when all cells of D have dimension less than all cells of C, the situation of a tower of cell attachments of increasing dimension. Without it the cells of D and of C together need not satisfy the closure-finiteness axiom: attaching a 1-cell to the closed 2-disk, with its usual cells, along two interior points of the disk gives a CW complex relative to the disk, but the boundary of the 1-cell lies in the open 2-cell.

Given the condition, the boundary of a cell of C is compact, so it meets only finitely many open cells of D (TauCeti.finite_setOf_nonempty_inter_openCell_of_isCompact); those of them that meet the boundary have dimension less than n. The weak topology of the composite combines the weak topologies of the two structures, because every closed cell of D lies in D.

Main definitions

• TauCeti.relCWComplexTrans: the CW structure on C relative to E.
• TauCeti.relCWComplexTransCellEquiv: its n-cells are the n-cells of D and of C.

References

• A. Hatcher, Algebraic Topology, Chapter 0 for CW complexes built by attaching cells inductively, and the Appendix, Proposition A.1, for the compactness argument.

@[instance_reducible]

def TauCeti.relCWComplexTrans {X : Type u_1} [TopologicalSpace X] [T2Space X] (C D E : Set X) [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) : Topology.RelCWComplex C E

Composing relative CW complexes. If C is a CW complex relative to D, and D is a CW complex relative to E, then C is a CW complex relative to E, as soon as the part in D of the boundary of each n-cell of C lies in the skeleton skeletonLT D n. Its n-cells are the n-cells of D together with those of C, with the same characteristic maps.

The structure is not an instance: the base of a relative CW complex is an outParam, so C cannot carry one instance for each base.

noncomputable def TauCeti.relCWComplexTransCellEquiv {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) : Topology.RelCWComplex.cell C n ≃ Topology.RelCWComplex.cell D n ⊕ Topology.RelCWComplex.cell C n

The n-cells of C relative to E are the n-cells of D together with the n-cells of C.

@[simp]

theorem TauCeti.map_relCWComplexTrans_inl {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) (i : Topology.RelCWComplex.cell D n) : Topology.RelCWComplex.map n ((relCWComplexTransCellEquiv h n).symm (Sum.inl i)) = Topology.RelCWComplex.map n i

The characteristic map of a cell of D, as a cell of C relative to E, is its characteristic map in D.

@[simp]

theorem TauCeti.map_relCWComplexTrans_inr {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.map n ((relCWComplexTransCellEquiv h n).symm (Sum.inr i)) = Topology.RelCWComplex.map n i

The characteristic map of a cell of C, as a cell of C relative to E, is its characteristic map relative to D.

@[simp]

theorem TauCeti.openCell_relCWComplexTrans_inl {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) (i : Topology.RelCWComplex.cell D n) : Topology.RelCWComplex.openCell n ((relCWComplexTransCellEquiv h n).symm (Sum.inl i)) = Topology.RelCWComplex.openCell n i

The open cells of C relative to E coming from D are the open cells of D.

@[simp]

theorem TauCeti.openCell_relCWComplexTrans_inr {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n ((relCWComplexTransCellEquiv h n).symm (Sum.inr i)) = Topology.RelCWComplex.openCell n i

The open cells of C relative to E coming from C are the open cells of C relative to D.

@[simp]

theorem TauCeti.closedCell_relCWComplexTrans_inl {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) (i : Topology.RelCWComplex.cell D n) : Topology.RelCWComplex.closedCell n ((relCWComplexTransCellEquiv h n).symm (Sum.inl i)) = Topology.RelCWComplex.closedCell n i

The closed cells of C relative to E coming from D are the closed cells of D.

@[simp]

theorem TauCeti.closedCell_relCWComplexTrans_inr {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.closedCell n ((relCWComplexTransCellEquiv h n).symm (Sum.inr i)) = Topology.RelCWComplex.closedCell n i

The closed cells of C relative to E coming from C are the closed cells of C relative to D.

@[simp]

theorem TauCeti.cellFrontier_relCWComplexTrans_inl {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) (i : Topology.RelCWComplex.cell D n) : Topology.RelCWComplex.cellFrontier n ((relCWComplexTransCellEquiv h n).symm (Sum.inl i)) = Topology.RelCWComplex.cellFrontier n i

The boundaries of the cells of C relative to E coming from D are the boundaries of the cells of D.

@[simp]

theorem TauCeti.cellFrontier_relCWComplexTrans_inr {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D E : Set X} [Topology.RelCWComplex C D] [Topology.RelCWComplex D E] (h : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ∩ D ⊆ ↑(Topology.RelCWComplex.skeletonLT D ↑n)) (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n ((relCWComplexTransCellEquiv h n).symm (Sum.inr i)) = Topology.RelCWComplex.cellFrontier n i

The boundaries of the cells of C relative to E coming from C are the boundaries of the cells of C relative to D.