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.{u_2, 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.{u_2, 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.{u_2, 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

@[reducible, inline]

abbrev HomotopicalAlgebra.IsFibrant {C : Type u_1} [CategoryTheory.Category.{u_2, 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.{u_2, 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.{u_2, 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