Homotopies of maps of topological pairs on singular simplicial sets

A homotopy between maps of topological pairs induces a homotopy between the induced morphisms of the corresponding pairs of singular simplicial sets, that is, an SSetPair.Homotopy. It is given on the subspace and on the ambient space by Mathlib's TopCat.Homotopy.toSSet, and the two agree on the subspace because the homotopy is one of maps of pairs.

noncomputable def TopPair.Homotopy.toSSetPair {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) : SSetPair.Homotopy (TopPair.toSSetPair.map f) (TopPair.toSSetPair.map g)

The homotopy between the induced maps of pairs of singular simplicial sets.

Equations

• H.toSSetPair = { left := H.snd.toSSet, right := H.fst.toSSet, w := ⋯ }

@[simp]

theorem TopPair.Homotopy.toSSetPair_left {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) : H.toSSetPair.left = H.snd.toSSet

@[simp]

theorem TopPair.Homotopy.toSSetPair_right {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) : H.toSSetPair.right = H.fst.toSSet