Theorems · Definition · algebraic topology
SSet.Truncated.mapHomotopyCategory
{V W : SSet.Truncated 2} → (V ⟶ W) → CategoryTheory.Functor V.HomotopyCategory W.HomotopyCategoryA map of 2-truncated simplicial sets induces a functor between homotopy categories.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 64 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.Functorstatement · cited by 16,252
- CategoryTheory.Functor.mapproof · cited by 8,698
- Oppositestatement · cited by 8,081
- CategoryTheory.Functor.compproof · cited by 6,529
- SimplexCategorystatement · cited by 2,204
- SimplexCategory.lenstatement · cited by 542
- CategoryTheory.Cat.Hom.toFunctorproof · cited by 531
- SimplexCategory.Truncatedstatement · cited by 236
- SSet.Truncatedstatement and proof · cited by 214
- SSet.Truncated.HomotopyCategorystatement · cited by 54
- CategoryTheory.Quotient.liftproof · cited by 11
Cited by21
Results whose statement or proof uses this declaration.
- SSet.Truncated.HomotopyCategory.BinaryProduct.functorproof · cited by 9
- SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIsostatement and proof · cited by 2
- SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_appstatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.idProdMapHomotopyCategoryCompInverseIsostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategoryFstIsostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategorySndIsostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fststatement · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_sndstatement · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategoryProdIdCompInverseIsostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Isostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_appstatement and proof · cited by 1
- SSet.Truncated.hoFunctor₂proof · cited by 0