Theorems · Definition · algebraic topology
TopCat.Homotopy.toSSet
{X Y : TopCat} → {f g : X ⟶ Y} → TopCat.Homotopy f g → SSet.Homotopy (TopCat.toSSet.map f) (TopCat.toSSet.map g)If two morphisms f : X ⟶ Y and g : X ⟶ Y in TopCat are homotopic, then so
are their images by the functor TopCat.toSSet : TopCat ⥤ SSet.
- Defined in
- Mathlib.Topology.Homotopy.TopCat.ToSSet
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Functor.mapstatement and proof · cited by 8,698
- Oppositestatement · cited by 8,081
- SimplexCategorystatement · cited by 2,204
- TopCatstatement and proof · cited by 1,889
- SSetstatement · cited by 1,283
- CategoryTheory.MonoidalCategoryStruct.whiskerLeftproof · cited by 915
- CategoryTheory.Functor.LaxMonoidal.μproof · cited by 285
- TopCat.Iproof · cited by 64
- TopCat.toSSetstatement and proof · cited by 29
Cited by1
Results whose statement or proof uses this declaration.
- TopCat.Homotopy.singularChainComplexFunctorObjMapproof · cited by 1