The zero-skeleton of a CW complex

The points of the zero-skeleton correspond to zero-cells. Its topology is discrete, while the preceding skeleton is empty.

def TauCeti.zeroCellPoint {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] (i : Topology.RelCWComplex.cell C 0) : ↥(Topology.RelCWComplex.skeletonLT C ↑1)

The characteristic point of a zero-cell, regarded as a point of the zero-skeleton.

Equations

• TauCeti.zeroCellPoint C i = ⟨↑(Topology.RelCWComplex.map 0 i) ![], ⋯⟩

noncomputable def TauCeti.zeroCellEquiv {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] : Topology.RelCWComplex.cell C 0 ≃ ↥(Topology.RelCWComplex.skeletonLT C ↑1)

The zero-cells are in bijection with the points of the zero-skeleton.

Equations

• TauCeti.zeroCellEquiv C = Equiv.ofBijective (TauCeti.zeroCellPoint C) ⋯

@[simp]

theorem TauCeti.zeroCellEquiv_apply {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] (i : Topology.RelCWComplex.cell C 0) : (zeroCellEquiv C) i = zeroCellPoint C i

instance TauCeti.zeroSkeletonDiscreteTopology {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] : DiscreteTopology ↥(Topology.RelCWComplex.skeletonLT C ↑1)

The zero-skeleton has the discrete topology: each of its cells consists of one point.

instance TauCeti.zeroSkeletonPreviousIsEmpty {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] : IsEmpty ↥(Topology.RelCWComplex.skeletonLT C ↑0)

The stage before the zero-skeleton is empty for an absolute CW complex.