The homology of the cellular chain complex

For a relative CW complex (X, A) write Xⁿ for its n-skeleton, so that X⁻¹ = A. This file proves the vanishing results on the relative singular homology of skeleta that drive the comparison of cellular and singular homology, and the first half of that comparison: the homology of the cellular chain complex in degree n is the relative singular homology Hₙ(Xⁿ⁺¹, X⁻¹) of the (n + 1)-skeleton.

• Hₖ(Xⁿ, Xⁿ⁻¹) = 0 for k ≠ n (TauCeti.isZero_singularHomology_skeletonPair_of_ne): the characteristic maps identify this group with the relative homology of a disjoint union of disk pairs (Dⁿ, Sⁿ⁻¹), which vanishes outside degree n.
• Hₖ(Xⁿ, X⁻¹) = 0 for n < k (TauCeti.isZero_singularHomology_skeletonBasePair_of_lt), by induction on n along the long exact sequences of the triples (Xⁿ⁺¹, Xⁿ, X⁻¹).
• The cellular differential Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹) factors as the connecting morphism TauCeti.skeletonBaseTripleδ of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹) followed by the map Hₙ(Xⁿ, X⁻¹) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹) induced by the identity of Xⁿ (TauCeti.cellularDifferential_eq_skeletonBaseTripleδ_comp_singularHomologyMap). The second map is a monomorphism, because Hₙ(Xⁿ⁻¹, X⁻¹) = 0.
• Hence the cellular cycles in degree n are Hₙ(Xⁿ, X⁻¹) (TauCeti.cellularCyclesIso) and the cellular boundaries are the image of TauCeti.skeletonBaseTripleδ. Since Hₙ(Xⁿ⁺¹, Xⁿ) = 0, the exact sequence of the triple (TauCeti.skeletonBaseTriple_singularHomology_exact_inner) identifies the cellular homology in degree n with Hₙ(Xⁿ⁺¹, X⁻¹) (TauCeti.cellularHomologyIso). Both identifications come from a left homology datum of the short complex of the cellular chain complex in degree n.

The base X⁻¹ is skeletonLT C 0, which is the base of the complex by TauCeti.range_skeletonBasePair_snd; using it keeps the pair (X⁰, X⁻¹) identical to the skeletal pair TauCeti.skeletonPair C 0.

Coefficients are an object R of an abelian category with coproducts in which coproducts indexed by the cells of each dimension are exact, as for modules over a ring, or for any abelian category when the complex has finitely many cells in each dimension.

References

• A. Hatcher, Algebraic Topology, Section 2.2, Lemma 2.34 and the proof of Theorem 2.35.

theorem TauCeti.isZero_singularHomology_skeletonPair_of_ne {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {n k : ℕ} [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C n)) A] (hk : k ≠ n) : CategoryTheory.Limits.IsZero ((skeletonPair C n).singularHomology R k)

The relative homology of consecutive skeleta vanishes outside the degree of their cells: Hₖ(Xⁿ, Xⁿ⁻¹) = 0 for k ≠ n, when coproducts indexed by the n-cells are exact.

instance TauCeti.isIso_singularHomologyMap_skeletonBasePairToSkeletonPair_zero {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (k : ℕ) : CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C 0) R k)

In degree 0 the map Hₖ(X⁰, X⁻¹) ⟶ Hₖ(X⁰, X⁻¹) induced by TauCeti.skeletonBasePairToSkeletonPair is an isomorphism, being the identity.

noncomputable def TauCeti.skeletonBaseTripleδ {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : cellularChainGroup C R (n + 1) ⟶ (skeletonBasePair C n).singularHomology R n

The connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, X⁻¹) of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹).

Equations

• TauCeti.skeletonBaseTripleδ C R n = (TauCeti.skeletonBaseTriple C n).singularHomologyδ R (n + 1) n ⋯

theorem TauCeti.skeletonBaseTripleδ_def {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : skeletonBaseTripleδ C R n = (skeletonBaseTriple C n).singularHomologyδ R (n + 1) n ⋯

TauCeti.skeletonBaseTripleδ is the connecting morphism of the triple TauCeti.skeletonBaseTriple C n.

@[simp]

theorem TauCeti.skeletonBaseTripleδ_comp_singularHomologyMap_skeletonBasePairToSucc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (skeletonBaseTripleδ C R n) (TopPair.singularHomologyMap (skeletonBasePairToSucc C n) R n) = 0

The connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, X⁻¹) followed by the map Hₙ(Xⁿ, X⁻¹) ⟶ Hₙ(Xⁿ⁺¹, X⁻¹) is zero.

@[simp]

theorem TauCeti.skeletonBaseTripleδ_comp_singularHomologyMap_skeletonBasePairToSucc_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) {Z : A} (h : (skeletonBasePair C (n + 1)).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (skeletonBaseTripleδ C R n) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairToSucc C n) R n) h) = CategoryTheory.CategoryStruct.comp 0 h

The connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, X⁻¹) followed by the map Hₙ(Xⁿ, X⁻¹) ⟶ Hₙ(Xⁿ⁺¹, X⁻¹) is zero.

@[simp]

theorem TauCeti.singularHomologyMap_skeletonBasePairToSkeletonPair_comp_skeletonBaseTripleδ {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C (n + 1)) R (n + 1)) (skeletonBaseTripleδ C R n) = 0

The map Hₙ₊₁(Xⁿ⁺¹, X⁻¹) ⟶ Hₙ₊₁(Xⁿ⁺¹, Xⁿ) followed by the connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, X⁻¹) is zero.

@[simp]

theorem TauCeti.singularHomologyMap_skeletonBasePairToSkeletonPair_comp_skeletonBaseTripleδ_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) {Z : A} (h : (skeletonBasePair C n).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C (n + 1)) R (n + 1)) (CategoryTheory.CategoryStruct.comp (skeletonBaseTripleδ C R n) h) = CategoryTheory.CategoryStruct.comp 0 h

The map Hₙ₊₁(Xⁿ⁺¹, X⁻¹) ⟶ Hₙ₊₁(Xⁿ⁺¹, Xⁿ) followed by the connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, X⁻¹) is zero.

theorem TauCeti.cellularDifferential_eq_skeletonBaseTripleδ_comp_singularHomologyMap {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : cellularDifferential C R n = CategoryTheory.CategoryStruct.comp (skeletonBaseTripleδ C R n) (TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C n) R n)

The cellular differential Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹) is the connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, X⁻¹) of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹) followed by the map Hₙ(Xⁿ, X⁻¹) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹).

theorem TauCeti.cellularDifferential_eq_skeletonBaseTripleδ_comp_singularHomologyMap_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) {Z : A} (h : cellularChainGroup C R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (cellularDifferential C R n) h = CategoryTheory.CategoryStruct.comp (skeletonBaseTripleδ C R n) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C n) R n) h)

The cellular differential Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹) is the connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, X⁻¹) of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹) followed by the map Hₙ(Xⁿ, X⁻¹) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹).

theorem TauCeti.skeletonBaseTriple_singularHomology_exact_outer {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : { X₁ := (skeletonBasePair C (n + 1)).singularHomology R (n + 1), X₂ := (skeletonPair C (n + 1)).singularHomology R (n + 1), X₃ := (skeletonBasePair C n).singularHomology R n, f := TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C (n + 1)) R (n + 1), g := skeletonBaseTripleδ C R n, zero := ⋯ }.Exact

Exactness at Hₙ₊₁(Xⁿ⁺¹, Xⁿ) in the long exact sequence of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹), stated with the maps of TauCeti.skeletonBasePair.

theorem TauCeti.skeletonBaseTriple_singularHomology_exact_inner {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : { X₁ := cellularChainGroup C R (n + 1), X₂ := (skeletonBasePair C n).singularHomology R n, X₃ := (skeletonBasePair C (n + 1)).singularHomology R n, f := skeletonBaseTripleδ C R n, g := TopPair.singularHomologyMap (skeletonBasePairToSucc C n) R n, zero := ⋯ }.Exact

Exactness at Hₙ(Xⁿ, X⁻¹) in the long exact sequence of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹), stated with the maps of TauCeti.skeletonBasePair.

instance TauCeti.epi_singularHomologyMap_skeletonBasePairToSucc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C (n + 1))) A] : CategoryTheory.Epi (TopPair.singularHomologyMap (skeletonBasePairToSucc C n) R n)

The map Hₙ(Xⁿ, X⁻¹) ⟶ Hₙ(Xⁿ⁺¹, X⁻¹) is an epimorphism: its cokernel embeds in Hₙ(Xⁿ⁺¹, Xⁿ) = 0.

theorem TauCeti.isZero_singularHomology_skeletonBasePair_of_lt {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] {n k : ℕ} (hk : n < k) : CategoryTheory.Limits.IsZero ((skeletonBasePair C n).singularHomology R k)

The homology of a skeleton relative to the base vanishes above its dimension: Hₖ(Xⁿ, X⁻¹) = 0 for n < k.

instance TauCeti.mono_singularHomologyMap_skeletonBasePairToSkeletonPair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) : CategoryTheory.Mono (TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C n) R n)

The map Hₙ(Xⁿ, X⁻¹) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹) is a monomorphism: its kernel is a quotient of Hₙ(Xⁿ⁻¹, X⁻¹) = 0.

noncomputable def TauCeti.cellularCyclesIso {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) : HomologicalComplex.cycles (cellularChainComplex C R) n ≅ (skeletonBasePair C n).singularHomology R n

The cycles of the cellular chain complex in degree n are Hₙ(Xⁿ, X⁻¹).

Equations

• TauCeti.cellularCyclesIso C R n = HomologicalComplex.cyclesIsoSc' (TauCeti.cellularChainComplex C R) (n + 1) n (n - 1) ⋯ ⋯ ≪≫ (TauCeti.cellularLeftHomologyData✝ C R n).cyclesIso

@[simp]

theorem TauCeti.cellularCyclesIso_inv_comp_iCycles {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) : CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).inv (HomologicalComplex.iCycles (cellularChainComplex C R) n) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C n) R n) (CategoryTheory.eqToHom ⋯)

Under TauCeti.cellularCyclesIso, the inclusion of the cellular cycles into the cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) is induced by the map of pairs (Xⁿ, X⁻¹) ⟶ (Xⁿ, Xⁿ⁻¹).

@[simp]

theorem TauCeti.cellularCyclesIso_inv_comp_iCycles_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) {Z : A} (h : (cellularChainComplex C R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (cellularChainComplex C R) n) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairToSkeletonPair C n) R n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

Under TauCeti.cellularCyclesIso, the inclusion of the cellular cycles into the cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) is induced by the map of pairs (Xⁿ, X⁻¹) ⟶ (Xⁿ, Xⁿ⁻¹).

noncomputable def TauCeti.cellularHomologyIso {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) : HomologicalComplex.homology (cellularChainComplex C R) n ≅ (skeletonBasePair C (n + 1)).singularHomology R n

The homology of the cellular chain complex in degree n is the relative singular homology Hₙ(Xⁿ⁺¹, X⁻¹) of the (n + 1)-skeleton relative to the base.

Equations

• TauCeti.cellularHomologyIso C R n = HomologicalComplex.homologyIsoSc' (TauCeti.cellularChainComplex C R) (n + 1) n (n - 1) ⋯ ⋯ ≪≫ (TauCeti.cellularLeftHomologyData✝ C R n).homologyIso

@[simp]

theorem TauCeti.homologyπ_comp_cellularHomologyIso_hom {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (cellularChainComplex C R) n) (cellularHomologyIso C R n).hom = CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).hom (TopPair.singularHomologyMap (skeletonBasePairToSucc C n) R n)

Under TauCeti.cellularCyclesIso and TauCeti.cellularHomologyIso, the projection from the cellular cycles to the cellular homology is induced by the inclusion (Xⁿ, X⁻¹) ⟶ (Xⁿ⁺¹, X⁻¹).

@[simp]

theorem TauCeti.homologyπ_comp_cellularHomologyIso_hom_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (n : ℕ) {Z : A} (h : (skeletonBasePair C (n + 1)).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (cellularChainComplex C R) n) (CategoryTheory.CategoryStruct.comp (cellularHomologyIso C R n).hom h) = CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).hom (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairToSucc C n) R n) h)

Under TauCeti.cellularCyclesIso and TauCeti.cellularHomologyIso, the projection from the cellular cycles to the cellular homology is induced by the inclusion (Xⁿ, X⁻¹) ⟶ (Xⁿ⁺¹, X⁻¹).