Singular Euler--Poincaré for finite CW pairs

The cellular--singular comparison transfers finite generation and Euler--Poincaré from cellular chains to relative singular homology. For a finite relative CW complex (C, D) and a finite-dimensional coefficient module M over a division ring k, the alternating sum of the dimensions of Hₙ(C, D; M) is dim M times the alternating count of relative cells. The singular homology groups are finite-dimensional and vanish in all sufficiently large degrees, so the sum has finite support.

Finite generation over a noetherian ring needs only finitely many cells in the degree in question, in addition to the finite-dimensional CW structure required by the comparison. Vanishing in a degree with no cells works for any coefficient object in an abelian category with coproducts exact for the cell sets. The ordinary singular homology statements are obtained from the quotient map for the empty subspace, not from a separate comparison.

The source is A. Hatcher, Algebraic Topology, Section 2.2, Theorems 2.35 and 2.44.

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

Relative singular homology of a finite-dimensional CW pair vanishes in any degree in which the relative CW structure has no cells.

theorem TauCeti.eventually_isZero_singularHomology_complexBasePair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [Topology.RelCWComplex.FiniteDimensional C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (R : A) : ∀ᶠ (n : ℕ) in Filter.atTop, CategoryTheory.Limits.IsZero ((complexBasePair C).singularHomology R n)

Relative singular homology of a finite-dimensional CW pair vanishes in all sufficiently large degrees, without any finiteness assumption on the number of cells in each degree.

theorem TauCeti.finite_singularHomology_complexBasePair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [Topology.RelCWComplex.FiniteDimensional C] {k : Type w} [Ring k] (M : ModuleCat k) [IsNoetherianRing k] [Module.Finite k ↑M] (n : ℕ) [Finite (Topology.RelCWComplex.cell C n)] : Module.Finite k ↑((complexBasePair C).singularHomology M n)

Over a noetherian ring, relative singular homology of a finite-dimensional CW pair is finitely generated in each degree with finitely many cells, for finitely generated coefficients.

theorem TauCeti.sum_range_finrank_singularHomology_complexBasePair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [Topology.RelCWComplex.FiniteDimensional C] {k : Type w} [DivisionRing k] (M : ModuleCat k) [Module.Finite k ↑M] {n : ℕ} (hfinite : ∀ i ≤ n, Finite (Topology.RelCWComplex.cell C i)) (hn : IsEmpty (Topology.RelCWComplex.cell C (n + 1))) : ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Module.finrank k ↑((complexBasePair C).singularHomology M i)) = ↑(Module.finrank k ↑M) * ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Nat.card (Topology.RelCWComplex.cell C i))

The truncated singular Euler--Poincaré formula. Only the cells through degree n need be finite; absence of (n + 1)-cells makes the truncated alternating sums agree.

theorem TauCeti.finsum_finrank_singularHomology_complexBasePair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {k : Type w} [DivisionRing k] (M : ModuleCat k) [Module.Finite k ↑M] [Topology.RelCWComplex.Finite C] : ∑ᶠ (i : ℕ), (-1) ^ i * ↑(Module.finrank k ↑((complexBasePair C).singularHomology M i)) = ↑(Module.finrank k ↑M) * cwEulerChar C

Euler--Poincaré for relative singular homology. For a finite relative CW complex, the alternating sum of the dimensions of relative singular homology is the coefficient dimension times the alternating count of relative cells. Both sums have finite support.

theorem TauCeti.finite_singularHomology_of_cwComplex {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {k : Type w} [Ring k] (M : ModuleCat k) [Topology.RelCWComplex.FiniteDimensional C] [IsNoetherianRing k] [Module.Finite k ↑M] (n : ℕ) [Finite (Topology.RelCWComplex.cell C n)] : Module.Finite k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj M).obj ↧↑C)

Over a noetherian ring, ordinary singular homology of a finite-dimensional CW complex is finitely generated in each degree with finitely many cells, for finitely generated coefficients.

theorem TauCeti.finsum_finrank_singularHomology_of_finite_cwComplex {X : Type w} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] {k : Type w} [DivisionRing k] (M : ModuleCat k) [Module.Finite k ↑M] [Topology.RelCWComplex.Finite C] : ∑ᶠ (i : ℕ), (-1) ^ i * ↑(Module.finrank k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj M).obj ↧↑C)) = ↑(Module.finrank k ↑M) * cwEulerChar C

Euler--Poincaré for ordinary singular homology. For a finite CW complex with finite-dimensional coefficients over a division ring, the alternating homology dimensions equal the coefficient dimension times the alternating cell count.