The Wang sequence of a mapping torus

The long exact sequence of the pair consisting of a mapping torus and one of its fibres gives the Wang sequence. The relative homology identification is the one in TauCeti.MappingTorus.singularHomologyFiberPairIso. The boundary morphism of the pair, under this identification, is id - φ_* followed by the map induced by the fibre inclusion. This file records the exact portion around the homology of the mapping torus, with no restriction on the coefficient object beyond those required for singular homology.

The construction is the mapping-torus sequence of Hatcher, Algebraic Topology, Section 2.2.

The full sequence is also obtained from the short exact sequence of singular chains of the infinite cyclic cover F × ℝ → T_φ (TauCeti.MappingTorus.cyclicCoverShortComplex_shortExact), transported to F along the projection F × ℝ → F. This gives the connecting morphism TauCeti.MappingTorus.wangδ, exactness at all three terms, and surjectivity of the fibre inclusion on degree-zero homology. For a path-connected fibre the monodromy acts trivially on H₀(F), so wangδ is surjective onto H₀(F) (TauCeti.MappingTorus.epi_wangδ_zero). With coefficients in a commutative ring k, exactness identifies the cokernel of 𝟙 - φ_* on Hₙ(F) with the image of the fibre in Hₙ(T_φ) (TauCeti.MappingTorus.wangCokernelEquiv).

noncomputable def TauCeti.MappingTorus.wangInclusion {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧F ⟶ ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧(MappingTorus φ)

The map Hₙ(F) ⟶ Hₙ(T) on singular homology induced by the fibre inclusion MappingTorus.incl of a mapping torus.

theorem TauCeti.MappingTorus.wangInclusion_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : wangInclusion φ R n = ((AlgebraicTopology.singularHomologyFunctor A n).obj R).map (TopCat.ofHom (incl φ))

The Wang inclusion is induced by the fibre inclusion.

noncomputable def TauCeti.MappingTorus.wangConnecting {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : ((AlgebraicTopology.singularHomologyFunctor A (n + 1)).obj R).obj ↧(MappingTorus φ) ⟶ ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧F

The connecting map in the Wang sequence, obtained from the pair sequence and the relative homology identification Hₙ₊₁(T, F) ≅ Hₙ(F).

theorem TauCeti.MappingTorus.wangConnecting_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : wangConnecting φ R n = CategoryTheory.CategoryStruct.comp ((fiberPair φ).singularHomologyπ R (n + 1)) (singularHomologyFiberPairIso φ R n).hom

The Wang connecting map is the ambient-to-relative homology map followed by the relative homology identification.

@[simp]

theorem TauCeti.MappingTorus.map_comp_wangConnecting {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor A (n + 1)).obj R).map (TopCat.ofHom (ContinuousMap.subtypeVal (fiber φ)))) (wangConnecting φ R n) = 0

The ambient-to-relative composite of the pair sequence of fiberPair φ vanishes.

@[simp]

theorem TauCeti.MappingTorus.map_comp_wangConnecting_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) {Z : A} (h : ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧F ⟶ Z) : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor A (n + 1)).obj R).map (TopCat.ofHom (ContinuousMap.subtypeVal (fiber φ)))) (CategoryTheory.CategoryStruct.comp (wangConnecting φ R n) h) = CategoryTheory.CategoryStruct.comp 0 h

The ambient-to-relative composite of the pair sequence of fiberPair φ vanishes.

@[simp]

theorem TauCeti.MappingTorus.wangInclusion_comp_wangConnecting {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (wangInclusion φ R (n + 1)) (wangConnecting φ R n) = 0

The map on homology induced by the fibre inclusion, followed by the Wang connecting map, is zero.

@[simp]

theorem TauCeti.MappingTorus.wangInclusion_comp_wangConnecting_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) {Z : A} (h : ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧F ⟶ Z) : CategoryTheory.CategoryStruct.comp (wangInclusion φ R (n + 1)) (CategoryTheory.CategoryStruct.comp (wangConnecting φ R n) h) = CategoryTheory.CategoryStruct.comp 0 h

The map on homology induced by the fibre inclusion, followed by the Wang connecting map, is zero.

theorem TauCeti.MappingTorus.wang_exact_total {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : { X₁ := ((AlgebraicTopology.singularHomologyFunctor A (n + 1)).obj R).obj ↧F, X₂ := ((AlgebraicTopology.singularHomologyFunctor A (n + 1)).obj R).obj ↧(MappingTorus φ), X₃ := ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧F, f := wangInclusion φ R (n + 1), g := wangConnecting φ R n, zero := ⋯ }.Exact

The exact portion Hₙ₊₁(F) → Hₙ₊₁(T) → Hₙ(F) of the Wang sequence, transported from the exactness of the pair sequence of fiberPair φ at ambient homology.

noncomputable def TauCeti.MappingTorus.cylinderHomologyIso (F : Type w) [TopologicalSpace F] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧(F × ℝ)) n ≅ HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n

The projection F × ℝ → F is an isomorphism on singular homology, with inverse the inclusion at height zero.

theorem TauCeti.MappingTorus.cylinderHomologyIso_hom (F : Type w) [TopologicalSpace F] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (cylinderHomologyIso F R n).hom = HomologicalComplex.homologyMap (((AlgebraicTopology.singularChainComplexFunctor A).obj R).map (TopCat.ofHom (cylinderHomotopyEquiv F).toFun)) n

The forward map of cylinderHomologyIso is induced by projection onto the fibre.

theorem TauCeti.MappingTorus.cylinderHomologyIso_inv (F : Type w) [TopologicalSpace F] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (cylinderHomologyIso F R n).inv = HomologicalComplex.homologyMap (((AlgebraicTopology.singularChainComplexFunctor A).obj R).map (TopCat.ofHom (cylinderHomotopyEquiv F).invFun)) n

The inverse map of cylinderHomologyIso is induced by inclusion at height zero.

theorem TauCeti.MappingTorus.homologyMap_deckChainMap_comp {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (deckChainMap φ R) n) (cylinderHomologyIso F R n).hom = CategoryTheory.CategoryStruct.comp (cylinderHomologyIso F R n).hom (HomologicalComplex.homologyMap (monodromyChainMap φ R) n)

On homology, the deck transformation of the cylinder corresponds to the monodromy under the projection F × ℝ → F.

theorem TauCeti.MappingTorus.homologyMap_coverChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : HomologicalComplex.homologyMap (coverChainMap φ R) n = CategoryTheory.CategoryStruct.comp (cylinderHomologyIso F R n).hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ R) n)

On homology, the covering map is the projection F × ℝ → F followed by the fibre inclusion.

theorem TauCeti.MappingTorus.homologyMap_id_sub_deckChainMap_comp {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧(F × ℝ)) - deckChainMap φ R) n) (cylinderHomologyIso F R n).hom = CategoryTheory.CategoryStruct.comp (cylinderHomologyIso F R n).hom (HomologicalComplex.homologyMap (wangEndomorphism φ R) n)

The map 𝟙 - φ_* on homology is the map 𝟙 - τ_* of the cylinder, transported along the projection.

noncomputable def TauCeti.MappingTorus.wangδ {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧(MappingTorus φ)) (n + 1) ⟶ HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n

The Wang connecting morphism Hₙ₊₁(T_φ) ⟶ Hₙ(F) of the mapping torus of φ: the connecting morphism of the short exact sequence of chains of the infinite cyclic cover, followed by the projection F × ℝ → F.

theorem TauCeti.MappingTorus.wangδ_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : wangδ φ R n = CategoryTheory.CategoryStruct.comp (⋯.δ (n + 1) n ⋯) (HomologicalComplex.homologyMap (((AlgebraicTopology.singularChainComplexFunctor A).obj R).map (TopCat.ofHom (cylinderHomotopyEquiv F).toFun)) n)

The Wang connecting morphism is the connecting morphism of the cyclic cover followed by the projection F × ℝ → F.

theorem TauCeti.MappingTorus.wangδ_comp_homologyMap_wangEndomorphism {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (wangδ φ R n) (HomologicalComplex.homologyMap (wangEndomorphism φ R) n) = 0

The composite Hₙ₊₁(T_φ) ⟶ Hₙ(F) ⟶ Hₙ(F) of the Wang connecting morphism and 𝟙 - φ_* vanishes.

theorem TauCeti.MappingTorus.wangδ_comp_homologyMap_wangEndomorphism_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) {Z : A} (h : HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (wangδ φ R n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (wangEndomorphism φ R) n) h) = CategoryTheory.CategoryStruct.comp 0 h

The composite Hₙ₊₁(T_φ) ⟶ Hₙ(F) ⟶ Hₙ(F) of the Wang connecting morphism and 𝟙 - φ_* vanishes.

@[simp]

theorem TauCeti.MappingTorus.homologyMap_fibreInclusionChainMap_comp_wangδ {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (fibreInclusionChainMap φ R) (n + 1)) (wangδ φ R n) = 0

The composite Hₙ₊₁(F) ⟶ Hₙ₊₁(T_φ) ⟶ Hₙ(F) of the fibre inclusion and the Wang connecting morphism vanishes.

@[simp]

theorem TauCeti.MappingTorus.homologyMap_fibreInclusionChainMap_comp_wangδ_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) {Z : A} (h : HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (fibreInclusionChainMap φ R) (n + 1)) (CategoryTheory.CategoryStruct.comp (wangδ φ R n) h) = CategoryTheory.CategoryStruct.comp 0 h

The composite Hₙ₊₁(F) ⟶ Hₙ₊₁(T_φ) ⟶ Hₙ(F) of the fibre inclusion and the Wang connecting morphism vanishes.

theorem TauCeti.MappingTorus.wang_exact₁ {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : { X₁ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧(MappingTorus φ)) (n + 1), X₂ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n, X₃ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n, f := wangδ φ R n, g := HomologicalComplex.homologyMap (wangEndomorphism φ R) n, zero := ⋯ }.Exact

Exactness of the Wang sequence at Hₙ(F), after the connecting morphism: Hₙ₊₁(T_φ) ⟶ Hₙ(F) ⟶ Hₙ(F), with maps wangδ and 𝟙 - φ_*.

theorem TauCeti.MappingTorus.wang_exact₂ {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : { X₁ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n, X₂ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n, X₃ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧(MappingTorus φ)) n, f := HomologicalComplex.homologyMap (wangEndomorphism φ R) n, g := HomologicalComplex.homologyMap (fibreInclusionChainMap φ R) n, zero := ⋯ }.Exact

Exactness of the Wang sequence at Hₙ(F), after 𝟙 - φ_*: Hₙ(F) ⟶ Hₙ(F) ⟶ Hₙ(T_φ), with maps 𝟙 - φ_* and the fibre inclusion.

theorem TauCeti.MappingTorus.wang_exact₃ {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : { X₁ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) (n + 1), X₂ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧(MappingTorus φ)) (n + 1), X₃ := HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor A).obj R).obj ↧F) n, f := HomologicalComplex.homologyMap (fibreInclusionChainMap φ R) (n + 1), g := wangδ φ R n, zero := ⋯ }.Exact

Exactness of the Wang sequence at Hₙ₊₁(T_φ): Hₙ₊₁(F) ⟶ Hₙ₊₁(T_φ) ⟶ Hₙ(F), with maps the fibre inclusion and wangδ.

instance TauCeti.MappingTorus.epi_homologyMap_fibreInclusionChainMap_zero {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : CategoryTheory.Epi (HomologicalComplex.homologyMap (fibreInclusionChainMap φ R) 0)

The Wang sequence ends with H₀(F) ⟶ H₀(T_φ) ⟶ 0: the fibre inclusion is surjective on H₀.

instance TauCeti.MappingTorus.epi_wangδ_zero {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [PathConnectedSpace F] : CategoryTheory.Epi (wangδ φ R 0)

The end of the Wang sequence of a mapping torus with path-connected fibre: H₁(T_φ) ⟶ H₀(F) ⟶ 0, that is, the Wang connecting morphism is an epimorphism in degree zero.

theorem TauCeti.MappingTorus.ker_homologyMap_fibreInclusionChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {k : Type w} [CommRing k] (n : ℕ) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ ↧k) n)).ker = (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧k) n)).range

The kernel of the map Hₙ(F) → Hₙ(T_φ) induced by the fibre inclusion is the image of 𝟙 - φ_*.

theorem TauCeti.MappingTorus.range_homologyMap_fibreInclusionChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {k : Type w} [CommRing k] (n : ℕ) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ ↧k) (n + 1))).range = (ModuleCat.Hom.hom (wangδ φ (↧k) n)).ker

The image of the map Hₙ₊₁(F) → Hₙ₊₁(T_φ) induced by the fibre inclusion is the kernel of the Wang connecting morphism Hₙ₊₁(T_φ) → Hₙ(F).

noncomputable def TauCeti.MappingTorus.wangCokernelEquiv {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {k : Type w} [CommRing k] (n : ℕ) : (↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) n) ⧸ (LinearMap.id - ModuleCat.Hom.hom (HomologicalComplex.homologyMap (monodromyChainMap φ ↧k) n)).range) ≃ₗ[k] ↥(ModuleCat.Hom.hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ ↧k) n)).range

The Wang cokernel. The cokernel of 𝟙 - φ_* on Hₙ(F) is isomorphic, through the fibre inclusion, to the image of Hₙ(F) in Hₙ(T_φ).

@[simp]

theorem TauCeti.MappingTorus.coe_wangCokernelEquiv_mk {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {k : Type w} [CommRing k] (n : ℕ) (x : ↑(HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).obj ↧k).obj ↧F) n)) : ↑((wangCokernelEquiv φ n) (Submodule.Quotient.mk x)) = (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (fibreInclusionChainMap φ ↧k) n)) x

The Wang cokernel isomorphism sends the class of x to the image of x under the fibre inclusion.