Singular-homology homotopy invariance from a prism operator

Defines the abstract proposition SingularPrismOperator and derives the standard homotopy invariance statements for integral singular homology from it. A concrete proof is exported as singularPrismOperator by SingularHomologyHomotopyInvariance.lean; this module remains the reusable conditional API.

def SphereOddDegree.SingularPrismOperator : Prop

The prism-operator hypothesis (the required keystone).

A SingularPrismOperator is the assertion that every topological homotopy between two TopCat maps gives rise to a chain homotopy of the induced integral singular chain maps. This is precisely the classical prism operator P_n : C_n(X) → C_{n+1}(Y) with ∂P + P∂ = g_# − f_#, the one ingredient of homotopy invariance of singular homology not provided by the pinned Mathlib version (the topological half is built in PrismOperator.lean as cylinder).

It is phrased as a Prop (using Nonempty of the chain-homotopy data) so it can be assumed cleanly as a hypothesis; this suffices for every homology-level equality below, which are propositions.

Equations

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

theorem SphereOddDegree.singularHomologyMap_eq_of_homotopy (prism : SingularPrismOperator) {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) (n : ℕ) : (singularHomologyℤ n).map f = (singularHomologyℤ n).map g

Conditional homotopy invariance (topological homotopy form).

Assuming the prism operator, a topological homotopy between two TopCat maps f, g : X ⟶ Y induces equal maps on the n-th integral singular homology.

theorem SphereOddDegree.singularHomologyMap_eq_of_homotopic (prism : SingularPrismOperator) {X Y : TopCat} {f g : X ⟶ Y} (h : (TopCat.Hom.hom f).Homotopic (TopCat.Hom.hom g)) (n : ℕ) : (singularHomologyℤ n).map f = (singularHomologyℤ n).map g

Conditional homotopy invariance (Homotopic form).

Assuming the prism operator, homotopic TopCat maps f, g : X ⟶ Y (i.e. ContinuousMap.Homotopic f.hom g.hom) induce equal maps on the n-th integral singular homology.

theorem SphereOddDegree.singularHomologyMap_eq_of_homotopic_continuousMap (prism : SingularPrismOperator) {X Y : TopCat} {f g : C(↑X, ↑Y)} (h : f.Homotopic g) (n : ℕ) : (singularHomologyℤ n).map (TopCat.ofHom f) = (singularHomologyℤ n).map (TopCat.ofHom g)

Conditional homotopy invariance (C(X, Y) interface).

Assuming the prism operator, two homotopic continuous maps f, g : C(X, Y) between topological spaces underlying TopCat objects induce equal maps on the n-th integral singular homology (after the canonical TopCat.ofHom).

theorem SphereOddDegree.singularHomologyFunctor_map_eq_of_homotopic (prism : SingularPrismOperator) {X Y : TopCat} {f g : X ⟶ Y} (h : (TopCat.Hom.hom f).Homotopic (TopCat.Hom.hom g)) (n : ℕ) : ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj ↧ℤ).map f = ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj ↧ℤ).map g

Conditional homotopy invariance (raw functor form).

The same statement as singularHomologyMap_eq_of_homotopic, written directly in terms of AlgebraicTopology.singularHomologyFunctor, for callers that prefer the unfolded functor.