Theorems · Definition · category theory
HomotopicalAlgebra.fibrantObjects
(C : Type u) →
[inst : CategoryTheory.Category.{v, u} C] →
[HomotopicalAlgebra.CategoryWithFibrations C] →
[CategoryTheory.Limits.HasTerminal C] → CategoryTheory.ObjectProperty CThe property that is satisfied by fibrant objects.
(This is only introduced in order to consider the full subcategory
FibrantObject. Otherwise, the typeclass IsFibrant
is preferred.)
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.ObjectPropertystatement · cited by 798
- CategoryTheory.Limits.HasTerminalstatement and proof · cited by 142
- HomotopicalAlgebra.IsFibrantproof · cited by 56
- HomotopicalAlgebra.CategoryWithFibrationsstatement and proof · cited by 46
Cited by40
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.bifibrantObjectsproof · cited by 37
- HomotopicalAlgebra.FibrantObjectproof · cited by 21
- HomotopicalAlgebra.FibrantObject.homRelstatement · cited by 12
- HomotopicalAlgebra.FibrantObject.homMkstatement · cited by 8
- HomotopicalAlgebra.FibrantObject.toHoCatstatement · cited by 8
- HomotopicalAlgebra.FibrantObject.ιstatement and proof · cited by 2
- HomotopicalAlgebra.BifibrantObject.ιFibrantObjectstatement · cited by 2
- HomotopicalAlgebra.FibrantObject.HoCat.resolutionstatement · cited by 2
- HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObjectstatement · cited by 2
- HomotopicalAlgebra.FibrantObject.homMk_homMkstatement · cited by 1
- HomotopicalAlgebra.FibrantObject.homRel_equivalence_of_isCofibrant_srcstatement · cited by 1
- HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRelstatement · cited by 1