Categories with classes of fibrations, cofibrations, weak equivalences

We introduce typeclasses CategoryWithFibrations, CategoryWithCofibrations and CategoryWithWeakEquivalences to express that a category C is equipped with classes of morphisms named "fibrations", "cofibrations" or "weak equivalences".

class HomotopicalAlgebra.CategoryWithFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)

A category with fibrations is a category equipped with a class of morphisms named "fibrations".

• fibrations : CategoryTheory.MorphismProperty C

  the class of fibrations

class HomotopicalAlgebra.CategoryWithCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)

A category with cofibrations is a category equipped with a class of morphisms named "cofibrations".

• cofibrations : CategoryTheory.MorphismProperty C

  the class of cofibrations

class HomotopicalAlgebra.CategoryWithWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)

A category with weak equivalences is a category equipped with a class of morphisms named "weak equivalences".

• weakEquivalences : CategoryTheory.MorphismProperty C

  the class of weak equivalences

def HomotopicalAlgebra.fibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] : CategoryTheory.MorphismProperty C

The class of fibrations in a category with fibrations.

class HomotopicalAlgebra.Fibration {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithFibrations C] : Prop

A morphism f satisfies [Fibration f] if it belongs to fibrations C.

• mem : fibrations C f

theorem HomotopicalAlgebra.fibration_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithFibrations C] : Fibration f ↔ fibrations C f

theorem HomotopicalAlgebra.mem_fibrations {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithFibrations C] [Fibration f] : fibrations C f

def HomotopicalAlgebra.cofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] : CategoryTheory.MorphismProperty C

The class of cofibrations in a category with cofibrations.

class HomotopicalAlgebra.Cofibration {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithCofibrations C] : Prop

A morphism f satisfies [Cofibration f] if it belongs to cofibrations C.

• mem : cofibrations C f

theorem HomotopicalAlgebra.cofibration_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithCofibrations C] : Cofibration f ↔ cofibrations C f

theorem HomotopicalAlgebra.mem_cofibrations {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithCofibrations C] [Cofibration f] : cofibrations C f

def HomotopicalAlgebra.weakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] : CategoryTheory.MorphismProperty C

The class of weak equivalences in a category with weak equivalences.

class HomotopicalAlgebra.WeakEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithWeakEquivalences C] : Prop

A morphism f satisfies [WeakEquivalence f] if it belongs to weakEquivalences C.

• mem : weakEquivalences C f

theorem HomotopicalAlgebra.weakEquivalence_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithWeakEquivalences C] : WeakEquivalence f ↔ weakEquivalences C f

theorem HomotopicalAlgebra.mem_weakEquivalences {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithWeakEquivalences C] [WeakEquivalence f] : weakEquivalences C f

def HomotopicalAlgebra.trivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] : CategoryTheory.MorphismProperty C

A trivial fibration is a morphism that is both a fibration and a weak equivalence.

theorem HomotopicalAlgebra.trivialFibrations_sub_fibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] : trivialFibrations C ≤ fibrations C

theorem HomotopicalAlgebra.trivialFibrations_sub_weakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] : trivialFibrations C ≤ weakEquivalences C

theorem HomotopicalAlgebra.mem_trivialFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] [Fibration f] [WeakEquivalence f] : trivialFibrations C f

theorem HomotopicalAlgebra.mem_trivialFibrations_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] : trivialFibrations C f ↔ Fibration f ∧ WeakEquivalence f

def HomotopicalAlgebra.trivialCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C] : CategoryTheory.MorphismProperty C

A trivial cofibration is a morphism that is both a cofibration and a weak equivalence.

theorem HomotopicalAlgebra.trivialCofibrations_sub_cofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C] : trivialCofibrations C ≤ cofibrations C

theorem HomotopicalAlgebra.trivialCofibrations_sub_weakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C] : trivialCofibrations C ≤ weakEquivalences C

theorem HomotopicalAlgebra.mem_trivialCofibrations {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C] [Cofibration f] [WeakEquivalence f] : trivialCofibrations C f

theorem HomotopicalAlgebra.mem_trivialCofibrations_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C] : trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f