Combinatorial simplicial homotopy from a topological homotopy (prism, link L4)

This file assembles the library's singular cylinder (SphereOddDegree.cylinder, the simplicial-set homotopy Sing X ⨯ Δ[1] ⟶ Sing Y of a ContinuousMap.Homotopy) into a combinatorial CategoryTheory.SimplicialObject.Homotopy (Sing.map f) (Sing.map g), the data consumed by the backported algebraic prism CategoryTheory.SimplicialObject.Homotopy.toChainHomotopy.

noncomputable def SphereOddDegree.prismH {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) {n : ℕ} (i : Fin (n + 1)) : (TopCat.toSSet.obj X).obj (Opposite.op { len := n }) ⟶ (TopCat.toSSet.obj Y).obj (Opposite.op { len := n + 1 })

The degree-, index- component of the combinatorial simplicial homotopy obtained from the singular cylinder of a topological homotopy.

Equations

• One or more equations did not get rendered due to their size.

theorem SphereOddDegree.toSSet_map_yonedaEquiv {Z : SSet} {m k : ℕ} (θ : { len := m } ⟶ { len := k }) (ψ : SSet.stdSimplex.obj { len := k } ⟶ Z) : (CategoryTheory.ConcreteCategory.hom (Z.map θ.op)) (SSet.yonedaEquiv ψ) = SSet.yonedaEquiv (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map θ) ψ)

SSet naturality of SSet.yonedaEquiv: applying a simplicial operator to a simplex classified by ψ reclassifies it by precomposition.

theorem SphereOddDegree.prismH_apply {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) {n : ℕ} (i : Fin (n + 1)) (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : (CategoryTheory.ConcreteCategory.hom (prismH H i)) x = (CategoryTheory.ConcreteCategory.hom ((cylinder H).app (Opposite.op { len := n + 1 }))) (SSet.yonedaEquiv (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map (SimplexCategory.σ i)) (SSet.yonedaEquiv.symm x)) (SSet.yonedaEquiv.symm (SSet.stdSimplex.objMk₁ i.succ.castSucc))))

Unfolding of prismH via SSet.yonedaEquiv_comp: the prism component is the cylinder applied to the classifying pair simplex.

theorem SphereOddDegree.prod_lift_map {X : TopCat} {m k : ℕ} (θ : { len := m } ⟶ { len := k }) (a : SSet.stdSimplex.obj { len := k } ⟶ TopCat.toSSet.obj X) (b : SSet.stdSimplex.obj { len := k } ⟶ SSet.stdSimplex.obj { len := 1 }) : (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X ⨯ SSet.stdSimplex.obj { len := 1 }).map θ.op)) (SSet.yonedaEquiv (CategoryTheory.Limits.prod.lift a b)) = SSet.yonedaEquiv (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map θ) a) (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map θ) b))

The classifying pair simplex of prismH H i x, mapped by a simplicial operator θ, is the pair simplex with components precomposed by θ.

theorem SphereOddDegree.yonedaEquiv_symm_natural {Z : SSet} {m k : ℕ} (θ : { len := m } ⟶ { len := k }) (t : Z.obj (Opposite.op { len := k })) : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map θ) (SSet.yonedaEquiv.symm t) = SSet.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (Z.map θ.op)) t)

yonedaEquiv.symm naturality: precomposition by a simplicial operator is reindexing of the classified simplex.

theorem SphereOddDegree.objMk₁_zero_eq_const (n : ℕ) : SSet.stdSimplex.objMk₁ 0 = SSet.stdSimplex.const 1 1 (Opposite.op { len := n })

objMk₁ 0 is the degenerate simplex concentrated at vertex 1 of Δ[1].

theorem SphereOddDegree.objMk₁_last_eq_const (n : ℕ) : SSet.stdSimplex.objMk₁ (Fin.last (n + 1)) = SSet.stdSimplex.const 1 0 (Opposite.op { len := n })

objMk₁ (last) is the degenerate simplex concentrated at vertex 0 of Δ[1].

theorem SphereOddDegree.prism_id_zero {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (prismH H 0) (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj Y) 0) = (TopCat.toSSet.map g).app (Opposite.op { len := n })

theorem SphereOddDegree.prism_id_last {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (prismH H (Fin.last n)) (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj Y) (Fin.last (n + 1))) = (TopCat.toSSet.map f).app (Opposite.op { len := n })

theorem SphereOddDegree.prism_id_succ_δ_castSucc_of_lt {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (hij : i ≤ j.castSucc) : CategoryTheory.CategoryStruct.comp (prismH H j.succ) (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj Y) i.castSucc) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) i) (prismH H j)

theorem SphereOddDegree.prism_id_succ_δ_castSucc_succ {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) {n : ℕ} (j : Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (prismH H j.succ) (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj Y) j.castSucc.succ) = CategoryTheory.CategoryStruct.comp (prismH H j.castSucc) (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj Y) j.castSucc.succ)

theorem SphereOddDegree.prism_id_castSucc_δ_succ_of_lt {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (hji : j.castSucc < i) : CategoryTheory.CategoryStruct.comp (prismH H j.castSucc) (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj Y) i.succ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) i) (prismH H j)

theorem SphereOddDegree.prism_id_comp_σ_castSucc_of_le {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) {n : ℕ} (i j : Fin (n + 1)) (hij : i ≤ j) : CategoryTheory.CategoryStruct.comp (prismH H j) (CategoryTheory.SimplicialObject.σ (TopCat.toSSet.obj Y) i.castSucc) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ (TopCat.toSSet.obj X) i) (prismH H j.succ)

theorem SphereOddDegree.prism_id_comp_σ_succ_of_lt {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) {n : ℕ} (i j : Fin (n + 1)) (hji : j ≤ i) : CategoryTheory.CategoryStruct.comp (prismH H j) (CategoryTheory.SimplicialObject.σ (TopCat.toSSet.obj Y) i.succ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ (TopCat.toSSet.obj X) i) (prismH H j.castSucc)

noncomputable def SphereOddDegree.prismHomotopy {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : CategoryTheory.SimplicialObject.Homotopy (TopCat.toSSet.map f) (TopCat.toSSet.map g)

The combinatorial simplicial homotopy between the singular simplicial maps of two homotopic continuous maps, assembled from the singular cylinder.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SphereOddDegree.singularChainHomotopyOfHomotopy {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : Homotopy (singularChainℤ.map f) (singularChainℤ.map g)

The singular prism operator (unconditional). A homotopy of continuous maps induces a chain homotopy between the induced integral singular chain maps. It combines the project's singular cylinder (prismHomotopy) with the backported algebraic prism CategoryTheory.SimplicialObject.Homotopy.toChainHomotopy.

Equations

• SphereOddDegree.singularChainHomotopyOfHomotopy H = ((SphereOddDegree.prismHomotopy H).whiskerRight (CategoryTheory.Limits.sigmaConst.obj ↧ℤ)).toChainHomotopy

noncomputable def SphereOddDegree.singularChainHomotopyOfHomotopyModule (R : Type) [CommRing R] (Mod : ModuleCat R) {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : Homotopy (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj Mod).map f) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj Mod).map g)

The singular prism operator, general coefficients (unconditional). A homotopy of continuous maps induces a chain homotopy between the singular chain maps with coefficients in an arbitrary module Mod : ModuleCat R. This is the coefficient-Mod generalization of singularChainHomotopyOfHomotopy; it is the keystone that discharges the cohomology prism hypothesis. The simplicial homotopy prismHomotopy H is coefficient-independent; whiskering it through sigmaConst.obj Mod and applying the algebraic prism gives the chain homotopy at coefficient Mod.

Equations

• SphereOddDegree.singularChainHomotopyOfHomotopyModule R Mod H = ((SphereOddDegree.prismHomotopy H).whiskerRight (CategoryTheory.Limits.sigmaConst.obj Mod)).toChainHomotopy