Singular prism construction

Builds the cylinder associated to a continuous homotopy after applying the singular simplicial-set functor. The endpoint identities connect this construction to the algebraic simplicial-homotopy and chain-homotopy machinery used by the singular-homology homotopy-invariance proof.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.unitI : TopCat

The unit interval as an object of TopCat.

Equations

• SphereOddDegree.unitI = ↧↑unitInterval

instance SphereOddDegree.singularPreservesLimits : CategoryTheory.Limits.PreservesLimits TopCat.toSSet

The singular simplicial set functor preserves limits, being a right adjoint (sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet).

noncomputable def SphereOddDegree.constI (X : TopCat) (t : ↑unitInterval) : X ⟶ unitI

The const-valued continuous map X → I at a point t of the interval.

Equations

• SphereOddDegree.constI X t = TopCat.ofHom (ContinuousMap.const (↑X) t)

noncomputable def SphereOddDegree.edgeCM : C(Convexity.StdSimplex ℝ (Fin (1 + 1)), ↑unitI)

The standard topological 1-simplex, viewed (via Convexity.StdSimplex.homeomorphI) as a continuous map into the interval.

Equations

• SphereOddDegree.edgeCM = { toFun := ⇑Convexity.StdSimplex.homeomorphI, continuous_toFun := SphereOddDegree.edgeCM._proof_1 }

noncomputable def SphereOddDegree.edge : SSet.stdSimplex.obj { len := 1 } ⟶ TopCat.toSSet.obj unitI

The singular edge of the interval: the simplicial 1-simplex of Sing I classified by the homeomorphism Δ¹_top ≃ₜ I.

Equations

• SphereOddDegree.edge = SSet.yonedaEquiv.symm ((SphereOddDegree.unitI.toSSetObjEquiv (Opposite.op { len := 1 })).symm SphereOddDegree.edgeCM)

noncomputable def SphereOddDegree.vtx (Z : SSet) (j : Fin 2) : Z ⟶ SSet.stdSimplex.obj { len := 1 }

The const-valued simplicial map onto the j-th vertex of Δ[1].

Equations

• SphereOddDegree.vtx Z j = SSet.const (SSet.stdSimplex.obj₀Equiv.symm j)

noncomputable def SphereOddDegree.homotopyMap {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : X ⨯ unitI ⟶ Y

A ContinuousMap.Homotopy between f.hom and g.hom, repackaged as a single morphism out of the categorical product X ⨯ I. On a point p it is H (snd p, fst p), i.e. H with its interval coordinate first.

Equations

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

noncomputable def SphereOddDegree.cylinder {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : TopCat.toSSet.obj X ⨯ SSet.stdSimplex.obj { len := 1 } ⟶ TopCat.toSSet.obj Y

The singular cylinder map of a homotopy H: Sing X × Δ[1] ⟶ Sing Y, built from the singular edge of the interval, the product-preservation isomorphism Sing X × Sing I ≅ Sing (X × I), and Sing H.

Equations

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

noncomputable def SphereOddDegree.sect (X : TopCat) (j : Fin 2) : TopCat.toSSet.obj X ⟶ TopCat.toSSet.obj X ⨯ SSet.stdSimplex.obj { len := 1 }

The j-th endpoint section Sing X ⟶ Sing X × Δ[1].

Equations

• SphereOddDegree.sect X j = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id (TopCat.toSSet.obj X)) (SphereOddDegree.vtx (TopCat.toSSet.obj X) j)

theorem SphereOddDegree.homotopyMap_zero {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (constI X 0)) (homotopyMap H) = f

At interval coordinate 0, the repackaged homotopy recovers f.

theorem SphereOddDegree.homotopyMap_one {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (constI X 1)) (homotopyMap H) = g

At interval coordinate 1, the repackaged homotopy recovers g.

theorem SphereOddDegree.edge_vtx_zero (X : TopCat) : CategoryTheory.CategoryStruct.comp (vtx (TopCat.toSSet.obj X) 0) edge = TopCat.toSSet.map (constI X 0)

The 0-vertex of Δ[1], pushed along the singular edge, is the const-valued singular map at 0 ∈ I.

theorem SphereOddDegree.edge_vtx_one (X : TopCat) : CategoryTheory.CategoryStruct.comp (vtx (TopCat.toSSet.obj X) 1) edge = TopCat.toSSet.map (constI X 1)

The 1-vertex of Δ[1], pushed along the singular edge, is the const-valued singular map at 1 ∈ I.

theorem SphereOddDegree.lift_const_comp_iso_inv (X : TopCat) (j : ↑unitInterval) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id (TopCat.toSSet.obj X)) (TopCat.toSSet.map (constI X j))) (CategoryTheory.Limits.PreservesLimitPair.iso TopCat.toSSet X unitI).inv = TopCat.toSSet.map (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (constI X j))

Key reduction: the product-comparison inverse turns the lifted const-valued section into Sing of the lifted topological section.

theorem SphereOddDegree.cylinder_sect_zero {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : CategoryTheory.CategoryStruct.comp (sect X 0) (cylinder H) = TopCat.toSSet.map f

Endpoint identity (start). The singular cylinder restricts to Sing f along the start inclusion.

theorem SphereOddDegree.cylinder_sect_one {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : CategoryTheory.CategoryStruct.comp (sect X 1) (cylinder H) = TopCat.toSSet.map g

Endpoint identity (end). The singular cylinder restricts to Sing g along the end inclusion.