Singular chains of a mapping torus

The fibre of the mapping torus of φ : F ≃ₜ F has a canonical inclusion at height zero. Traversing the cylinder from height zero to height one gives a homotopy from this inclusion after φ to the inclusion itself. This file transfers that homotopy to singular chains and homology, and constructs the resulting map from the mapping cone of id - φ_* to the singular chains of the mapping torus.

Thus the inclusion coequalizes the identity and monodromy maps, first up to chain homotopy and then on homology. Equivalently, its composite with id - φ_* is null-homotopic. The universal property of the mapping cone then gives the chain map which underlies the Wang sequence.

Main declarations

• TauCeti.MappingTorus.singularChainHomotopy: the composite of the monodromy chain map with the fibre-inclusion chain map is chain-homotopic to the fibre-inclusion map.
• TauCeti.MappingTorus.homologyMap_monodromy_comp_incl: the corresponding equality on singular homology.
• TauCeti.MappingTorus.wangEndomorphism: the chain endomorphism id - φ_* of the fibre.
• TauCeti.MappingTorus.homologyMap_monodromyChainMap_zero: on a path-connected fibre the monodromy induces the identity of H₀(F).
• TauCeti.MappingTorus.wangMappingConeMap: the canonical map from the mapping cone of id - φ_* to the singular chains of the mapping torus.
• TauCeti.MappingTorus.wangMappingConeMapOfSemiconj: the functorial map between these cones induced by a map intertwining two monodromies.

The construction follows the mapping-torus derivation of the Wang sequence; see A. Hatcher, Algebraic Topology, Section 2.2. The chain homotopy itself is obtained from Mathlib's homotopy invariance of singular chains, TopCat.Homotopy.singularChainComplexFunctorObjMap.

noncomputable def TauCeti.MappingTorus.monodromyChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F ⟶ ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F

The endomorphism of singular chains induced by the monodromy of a mapping torus.

theorem TauCeti.MappingTorus.monodromyChainMap_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : monodromyChainMap φ R = ((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom { toFun := ⇑φ, continuous_toFun := ⋯ })

The monodromy chain map is the singular-chain functor applied to the monodromy.

noncomputable def TauCeti.MappingTorus.fibreInclusionChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F ⟶ ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus φ)

The map on singular chains induced by inclusion of the fibre at height zero.

theorem TauCeti.MappingTorus.fibreInclusionChainMap_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : fibreInclusionChainMap φ R = ((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom (incl φ))

The fibre-inclusion chain map is the singular-chain functor applied to the fibre inclusion.

noncomputable def TauCeti.MappingTorus.singularChainHomotopy {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : Homotopy (CategoryTheory.CategoryStruct.comp (monodromyChainMap φ R) (fibreInclusionChainMap φ R)) (fibreInclusionChainMap φ R)

The singular-chain map induced by monodromy followed by fibre inclusion is chain-homotopic to the fibre-inclusion chain map.

@[simp]

theorem TauCeti.MappingTorus.singularChainHomotopy_hom {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (i j : ℕ) : (singularChainHomotopy φ R).hom i j = (TopCat.Homotopy.singularChainComplexFunctorObjMap (monodromyHomotopy φ) R).hom i j

The components of the singular-chain homotopy are those induced by the cylinder homotopy.

@[simp]

theorem TauCeti.MappingTorus.homologyMap_monodromy_comp_incl {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (monodromyChainMap φ R) n) (HomologicalComplex.homologyMap (fibreInclusionChainMap φ R) n) = HomologicalComplex.homologyMap (fibreInclusionChainMap φ R) n

On singular homology, the map induced by the fibre inclusion is unchanged after precomposition with the monodromy map.

noncomputable def TauCeti.MappingTorus.wangEndomorphism {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F ⟶ ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F

The Wang endomorphism id - φ_* on the singular chains of the fibre.

theorem TauCeti.MappingTorus.wangEndomorphism_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : wangEndomorphism φ R = CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F) - monodromyChainMap φ R

The Wang endomorphism is the identity minus the monodromy chain map.

@[simp]

theorem TauCeti.MappingTorus.homologyMap_wangEndomorphism {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : HomologicalComplex.homologyMap (wangEndomorphism φ R) n = CategoryTheory.CategoryStruct.id (HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F) n) - HomologicalComplex.homologyMap (monodromyChainMap φ R) n

On homology, the Wang endomorphism is the identity minus the map induced by monodromy.

@[simp]

theorem TauCeti.MappingTorus.homologyMap_monodromyChainMap_zero {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] [PathConnectedSpace F] : HomologicalComplex.homologyMap (monodromyChainMap φ R) 0 = CategoryTheory.CategoryStruct.id (HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F) 0)

On a path-connected fibre the monodromy induces the identity of H₀(F).

noncomputable def TauCeti.MappingTorus.wangNullHomotopy {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : Homotopy (CategoryTheory.CategoryStruct.comp (wangEndomorphism φ R) (fibreInclusionChainMap φ R)) 0

The fibre inclusion after id - φ_* is null-homotopic. The sign is chosen so that the endomorphism on the fibre is literally id - φ_*, rather than its negative.

@[simp]

theorem TauCeti.MappingTorus.wangNullHomotopy_hom {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (i j : ℕ) : (wangNullHomotopy φ R).hom i j = -(singularChainHomotopy φ R).hom i j

The null-homotopy used in the Wang mapping-cone map is the negative of the canonical monodromy homotopy.

@[reducible, inline]

noncomputable abbrev TauCeti.MappingTorus.wangMappingCone {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.Limits.HasBinaryBiproducts C] : ChainComplex C ℕ

The chain-level mapping cone of id - φ_* used in the mapping-cone formulation of the Wang sequence.

noncomputable def TauCeti.MappingTorus.wangMappingConeMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.Limits.HasBinaryBiproducts C] : wangMappingCone φ R ⟶ ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus φ)

The canonical chain map from the mapping cone of id - φ_* to singular chains of the mapping torus. It is induced by fibre inclusion and the canonical monodromy homotopy.

@[simp]

theorem TauCeti.MappingTorus.homotopyCofiber_inr_comp_wangMappingConeMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr (wangEndomorphism φ R)) (wangMappingConeMap φ R) = fibreInclusionChainMap φ R

The Wang mapping-cone map restricts to fibre inclusion on the unsuspended summand.

@[simp]

theorem TauCeti.MappingTorus.homotopyCofiber_inr_comp_wangMappingConeMap_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.Limits.HasBinaryBiproducts C] {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus φ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr (wangEndomorphism φ R)) (CategoryTheory.CategoryStruct.comp (wangMappingConeMap φ R) h) = CategoryTheory.CategoryStruct.comp (fibreInclusionChainMap φ R) h

The Wang mapping-cone map restricts to fibre inclusion on the unsuspended summand.

@[simp]

theorem TauCeti.MappingTorus.homotopyCofiber_inlX_comp_wangMappingConeMap_f {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.Limits.HasBinaryBiproducts C] (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX (wangEndomorphism φ R) i j hij) ((wangMappingConeMap φ R).f j) = -(singularChainHomotopy φ R).hom i j

On the suspended fibre summand, the Wang mapping-cone map is the negative of the canonical monodromy homotopy.

@[simp]

theorem TauCeti.MappingTorus.homotopyCofiber_inlX_comp_wangMappingConeMap_f_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.Limits.HasBinaryBiproducts C] (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) {Z : C} (h : (((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus φ)).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX (wangEndomorphism φ R) i j hij) (CategoryTheory.CategoryStruct.comp ((wangMappingConeMap φ R).f j) h) = CategoryTheory.CategoryStruct.comp (-(singularChainHomotopy φ R).hom i j) h

On the suspended fibre summand, the Wang mapping-cone map is the negative of the canonical monodromy homotopy.

noncomputable def TauCeti.MappingTorus.fibreChainMap {F : Type w} [TopologicalSpace F] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (g : C(F, G)) : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧F ⟶ ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧G

The map on singular chains induced by a map between the fibres of two mapping tori.

theorem TauCeti.MappingTorus.fibreChainMap_def {F : Type w} [TopologicalSpace F] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (g : C(F, G)) : fibreChainMap R g = ((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom g)

The fibre chain map is the singular-chain functor applied to the map of fibres.

noncomputable def TauCeti.MappingTorus.mappingTorusChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus φ) ⟶ ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus ψ)

The map on singular chains induced by a map of mapping tori.

theorem TauCeti.MappingTorus.mappingTorusChainMap_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : mappingTorusChainMap φ R ψ g h = ((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom (map φ ψ g h))

The mapping-torus chain map is the singular-chain functor applied to the map of mapping tori.

theorem TauCeti.MappingTorus.monodromyChainMap_comp_fibreChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : CategoryTheory.CategoryStruct.comp (monodromyChainMap φ R) (fibreChainMap R g) = CategoryTheory.CategoryStruct.comp (fibreChainMap R g) (monodromyChainMap ψ R)

A map intertwining two monodromies gives a commuting square on singular chains.

theorem TauCeti.MappingTorus.monodromyChainMap_comp_fibreChainMap_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) {Z : ChainComplex C ℕ} (h✝ : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧G ⟶ Z) : CategoryTheory.CategoryStruct.comp (monodromyChainMap φ R) (CategoryTheory.CategoryStruct.comp (fibreChainMap R g) h✝) = CategoryTheory.CategoryStruct.comp (fibreChainMap R g) (CategoryTheory.CategoryStruct.comp (monodromyChainMap ψ R) h✝)

A map intertwining two monodromies gives a commuting square on singular chains.

theorem TauCeti.MappingTorus.fibreInclusionChainMap_comp_mappingTorusChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : CategoryTheory.CategoryStruct.comp (fibreInclusionChainMap φ R) (mappingTorusChainMap φ R ψ g h) = CategoryTheory.CategoryStruct.comp (fibreChainMap R g) (fibreInclusionChainMap ψ R)

Fibre inclusion is natural for maps of mapping tori.

theorem TauCeti.MappingTorus.fibreInclusionChainMap_comp_mappingTorusChainMap_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) {Z : ChainComplex C ℕ} (h✝ : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus ψ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (fibreInclusionChainMap φ R) (CategoryTheory.CategoryStruct.comp (mappingTorusChainMap φ R ψ g h) h✝) = CategoryTheory.CategoryStruct.comp (fibreChainMap R g) (CategoryTheory.CategoryStruct.comp (fibreInclusionChainMap ψ R) h✝)

Fibre inclusion is natural for maps of mapping tori.

theorem TauCeti.MappingTorus.wangEndomorphism_comp_fibreChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : CategoryTheory.CategoryStruct.comp (wangEndomorphism φ R) (fibreChainMap R g) = CategoryTheory.CategoryStruct.comp (fibreChainMap R g) (wangEndomorphism ψ R)

The fibre chain map intertwines the Wang endomorphisms id - φ_* and id - ψ_*.

theorem TauCeti.MappingTorus.wangEndomorphism_comp_fibreChainMap_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) {Z : ChainComplex C ℕ} (h✝ : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧G ⟶ Z) : CategoryTheory.CategoryStruct.comp (wangEndomorphism φ R) (CategoryTheory.CategoryStruct.comp (fibreChainMap R g) h✝) = CategoryTheory.CategoryStruct.comp (fibreChainMap R g) (CategoryTheory.CategoryStruct.comp (wangEndomorphism ψ R) h✝)

The fibre chain map intertwines the Wang endomorphisms id - φ_* and id - ψ_*.

noncomputable def TauCeti.MappingTorus.wangArrowHom {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : CategoryTheory.Arrow.mk (wangEndomorphism φ R) ⟶ CategoryTheory.Arrow.mk (wangEndomorphism ψ R)

The commuting square between the Wang endomorphisms associated to a map intertwining monodromies.

noncomputable def TauCeti.MappingTorus.wangMappingConeMapOfSemiconj {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) [CategoryTheory.Limits.HasBinaryBiproducts C] : wangMappingCone φ R ⟶ wangMappingCone ψ R

The map between Wang mapping cones induced by a map intertwining the monodromies.

@[simp]

theorem TauCeti.MappingTorus.homotopyCofiber_inr_comp_wangMappingConeMapOfSemiconj {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr (wangEndomorphism φ R)) (wangMappingConeMapOfSemiconj φ R ψ g h) = CategoryTheory.CategoryStruct.comp (fibreChainMap R g) (HomologicalComplex.homotopyCofiber.inr (wangEndomorphism ψ R))

On the unsuspended fibre summand, the induced map of Wang cones is the fibre chain map.

@[simp]

theorem TauCeti.MappingTorus.homotopyCofiber_inr_comp_wangMappingConeMapOfSemiconj_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) [CategoryTheory.Limits.HasBinaryBiproducts C] {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h✝ : wangMappingCone ψ R ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr (wangEndomorphism φ R)) (CategoryTheory.CategoryStruct.comp (wangMappingConeMapOfSemiconj φ R ψ g h) h✝) = CategoryTheory.CategoryStruct.comp (fibreChainMap R g) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr (wangEndomorphism ψ R)) h✝)

On the unsuspended fibre summand, the induced map of Wang cones is the fibre chain map.

@[simp]

theorem TauCeti.MappingTorus.homotopyCofiber_inlX_comp_wangMappingConeMapOfSemiconj_f {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) [CategoryTheory.Limits.HasBinaryBiproducts C] (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX (wangEndomorphism φ R) i j hij) ((wangMappingConeMapOfSemiconj φ R ψ g h).f j) = CategoryTheory.CategoryStruct.comp ((fibreChainMap R g).f i) (HomologicalComplex.homotopyCofiber.inlX (wangEndomorphism ψ R) i j hij)

On the suspended fibre summand, the induced map of Wang cones is again the fibre chain map.

@[simp]

theorem TauCeti.MappingTorus.homotopyCofiber_inlX_comp_wangMappingConeMapOfSemiconj_f_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {G : Type w} [TopologicalSpace G] (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) [CategoryTheory.Limits.HasBinaryBiproducts C] (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) {Z : C} (h✝ : (wangMappingCone ψ R).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX (wangEndomorphism φ R) i j hij) (CategoryTheory.CategoryStruct.comp ((wangMappingConeMapOfSemiconj φ R ψ g h).f j) h✝) = CategoryTheory.CategoryStruct.comp ((fibreChainMap R g).f i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX (wangEndomorphism ψ R) i j hij) h✝)

On the suspended fibre summand, the induced map of Wang cones is again the fibre chain map.