Fibrant and cofibrant objects in a model category

Once a category C has been endowed with a CategoryWithCofibrations C instance, it is possible to define the property IsCofibrant X for any X : C as an abbreviation for Cofibration (initial.to X : ⊥_ C ⟶ X). (Fibrant objects are defined similarly.)

@[reducible, inline]

abbrev HomotopicalAlgebra.IsCofibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : C) : Prop

An object X is cofibrant if ⊥_ C ⟶ X is a cofibration.

Equations

• HomotopicalAlgebra.IsCofibrant X = HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.initial.to X)

theorem HomotopicalAlgebra.isCofibrant_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : C) : IsCofibrant X ↔ Cofibration (CategoryTheory.Limits.initial.to X)

theorem HomotopicalAlgebra.isCofibrant_iff_of_isInitial {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(cofibrations C).RespectsIso] {A X : C} (i : A ⟶ X) (hA : CategoryTheory.Limits.IsInitial A) : IsCofibrant X ↔ Cofibration i

theorem HomotopicalAlgebra.isCofibrant_of_cofibration {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(cofibrations C).IsStableUnderComposition] {X Y : C} (i : X ⟶ Y) [Cofibration i] [hX : IsCofibrant X] : IsCofibrant Y

instance HomotopicalAlgebra.instCofibrationInlOfIsCofibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X Y : C) [(cofibrations C).IsStableUnderCobaseChange] [CategoryTheory.Limits.HasBinaryCoproduct X Y] [hY : IsCofibrant Y] : Cofibration CategoryTheory.Limits.coprod.inl

instance HomotopicalAlgebra.instCofibrationInrOfIsCofibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X Y : C) [(cofibrations C).IsStableUnderCobaseChange] [CategoryTheory.Limits.HasBinaryCoproduct X Y] [hX : IsCofibrant X] : Cofibration CategoryTheory.Limits.coprod.inr

@[reducible, inline]

abbrev HomotopicalAlgebra.IsFibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) : Prop

An object X is fibrant if X ⟶ ⊤_ C is a fibration.

Equations

• HomotopicalAlgebra.IsFibrant X = HomotopicalAlgebra.Fibration (CategoryTheory.Limits.terminal.from X)

theorem HomotopicalAlgebra.isFibrant_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) : IsFibrant X ↔ Fibration (CategoryTheory.Limits.terminal.from X)

theorem HomotopicalAlgebra.isFibrant_iff_of_isTerminal {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(fibrations C).RespectsIso] {X Y : C} (p : X ⟶ Y) (hY : CategoryTheory.Limits.IsTerminal Y) : IsFibrant X ↔ Fibration p

theorem HomotopicalAlgebra.isFibrant_of_fibration {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(fibrations C).IsStableUnderComposition] {X Y : C} (p : X ⟶ Y) [Fibration p] [hY : IsFibrant Y] : IsFibrant X

instance HomotopicalAlgebra.instFibrationFstOfIsFibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X Y : C) [(fibrations C).IsStableUnderBaseChange] [CategoryTheory.Limits.HasBinaryProduct X Y] [hY : IsFibrant Y] : Fibration CategoryTheory.Limits.prod.fst

instance HomotopicalAlgebra.instFibrationSndOfIsFibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X Y : C) [(fibrations C).IsStableUnderBaseChange] [CategoryTheory.Limits.HasBinaryProduct X Y] [hX : IsFibrant X] : Fibration CategoryTheory.Limits.prod.snd