The Euler characteristic from singular cohomology

Over a field k, singular cohomology is the dual of singular homology (TopCat.singularCohomologyDualEquiv). For a space of finite CW type the homology is finite-dimensional and vanishes in large degrees, so the cohomology is finite-dimensional of the same dimension in every degree and also vanishes in large degrees. Hence the Euler characteristic is also the alternating sum of the dimensions of singular cohomology with coefficients in k.

Main declarations

• TauCeti.finite_singularCohomology_of_finiteCWType and TauCeti.eventually_isZero_singularCohomology_of_finiteCWType: over a field, the singular cohomology of a space of finite CW type is finite-dimensional in every degree and vanishes in all large degrees.
• TauCeti.eulerChar_eq_finsum_finrank_singularCohomology: eulerChar X is the alternating sum of the dimensions of the singular cohomology of X over any field.

References

• A. Hatcher, Algebraic Topology, Section 2.2, Theorem 2.44, and Section 3.1, Theorem 3.2.

theorem TauCeti.finite_singularCohomology_of_finiteCWType (X : Type w) [TopologicalSpace X] [FiniteCWType X] (k : Type w) [Field k] (n : ℕ) : Module.Finite k ↑(TopCat.singularCohomology (↧k) k (↧k) (↧X) n)

Over a field, the singular cohomology of a space of finite CW type is finite-dimensional in every degree.

theorem TauCeti.eventually_isZero_singularCohomology_of_finiteCWType (X : Type w) [TopologicalSpace X] [FiniteCWType X] (k : Type w) [Field k] : ∀ᶠ (n : ℕ) in Filter.atTop, CategoryTheory.Limits.IsZero (TopCat.singularCohomology (↧k) k (↧k) (↧X) n)

Over a field, the singular cohomology of a space of finite CW type vanishes in all sufficiently large degrees.

theorem TauCeti.eulerChar_eq_finsum_finrank_singularCohomology (X : Type w) [TopologicalSpace X] [FiniteCWType X] (k : Type w) [Field k] : eulerChar X = ∑ᶠ (i : ℕ), (-1) ^ i * ↑(Module.finrank k ↑(TopCat.singularCohomology (↧k) k (↧k) (↧X) i))

Euler--Poincaré in cohomology for a space of finite CW type: its Euler characteristic is the alternating sum of the dimensions of its singular cohomology over any field.