The torsion of the homology of a mapping torus

Let φ : F ≃ₜ F be a homeomorphism and T_φ its mapping torus, with singular homology taken with coefficients in a commutative ring k. The Wang sequence

Hₙ₊₁(F) ⟶ Hₙ₊₁(F) ⟶ Hₙ₊₁(T_φ) ⟶ Hₙ(F) ⟶ Hₙ(F),

with maps 𝟙 - φ_*, the fibre inclusion and the Wang connecting morphism, identifies the image of the fibre in Hₙ₊₁(T_φ) with the cokernel of 𝟙 - φ_* on Hₙ₊₁(F) (TauCeti.MappingTorus.wangCokernelEquiv).

Suppose k is a domain, Hₙ₊₁(F) is free of finite rank, det (𝟙 - φ_*) ≠ 0 on it, and Hₙ(F) is torsion-free. The cokernel of 𝟙 - φ_* is then killed by det (𝟙 - φ_*), while the quotient of Hₙ₊₁(T_φ) by the image of the fibre embeds in Hₙ(F). Hence the image of the fibre is exactly the torsion submodule of Hₙ₊₁(T_φ). Over a principal ideal domain its Nat.card equals that of k ⧸ (det (𝟙 - φ_*)), and over ℤ it is finite of order |det (𝟙 - φ_*)|.

In degree one the torsion-freeness hypothesis always holds, since H₀(F) is free on the path components of F. When H₁(F; ℤ) is free of finite rank, as for a closed orientable surface, and φ_* has no eigenvalue one on it, this computes the torsion subgroup of H₁(T_φ; ℤ) as the cokernel of 1 - φ_*, and its order as |det (1 - φ_*)|.

Main results

• TauCeti.MappingTorus.torsion_homology_eq_range_homologyMap_fibreInclusionChainMap: the torsion submodule of Hₙ₊₁(T_φ) is the image of the fibre, under the hypotheses above.
• TauCeti.MappingTorus.card_torsion_homology_eq_card_quotient_span_det: over a principal ideal domain, this torsion submodule has the same Nat.card as k ⧸ (det (𝟙 - φ_*)).
• TauCeti.MappingTorus.card_torsion_homology_one_eq_natAbs_det: the integral Wang torsion order, #(H₁(T_φ; ℤ))_tors = |det (1 - φ_*)|.

See A. Hatcher, Algebraic Topology, Section 2.2, for the Wang sequence of a mapping torus.

theorem TauCeti.MappingTorus.torsion_homology_le_range_homologyMap_fibreInclusionChainMap {k : Type w} [CommRing k] {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) (n : ℕ) [Module.IsTorsionFree k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) n)] : Submodule.torsion k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧(MappingTorus φ)) (n + 1)) ≤ (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ ↧k) (n + 1))).range

If Hₙ(F) is torsion-free, every torsion class of Hₙ₊₁(T_φ) comes from the fibre: the Wang connecting morphism sends it to a torsion class of Hₙ(F), hence to zero.

theorem TauCeti.MappingTorus.range_homologyMap_fibreInclusionChainMap_le_torsion_homology {k : Type w} [CommRing k] {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) [IsDomain k] (n : ℕ) [Module.Free k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) n)] [Module.Finite k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) n)] (hdet : LinearMap.det (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧k) n)) ≠ 0) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ ↧k) n)).range ≤ Submodule.torsion k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧(MappingTorus φ)) n)

If Hₙ(F) is free of finite rank and det (𝟙 - φ_*) ≠ 0 on it, the image of the fibre in Hₙ(T_φ) is torsion: it is killed by det (𝟙 - φ_*).

theorem TauCeti.MappingTorus.torsion_homology_eq_range_homologyMap_fibreInclusionChainMap {k : Type w} [CommRing k] {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) [IsDomain k] (n : ℕ) [Module.Free k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) (n + 1))] [Module.Finite k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) (n + 1))] [Module.IsTorsionFree k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) n)] (hdet : LinearMap.det (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧k) (n + 1))) ≠ 0) : Submodule.torsion k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧(MappingTorus φ)) (n + 1)) = (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ ↧k) (n + 1))).range

The torsion of the homology of a mapping torus. If Hₙ₊₁(F) is free of finite rank, det (𝟙 - φ_*) ≠ 0 on it and Hₙ(F) is torsion-free, the torsion submodule of Hₙ₊₁(T_φ) is the image of the fibre, which wangCokernelEquiv identifies with the cokernel of 𝟙 - φ_*.

theorem TauCeti.MappingTorus.card_torsion_homology_eq_card_quotient_span_det {k : Type w} [CommRing k] {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) [IsDomain k] [IsPrincipalIdealRing k] (n : ℕ) [Module.Free k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) (n + 1))] [Module.Finite k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) (n + 1))] [Module.IsTorsionFree k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) n)] (hdet : LinearMap.det (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧k) (n + 1))) ≠ 0) : Nat.card ↥(Submodule.torsion k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧(MappingTorus φ)) (n + 1))) = Nat.card (k ⧸ Ideal.span {LinearMap.det (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧k) (n + 1)))})

The order of the torsion of the homology of a mapping torus over a principal ideal domain: under the hypotheses of torsion_homology_eq_range_homologyMap_fibreInclusionChainMap, the torsion submodule of Hₙ₊₁(T_φ) has the same Nat.card as k ⧸ (det (𝟙 - φ_*)). Both sides are 0 when these modules are infinite.

theorem TauCeti.MappingTorus.torsion_homology_one_eq_range_homologyMap_fibreInclusionChainMap {k : Type w} [CommRing k] {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) [IsDomain k] [Module.Free k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) 1)] [Module.Finite k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) 1)] (hdet : LinearMap.det (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧k) 1)) ≠ 0) : Submodule.torsion k ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧(MappingTorus φ)) 1) = (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ ↧k) 1)).range

In degree one, the torsion of H₁(T_φ) is the image of the fibre whenever H₁(F) is free of finite rank and det (𝟙 - φ_*) ≠ 0 on it; no hypothesis on H₀(F) is needed, since it is free.

theorem TauCeti.MappingTorus.card_torsion_homology_one_eq_natAbs_det {F : Type} [TopologicalSpace F] (φ : F ≃ₜ F) [Module.Free ℤ ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj ↧ℤ).obj ↧F) 1)] [Module.Finite ℤ ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj ↧ℤ).obj ↧F) 1)] (hdet : LinearMap.det (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧ℤ) 1)) ≠ 0) : Nat.card ↥(Submodule.torsion ℤ ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj ↧ℤ).obj ↧(MappingTorus φ)) 1)) = (LinearMap.det (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧ℤ) 1))).natAbs

The integral Wang torsion order. If H₁(F; ℤ) is free of finite rank and det (1 - φ_*) ≠ 0 on it, the torsion subgroup of H₁(T_φ; ℤ) has order |det (1 - φ_*)|.