The open cells lying between two consecutive skeleta

The points of a relative CW complex that lie in the n-skeleton but not in the (n-1)-skeleton are exactly the points of the open n-cells. This file shows that they form a topological disjoint union of open unit balls, one for each n-cell.

The characteristic map of a cell is, by the definition of a relative CW complex, a bijection of the open unit ball onto the open cell whose inverse is continuous, hence a homeomorphism onto the open cell. The individual open cells are moreover open in the difference of the two skeleta: the complement of one of them there is cut out by the closed set obtained by adjoining all the remaining closed n-cells to the (n-1)-skeleton. Being open, pairwise disjoint and covering, the open n-cells split that difference as a topological sum.

An open cell is in general not open in the complex itself; openness here is relative to the difference of the two skeleta.

Main results

• TauCeti.openCellHomeomorph: the characteristic map of a cell is a homeomorphism from the open unit ball onto the open cell.
• TauCeti.isClosed_skeletonLT_union_iUnion_closedCell: adjoining any family of closed n-cells to the (n-1)-skeleton gives a closed set.
• TauCeti.skeletonLT_succ_diff_skeletonLT: the difference of two consecutive skeleta is the union of the open cells of the top dimension.
• TauCeti.isOpen_preimage_val_openCell: each open n-cell is open in that union.
• TauCeti.iUnionOpenCellHomeomorph: that union is homeomorphic to the disjoint union of one open unit ball for each cell of the top dimension.

References

• A. Hatcher, Algebraic Topology, Chapter 0 and the Appendix "Topology of Cell Complexes".

@[simp]

theorem TauCeti.target_map_eq_openCell {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : (Topology.RelCWComplex.map n i).target = Topology.RelCWComplex.openCell n i

The target of a characteristic map is the corresponding open cell.

theorem TauCeti.map_symm_mem_ball {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) {i : Topology.RelCWComplex.cell C n} {x : X} (hx : x ∈ Topology.RelCWComplex.openCell n i) : ↑(Topology.RelCWComplex.map n i).symm x ∈ Metric.ball 0 1

The inverse of a characteristic map sends a point of the open cell into the open unit ball.

theorem TauCeti.map_map_symm {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) {i : Topology.RelCWComplex.cell C n} {x : X} (hx : x ∈ Topology.RelCWComplex.openCell n i) : ↑(Topology.RelCWComplex.map n i) (↑(Topology.RelCWComplex.map n i).symm x) = x

A characteristic map undoes its inverse on the open cell.

def TauCeti.openCellHomeomorph {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ↑(Metric.ball 0 1) ≃ₜ ↑(Topology.RelCWComplex.openCell n i)

The characteristic map of a cell is a homeomorphism from the open unit ball onto the open cell. Its forward and inverse maps are described by TauCeti.openCellHomeomorph_apply and TauCeti.openCellHomeomorph_symm_apply.

Equations

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

@[simp]

theorem TauCeti.openCellHomeomorph_apply {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) (y : ↑(Metric.ball 0 1)) : ↑((openCellHomeomorph n i) y) = ↑(Topology.RelCWComplex.map n i) ↑y

The homeomorphism onto an open cell is the characteristic map.

@[simp]

theorem TauCeti.openCellHomeomorph_symm_apply {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) (x : ↑(Topology.RelCWComplex.openCell n i)) : ↑((openCellHomeomorph n i).symm x) = ↑(Topology.RelCWComplex.map n i).symm ↑x

The inverse of the homeomorphism onto an open cell is the inverse of the characteristic map.

theorem TauCeti.isClosed_skeletonLT_union_iUnion_closedCell {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) [T2Space X] (J : Set (Topology.RelCWComplex.cell C n)) : IsClosed (↑(Topology.RelCWComplex.skeletonLT C ↑n) ∪ ⋃ j ∈ J, Topology.RelCWComplex.closedCell n j)

Adjoining any family of closed n-cells to the (n-1)-skeleton gives a closed set. Taking the family of all n-cells gives the n-skeleton; the point of the general statement is that omitting some of the cells costs nothing.

theorem TauCeti.skeletonLT_succ_diff_skeletonLT {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) [T2Space X] : ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1)) \ ↑(Topology.RelCWComplex.skeletonLT C ↑n) = ⋃ (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.openCell n i

The difference of two consecutive skeleta is the union of the open cells of the top dimension.

theorem TauCeti.mem_skeletonLT_of_forall_notMem_openCell {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) [T2Space X] {x : X} (hx : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) (h : ∀ (j : Topology.RelCWComplex.cell C n), x ∉ Topology.RelCWComplex.openCell n j) : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑n)

A point of skeletonLT C (n + 1) that lies in no open n-cell lies in skeletonLT C n.

theorem TauCeti.isOpen_preimage_val_openCell {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) [T2Space X] (i : Topology.RelCWComplex.cell C n) : IsOpen (Subtype.val ⁻¹' Topology.RelCWComplex.openCell n i)

Each open n-cell is open in the union of all open n-cells: its complement there is cut out by the closed set obtained by adjoining the remaining closed n-cells to the (n-1)-skeleton.

noncomputable def TauCeti.iUnionOpenCellHomeomorph {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) [T2Space X] : (_ : Topology.RelCWComplex.cell C n) × ↑(Metric.ball 0 1) ≃ₜ ↑(⋃ (k : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.openCell n k)

The open n-cells form a topological disjoint union of open balls. This is a homeomorphism from the disjoint union of one open unit ball for each n-cell onto the union of the open n-cells, which by TauCeti.skeletonLT_succ_diff_skeletonLT is the difference of the n-skeleton and the (n-1)-skeleton. Its forward and inverse maps are described by TauCeti.iUnionOpenCellHomeomorph_apply and TauCeti.iUnionOpenCellHomeomorph_symm_apply.

Equations

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

@[simp]

theorem TauCeti.iUnionOpenCellHomeomorph_apply {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) [T2Space X] (p : (_ : Topology.RelCWComplex.cell C n) × ↑(Metric.ball 0 1)) : ↑((iUnionOpenCellHomeomorph n) p) = ↑(Topology.RelCWComplex.map n p.fst) ↑p.snd

The homeomorphism onto the union of the open n-cells is the assembled characteristic map.

theorem TauCeti.iUnionOpenCellHomeomorph_symm_apply {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) [T2Space X] {i : Topology.RelCWComplex.cell C n} {x : ↑(⋃ (k : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.openCell n k)} (hx : ↑x ∈ Topology.RelCWComplex.openCell n i) : (iUnionOpenCellHomeomorph n).symm x = ⟨i, ⟨↑(Topology.RelCWComplex.map n i).symm ↑x, ⋯⟩⟩

The inverse of the homeomorphism onto the union of the open n-cells. A point lying in the open cell i comes from the summand indexed by i, with coordinate its image under the inverse characteristic map of that cell. This is not a simp lemma: the cell i is determined by x only through the hypothesis, so simp could never instantiate it.