Theorems · Definition · category theory
HomotopicalAlgebra.CofibrantObject.toHoCat
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : HomotopicalAlgebra.ModelCategory C] →
CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject C) (HomotopicalAlgebra.CofibrantObject.HoCat C)The quotient functor from the category of cofibrant objects to its homotopy category.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement · cited by 16,252
- HomotopicalAlgebra.ModelCategorystatement and proof · cited by 141
- CategoryTheory.Quotient.functorproof · cited by 41
- HomotopicalAlgebra.CofibrantObjectstatement · cited by 35
- HomotopicalAlgebra.cofibrantObjectsstatement · cited by 34
- HomotopicalAlgebra.CofibrantObject.homRelstatement and proof · cited by 20
- HomotopicalAlgebra.CofibrantObject.HoCatstatement · cited by 17
Cited by22
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObjectproof · cited by 6
- HomotopicalAlgebra.CofibrantObject.HoCat.resolutionproof · cited by 2
- HomotopicalAlgebra.CofibrantObject.HoCat.adjUnitproof · cited by 1
- HomotopicalAlgebra.CofibrantObject.toHoCat_map_eqstatement · cited by 1
- HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_iffstatement · cited by 1
- HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'statement and proof · cited by 1
- HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTransstatement and proof · cited by 1
- HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_appstatement · cited by 0
- HomotopicalAlgebra.CofibrantObject.toHoCatLocalizerMorphismproof · cited by 0
- HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjectivestatement and proof · cited by 0
- HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_mapstatement · cited by 0
- HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assocstatement and proof · cited by 0