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] [HomotopicalAlgebra.CategoryWithFibrations C] : CategoryTheory.MorphismProperty C

The class of fibrations in a category with fibrations.

Equations

• HomotopicalAlgebra.fibrations C = HomotopicalAlgebra.CategoryWithFibrations.fibrations

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

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

• mem : HomotopicalAlgebra.fibrations C f

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

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

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

The class of cofibrations in a category with cofibrations.

Equations

• HomotopicalAlgebra.cofibrations C = HomotopicalAlgebra.CategoryWithCofibrations.cofibrations

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

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

• mem : HomotopicalAlgebra.cofibrations C f

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

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

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

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

Equations

• HomotopicalAlgebra.weakEquivalences C = HomotopicalAlgebra.CategoryWithWeakEquivalences.weakEquivalences

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

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

• mem : HomotopicalAlgebra.weakEquivalences C f

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

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

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

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

Equations

• HomotopicalAlgebra.trivialFibrations C = HomotopicalAlgebra.fibrations C ⊓ HomotopicalAlgebra.weakEquivalences C

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

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

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

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

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

Equations

• HomotopicalAlgebra.trivialCofibrations C = HomotopicalAlgebra.cofibrations C ⊓ HomotopicalAlgebra.weakEquivalences C

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

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

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