Degree zero of the cellular chain complex

For an absolute CW complex, the first two stages of the skeletal filtration are the empty space and the space of its zero-cells. Thus its degree-zero cellular group is the ordinary zeroth singular homology of the zero-skeleton. The characteristic points of the zero-cells give a bijection with this skeleton.

The comparison uses the natural quotient map from ordinary to relative singular homology. These identifications are the degree-zero starting point for identifying cellular groups with free modules on cells.

The mathematical source is Hatcher, Algebraic Topology, Section 2.2. The degree-zero homology calculation for totally disconnected spaces is Andrew Yang's AlgebraicTopology.singularHomologyFunctorZeroOfTotallyDisconnectedSpace in Mathlib.

def TauCeti.skeletonPairZeroIso {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] : skeletonPair C 0 ≅ TopPair.incl.obj (skeletonObj C 1)

The degree-zero skeletal pair is isomorphic to the zero-skeleton modulo the empty space.

Equations

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

noncomputable def TauCeti.zeroSkeletonHomologyIso {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : skeletonHomology C R 1 0 ≅ cellularChainGroup C R 0

The degree-zero cellular group is the ordinary zeroth singular homology of the zero-skeleton. The forward map is induced by the quotient from absolute to relative chains.

Equations

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

noncomputable def TauCeti.cellularChainGroupZeroIso {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : cellularChainGroup C R 0 ≅ ∐ fun (x : Topology.RelCWComplex.cell C 0) => R

The degree-zero cellular group of an absolute CW complex is the coproduct of one copy of the coefficient object for each zero-cell.

Equations

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

@[simp]

theorem TauCeti.cellularChainGroupZeroIso_inv_ι {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (i : Topology.RelCWComplex.cell C 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C 0) => R) i) (cellularChainGroupZeroIso C R).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : ↑(skeletonObj C 1)) => R) (zeroCellPoint C i)) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.singularHomologyFunctorZeroOfTotallyDisconnectedSpace A R (skeletonObj C 1)).inv (zeroSkeletonHomologyIso C R).hom)

The inverse degree-zero identification sends the generator of a zero-cell to the homology class of its characteristic point in the zero-skeleton, then to the skeletal pair. The middle inverse is Mathlib's identification of zeroth homology of a discrete space with its point basis.