Euler--Poincaré for cellular chains

For a relative CW complex (X, A) and a coefficient module M over a ring k, the cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹; M) is the direct sum of one copy of M for each n-cell (TauCeti.cellularChainGroupIso). This file draws the numerical and finiteness consequences.

• The Euler characteristic of a relative CW complex is the alternating count of its cells (TauCeti.cwEulerChar).
• The cellular chain group is free when M is, finitely generated when M is and there are finitely many n-cells, and then has rank #(n-cells) · rank M (TauCeti.finrank_cellularChainGroup).
• Over a noetherian ring, the cellular homology in degree n of a complex with finitely many n-cells is finitely generated when M is (TauCeti.finite_cellularHomology).
• Euler--Poincaré. Over a division ring, for a finite-dimensional coefficient module M and a complex with finitely many cells through degree n, the alternating sum of the dimensions of the cellular homology up to degree n, when there are no (n + 1)-cells, equals dim M times the alternating count of the cells of dimension at most n (TauCeti.sum_range_finrank_cellularHomology). For a finite complex this is the equality of the homology Euler characteristic of the cellular chain complex with dim M times the alternating count of all cells, dim M · cwEulerChar C (TauCeti.homologyEulerChar_cellularChainComplex).

The statements concern the cellular chain complex itself; its identification with singular homology is what turns them into statements about the space. The coefficient ring lives in the universe of the space, where Mathlib provides the exactness of coproducts of modules that TauCeti.cellularChainGroupIso needs.

References

• A. Hatcher, Algebraic Topology, Section 2.2, Theorem 2.44.

noncomputable def TauCeti.cwEulerChar {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : ℤ

The Euler characteristic of a relative CW complex (C, D): the alternating count ∑ₙ (-1)ⁿ · #(n-cells) of its relative cells. It is meant for finite complexes, where the sum has finite support; for an absolute CW complex it is the Euler characteristic of C.

Equations

• TauCeti.cwEulerChar C = ∑ᶠ (n : ℕ), (-1) ^ n * ↑(Nat.card (Topology.RelCWComplex.cell C n))

theorem TauCeti.cwEulerChar_def {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : cwEulerChar C = ∑ᶠ (n : ℕ), (-1) ^ n * ↑(Nat.card (Topology.RelCWComplex.cell C n))

instance TauCeti.free_cellularChainGroup {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {k : Type w} [Ring k] (M : ModuleCat k) [Module.Free k ↑M] (n : ℕ) : Module.Free k ↑(cellularChainGroup C M n)

With free coefficients, the cellular chain groups are free.

instance TauCeti.finite_cellularChainGroup {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {k : Type w} [Ring k] (M : ModuleCat k) [Module.Finite k ↑M] (n : ℕ) [Finite (Topology.RelCWComplex.cell C n)] : Module.Finite k ↑(cellularChainGroup C M n)

With finitely generated coefficients, the cellular chain group in a degree with finitely many cells is finitely generated.

theorem TauCeti.finrank_cellularChainGroup {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {k : Type w} [Ring k] (M : ModuleCat k) [StrongRankCondition k] [Module.Free k ↑M] [Module.Finite k ↑M] (n : ℕ) [Finite (Topology.RelCWComplex.cell C n)] : Module.finrank k ↑(cellularChainGroup C M n) = Nat.card (Topology.RelCWComplex.cell C n) * Module.finrank k ↑M

The rank of the cellular chain group in degree n is the number of n-cells times the rank of the coefficient module.

theorem TauCeti.finite_cellularHomology {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {k : Type w} [Ring k] (M : ModuleCat k) [IsNoetherianRing k] [Module.Finite k ↑M] (n : ℕ) [Finite (Topology.RelCWComplex.cell C n)] : Module.Finite k ↑(HomologicalComplex.homology (cellularChainComplex C M) n)

Over a noetherian ring, with finitely generated coefficients, the cellular homology in a degree with finitely many cells is finitely generated.

theorem TauCeti.sum_range_finrank_cellularHomology {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {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 ↑(HomologicalComplex.homology (cellularChainComplex C M) i)) = ↑(Module.finrank k ↑M) * ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Nat.card (Topology.RelCWComplex.cell C i))

Euler--Poincaré for cellular chains. For a relative CW complex with finitely many cells through degree n and a finite-dimensional coefficient module M, if there are no (n + 1)-cells, then the alternating sum of the dimensions of the cellular homology groups in degrees at most n is dim M times the alternating count of the cells of dimension at most n.

theorem TauCeti.eulerChar_cellularChainComplex {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {k : Type w} [DivisionRing k] (M : ModuleCat k) [Module.Finite k ↑M] [Topology.RelCWComplex.Finite C] : HomologicalComplex.eulerChar (cellularChainComplex C M) = ↑(Module.finrank k ↑M) * cwEulerChar C

The Euler characteristic of the cellular chain complex of a finite relative CW complex is dim M times the alternating count of its cells.

theorem TauCeti.homologyEulerChar_cellularChainComplex {X : Type w} [TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {k : Type w} [DivisionRing k] (M : ModuleCat k) [Module.Finite k ↑M] [Topology.RelCWComplex.Finite C] : HomologicalComplex.homologyEulerChar (cellularChainComplex C M) = ↑(Module.finrank k ↑M) * cwEulerChar C

Euler--Poincaré for a finite relative CW complex. The alternating sum of the dimensions of the cellular homology groups of a finite relative CW complex, with coefficients in a finite-dimensional module M, is dim M times the alternating count of its cells.