IsCofibrant

📁 Source: Mathlib/AlgebraicTopology/ModelCategory/IsCofibrant.lean

Statistics

Metric	Count
Definitions IsCofibrant, IsFibrant	2
Theorems instCofibrationInlOfIsCofibrant, instCofibrationInrOfIsCofibrant, instFibrationFstOfIsFibrant, instFibrationSndOfIsFibrant, isCofibrant_iff, isCofibrant_iff_of_isInitial, isCofibrant_of_cofibration, isFibrant_iff, isFibrant_iff_of_isTerminal, isFibrant_of_fibration	10
Total	12

HomotopicalAlgebra

Definitions

Name	Category	Theorems
IsCofibrant 📖	MathDef	13 math math: Cylinder.instIsCofibrantI, CofibrantObject.instIsCofibrantObjι, CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, PathObject.instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations, CofibrantObject.instIsCofibrantResolutionObj, isCofibrant_iff, PathObject.instIsCofibrantPOfIsVeryGood, isCofibrant_of_cofibration, BifibrantObject.instIsCofibrantObjBifibrantObjects, BifibrantObject.instIsCofibrantObjι, CofibrantObject.instIsCofibrantObjCofibrantObjects, isCofibrant_iff_of_isInitial
IsFibrant 📖	MathDef	14 math math: isFibrant_iff_of_isTerminal, BifibrantObject.instIsFibrantObjBifibrantObjects, CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations, PathObject.instIsFibrantP, Cylinder.instIsFibrantIOfIsVeryGood, FibrantObject.instIsFibrantObjι, isFibrant_of_fibration, BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, FibrantObject.instIsFibrantResolutionObj, FibrantObject.instIsFibrantObjFibrantObjects, isFibrant_iff, FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, BifibrantObject.instIsFibrantObjι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCofibrationInlOfIsCofibrant 📖	mathematical	—	Cofibration CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.inl	—	cofibration_iff CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPushout.flip CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial isCofibrant_iff
instCofibrationInrOfIsCofibrant 📖	mathematical	—	Cofibration CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.inr	—	cofibration_iff CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial isCofibrant_iff
instFibrationFstOfIsFibrant 📖	mathematical	—	Fibration CategoryTheory.Limits.prod CategoryTheory.Limits.prod.fst	—	fibration_iff CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal isFibrant_iff
instFibrationSndOfIsFibrant 📖	mathematical	—	Fibration CategoryTheory.Limits.prod CategoryTheory.Limits.prod.snd	—	fibration_iff CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal isFibrant_iff
isCofibrant_iff 📖	mathematical	—	IsCofibrant Cofibration CategoryTheory.Limits.initial CategoryTheory.Limits.initial.to	—	—
isCofibrant_iff_of_isInitial 📖	mathematical	—	IsCofibrant Cofibration	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.Limits.IsInitial.to_comp CategoryTheory.Category.comp_id
isCofibrant_of_cofibration 📖	mathematical	—	IsCofibrant	—	isCofibrant_iff Unique.instSubsingleton instCofibrationCompOfIsStableUnderCompositionCofibrations
isFibrant_iff 📖	mathematical	—	IsFibrant Fibration CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from	—	—
isFibrant_iff_of_isTerminal 📖	mathematical	—	IsFibrant Fibration	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.Limits.terminal.comp_from CategoryTheory.Limits.IsTerminal.comp_from
isFibrant_of_fibration 📖	mathematical	—	IsFibrant	—	isFibrant_iff Unique.instSubsingleton instFibrationCompOfIsStableUnderCompositionFibrations

---

← Back to Index