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

@[implicit_reducible]

instance HomotopicalAlgebra.instCategoryWithFibrationsOpposite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] : CategoryWithFibrations Cᵒᵖ

theorem HomotopicalAlgebra.fibrations_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] : fibrations Cᵒᵖ = (cofibrations C).op

theorem HomotopicalAlgebra.cofibrations_eq_unop (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] : cofibrations C = (fibrations Cᵒᵖ).unop

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

theorem HomotopicalAlgebra.cofibration_unop_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : Cofibration f.unop ↔ Fibration f

instance HomotopicalAlgebra.instFibrationOppositeOpOfCofibration {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithCofibrations C] [Cofibration f] : Fibration f.op

instance HomotopicalAlgebra.instCofibrationUnopOfFibrationOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [Fibration f] : Cofibration f.unop

@[implicit_reducible]

instance HomotopicalAlgebra.instCategoryWithCofibrationsOpposite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] : CategoryWithCofibrations Cᵒᵖ

theorem HomotopicalAlgebra.cofibrations_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] : cofibrations Cᵒᵖ = (fibrations C).op

theorem HomotopicalAlgebra.fibrations_eq_unop (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] : fibrations C = (cofibrations Cᵒᵖ).unop

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

theorem HomotopicalAlgebra.fibration_unop_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : Fibration f.unop ↔ Cofibration f

instance HomotopicalAlgebra.instCofibrationOppositeOpOfFibration {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryWithFibrations C] [Fibration f] : Cofibration f.op

instance HomotopicalAlgebra.instFibrationUnopOfCofibrationOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [Cofibration f] : Fibration f.unop

@[implicit_reducible]

instance HomotopicalAlgebra.instCategoryWithWeakEquivalencesOpposite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] : CategoryWithWeakEquivalences Cᵒᵖ

theorem HomotopicalAlgebra.weakEquivalences_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] : weakEquivalences Cᵒᵖ = (weakEquivalences C).op

theorem HomotopicalAlgebra.weakEquivalences_eq_unop (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] : weakEquivalences C = (weakEquivalences Cᵒᵖ).unop

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

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

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

instance HomotopicalAlgebra.instWeakEquivalenceUnopOfOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [WeakEquivalence f] : WeakEquivalence f.unop

theorem HomotopicalAlgebra.trivialFibrations_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] : trivialFibrations Cᵒᵖ = (trivialCofibrations C).op

theorem HomotopicalAlgebra.trivialCofibrations_eq_unop (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] : trivialCofibrations C = (trivialFibrations Cᵒᵖ).unop

theorem HomotopicalAlgebra.trivialCofibrations_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithFibrations C] : trivialCofibrations Cᵒᵖ = (trivialFibrations C).op

theorem HomotopicalAlgebra.trivialFibrations_eq_unop (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithFibrations C] : trivialFibrations C = (trivialCofibrations Cᵒᵖ).unop

@[implicit_reducible]

instance HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {P : CategoryTheory.ObjectProperty C} : CategoryWithWeakEquivalences P.FullSubcategory

instance HomotopicalAlgebra.instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {P : CategoryTheory.ObjectProperty C} [(weakEquivalences C).HasTwoOutOfThreeProperty] : (weakEquivalences P.FullSubcategory).HasTwoOutOfThreeProperty

instance HomotopicalAlgebra.instIsMultiplicativeFullSubcategoryWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {P : CategoryTheory.ObjectProperty C} [(weakEquivalences C).IsMultiplicative] : (weakEquivalences P.FullSubcategory).IsMultiplicative

theorem HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) : WeakEquivalence f ↔ WeakEquivalence f.hom

instance HomotopicalAlgebra.instWeakEquivalenceHomFullSubcategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) [WeakEquivalence f] : WeakEquivalence f.hom

instance HomotopicalAlgebra.instWeakEquivalenceMapFullSubcategoryι (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) [WeakEquivalence f] : WeakEquivalence (P.ι.map f)