The singular homology of tori

Over a nontrivial commutative ring k, the torus Tⁿ = (S¹)ⁿ has free homology with rank H_m(Tⁿ; M) = (n choose m) · rank M for a free coefficient module M of finite rank. Splitting off one circle at a time, Tⁿ⁺¹ ≅ S¹ × Tⁿ, and the homology of a product of spaces with free homology is free with ranks given by the Künneth formula (TopCat.free_singularHomology_tensor, TopCat.finrank_singularHomology_tensor), from the homology of the circle (ModuleCat.finrank_singularHomology_sphere) and of a point (ModuleCat.finrank_singularHomology_of_contractibleSpace). In particular, with these freeness instances, TopCat.isIso_singularHomologyKunneth_of_projective_homology shows that the Künneth map H(S¹) ⊗ H(Tⁿ) ⟶ H(S¹ × Tⁿ) is an isomorphism for every n, as an iterated Künneth description of the homology of a torus requires.

The torus is modelled as ι → TopCat.sphere 1 for a finite index type ι, the circle being Mathlib's TopCat.sphere 1.

Main results

• ModuleCat.free_singularHomology_torus and ModuleCat.finrank_singularHomology_torus: the homology of a torus is free, with rank H_m(Tⁿ; M) = (n choose m) · rank M.

References

• A. Hatcher, Algebraic Topology, Section 3.B, the Künneth formula.

instance ModuleCat.free_singularHomology_torus {k : Type w} [CommRing k] (M : ModuleCat k) [Module.Free k ↑M] (ι : Type w) [Finite ι] (m : ℕ) : Module.Free k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) m).obj M).obj ↧(ι → ↑(TopCat.sphere 1)))

The homology of a torus is free: over any commutative ring, the singular homology of Tⁿ = (S¹)ⁿ with coefficients in a free module is free.

instance ModuleCat.finite_singularHomology_torus {k : Type w} [CommRing k] (M : ModuleCat k) [Module.Free k ↑M] [Module.Finite k ↑M] (ι : Type w) [Finite ι] (m : ℕ) : Module.Finite k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) m).obj M).obj ↧(ι → ↑(TopCat.sphere 1)))

The singular homology of a torus with coefficients in a free module of finite rank has finite rank; over the zero ring every module is trivial.

@[simp]

theorem ModuleCat.finrank_singularHomology_torus {k : Type w} [CommRing k] (M : ModuleCat k) [Module.Free k ↑M] [Module.Finite k ↑M] (ι : Type w) [Finite ι] [Nontrivial k] (m : ℕ) : Module.finrank k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) m).obj M).obj ↧(ι → ↑(TopCat.sphere 1))) = (Nat.card ι).choose m * Module.finrank k ↑M

The ranks of the homology of a torus: over a nontrivial commutative ring, with coefficients in a free module M of finite rank, rank H_m(Tⁿ; M) = (n choose m) · rank M, where Tⁿ is the product of n circles. Nontriviality is needed: over the zero ring every module has rank one.