Bifibrant objects

In this file, we introduce the full subcategories CofibrantObject C, FibrantObject C and BifibrantObject C of a model category C which respectively consist of cofibrant objects, fibrant objects, and bifibrant objects, where "bifibrant" means both cofibrant and fibrant.

def HomotopicalAlgebra.cofibrantObjects (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.ObjectProperty C

The property that is satisfied by cofibrant objects. (This is only introduced in order to consider the full subcategory CofibrantObject. Otherwise, the typeclass IsCofibrant is preferred.)

@[reducible, inline]

abbrev HomotopicalAlgebra.CofibrantObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] : Type u

The full subcategory of cofibrant objects.

@[reducible, inline]

abbrev HomotopicalAlgebra.CofibrantObject.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : C) [IsCofibrant X] : CofibrantObject C

Constructor for CofibrantObject C.

theorem HomotopicalAlgebra.CofibrantObject.mk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : CofibrantObject C) : ∃ (Y : C) (x : IsCofibrant Y), X = mk Y

@[reducible, inline]

abbrev HomotopicalAlgebra.CofibrantObject.homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] (f : X ⟶ Y) : mk X ⟶ mk Y

Constructor for morphisms in CofibrantObject C.

theorem HomotopicalAlgebra.CofibrantObject.homMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] (f : mk X ⟶ mk Y) : ∃ (g : X ⟶ Y), f = homMk g

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.weakEquivalence_homMk_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithWeakEquivalences C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] (f : X ⟶ Y) : WeakEquivalence (homMk f) ↔ WeakEquivalence f

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.homMk_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : C) [IsCofibrant X] : homMk (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (mk X)

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.homMk_homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] {X Y Z : C} [IsCofibrant X] [IsCofibrant Y] [IsCofibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (homMk f) (homMk g) = homMk (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.homMk_homMk_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] {X Y Z : C} [IsCofibrant X] [IsCofibrant Y] [IsCofibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : CofibrantObject C} (h : mk Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (homMk f) (CategoryTheory.CategoryStruct.comp (homMk g) h) = CategoryTheory.CategoryStruct.comp (homMk (CategoryTheory.CategoryStruct.comp f g)) h

@[reducible, inline]

abbrev HomotopicalAlgebra.CofibrantObject.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Functor (CofibrantObject C) C

The inclusion functor CofibrantObject C ⥤ C.

instance HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjCofibrantObjects {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : CofibrantObject C) : IsCofibrant X.obj

instance HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : CofibrantObject C) : IsCofibrant (ι.obj X)

def HomotopicalAlgebra.fibrantObjects (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.ObjectProperty C

The 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.)

@[reducible, inline]

abbrev HomotopicalAlgebra.FibrantObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : Type u

The full subcategory of fibrant objects.

@[reducible, inline]

abbrev HomotopicalAlgebra.FibrantObject.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) [IsFibrant X] : FibrantObject C

Constructor for FibrantObject C.

theorem HomotopicalAlgebra.FibrantObject.mk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : FibrantObject C) : ∃ (Y : C) (x : IsFibrant Y), X = mk Y

@[reducible, inline]

abbrev HomotopicalAlgebra.FibrantObject.homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y : C} [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) : mk X ⟶ mk Y

Constructor for morphisms in FibrantObject C.

theorem HomotopicalAlgebra.FibrantObject.homMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y : C} [IsFibrant X] [IsFibrant Y] (f : mk X ⟶ mk Y) : ∃ (g : X ⟶ Y), f = homMk g

@[simp]

theorem HomotopicalAlgebra.FibrantObject.weakEquivalence_homMk_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [CategoryWithWeakEquivalences C] {X Y : C} [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) : WeakEquivalence (homMk f) ↔ WeakEquivalence f

@[simp]

theorem HomotopicalAlgebra.FibrantObject.homMk_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) [IsFibrant X] : homMk (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (mk X)

@[simp]

theorem HomotopicalAlgebra.FibrantObject.homMk_homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [IsFibrant X] [IsFibrant Y] [IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (homMk f) (homMk g) = homMk (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem HomotopicalAlgebra.FibrantObject.homMk_homMk_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [IsFibrant X] [IsFibrant Y] [IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : FibrantObject C} (h : mk Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (homMk f) (CategoryTheory.CategoryStruct.comp (homMk g) h) = CategoryTheory.CategoryStruct.comp (homMk (CategoryTheory.CategoryStruct.comp f g)) h

@[reducible, inline]

abbrev HomotopicalAlgebra.FibrantObject.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor (FibrantObject C) C

The inclusion functor FibrantObject C ⥤ C.

instance HomotopicalAlgebra.FibrantObject.instIsFibrantObjFibrantObjects {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : FibrantObject C) : IsFibrant X.obj

instance HomotopicalAlgebra.FibrantObject.instIsFibrantObjι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : FibrantObject C) : IsFibrant (ι.obj X)

def HomotopicalAlgebra.bifibrantObjects (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.ObjectProperty C

The property that is satisfied by bifibrant objects, i.e. objects that are both cofibrant and fibrant. (This is only introduced in order to consider the full subcategory BifibrantObject. Otherwise, the typeclasses IsCofibrant and IsFibrant are preferred.)

theorem HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : bifibrantObjects C ≤ cofibrantObjects C

theorem HomotopicalAlgebra.bifibrantObjects_le_fibrantObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : bifibrantObjects C ≤ fibrantObjects C

@[reducible, inline]

abbrev HomotopicalAlgebra.BifibrantObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : Type u

The full subcategory of bifibrant objects.

@[reducible, inline]

abbrev HomotopicalAlgebra.BifibrantObject.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) [IsCofibrant X] [IsFibrant X] : BifibrantObject C

Constructor for BifibrantObject C.

theorem HomotopicalAlgebra.BifibrantObject.mk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : BifibrantObject C) : ∃ (Y : C) (x : IsCofibrant Y) (x_1 : IsFibrant Y), X = mk Y

@[reducible, inline]

abbrev HomotopicalAlgebra.BifibrantObject.homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) : mk X ⟶ mk Y

Constructor for morphisms in BifibrantObject C.

theorem HomotopicalAlgebra.BifibrantObject.homMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : mk X ⟶ mk Y) : ∃ (g : X ⟶ Y), f = homMk g

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.weakEquivalence_homMk_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [CategoryWithWeakEquivalences C] {X Y : C} [IsCofibrant X] [IsFibrant X] [IsCofibrant Y] [IsFibrant Y] (f : X ⟶ Y) : WeakEquivalence (homMk f) ↔ WeakEquivalence f

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.homMk_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) [IsCofibrant X] [IsFibrant X] : homMk (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (mk X)

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.homMk_homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [IsCofibrant X] [IsCofibrant Y] [IsCofibrant Z] [IsFibrant X] [IsFibrant Y] [IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (homMk f) (homMk g) = homMk (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.homMk_homMk_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [IsCofibrant X] [IsCofibrant Y] [IsCofibrant Z] [IsFibrant X] [IsFibrant Y] [IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : BifibrantObject C} (h : mk Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (homMk f) (CategoryTheory.CategoryStruct.comp (homMk g) h) = CategoryTheory.CategoryStruct.comp (homMk (CategoryTheory.CategoryStruct.comp f g)) h

@[reducible, inline]

abbrev HomotopicalAlgebra.BifibrantObject.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor (BifibrantObject C) C

The inclusion functor BifibrantObject C ⥤ C.

instance HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : BifibrantObject C) : IsCofibrant X.obj

instance HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : BifibrantObject C) : IsFibrant X.obj

instance HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : BifibrantObject C) : IsCofibrant (ι.obj X)

instance HomotopicalAlgebra.BifibrantObject.instIsFibrantObjι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : BifibrantObject C) : IsFibrant (ι.obj X)

@[reducible, inline]

abbrev HomotopicalAlgebra.BifibrantObject.ιCofibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor (BifibrantObject C) (CofibrantObject C)

The inclusion BifibrantObject C ⥤ CofibrantObject C.

@[reducible, inline]

abbrev HomotopicalAlgebra.BifibrantObject.ιFibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor (BifibrantObject C) (FibrantObject C)

The inclusion functor BifibrantObject C ⥤ FibrantObject C.

instance HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : BifibrantObject C) : IsCofibrant (ιFibrantObject.obj X).obj

instance HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : BifibrantObject C) : IsFibrant (ιCofibrantObject.obj X).obj