The factorization axiom

In this file, we introduce a type-class HasFactorization W₁ W₂, which, given two classes of morphisms W₁ and W₂ in a category C, asserts that any morphism in C can be factored as a morphism in W₁ followed by a morphism in W₂. The data of such factorizations can be packaged in the type FactorizationData W₁ W₂.

This shall be used in the formalization of model categories for which the CM5 axiom asserts that any morphism can be factored as a cofibration followed by a trivial fibration (or a trivial cofibration followed by a fibration).

We also provide a structure FunctorialFactorizationData W₁ W₂ which contains the data of a functorial factorization as above. With this design, when we formalize certain constructions (e.g. cylinder objects in model categories), we may first construct them using using data : FactorizationData W₁ W₂. Without duplication of code, it shall be possible to show these cylinders are functorial when a term data : FunctorialFactorizationData W₁ W₂ is available, the existence of which is asserted in the type-class HasFunctorialFactorization W₁ W₂.

We also introduce the class W₁.comp W₂ of morphisms of the form i ≫ p with W₁ i and W₂ p and show that W₁.comp W₂ = ⊤ iff HasFactorization W₁ W₂ holds (this is MorphismProperty.comp_eq_top_iff).

structure CategoryTheory.MorphismProperty.MapFactorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) : Type (max u_1 u_2)

Given two classes of morphisms W₁ and W₂ on a category C, this is the data of the factorization of a morphism f : X ⟶ Y as i ≫ p with W₁ i and W₂ p.

• Z : C

  the intermediate object in the factorization

• i : X ⟶ self.Z

  the first morphism in the factorization

• p : self.Z ⟶ Y

  the second morphism in the factorization

• fac : CategoryTheory.CategoryStruct.comp self.i self.p = f
• hi : W₁ self.i
• hp : W₂ self.p

@[simp]

theorem CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y} (self : W₁.MapFactorizationData W₂ f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.p h) = CategoryTheory.CategoryStruct.comp f h

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.FactorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) : Type (max u_1 u_2)

The data of a term in MapFactorizationData W₁ W₂ f for any morphism f.

Equations

• W₁.FactorizationData W₂ = ({X Y : C} → (f : X ⟶ Y) → W₁.MapFactorizationData W₂ f)

class CategoryTheory.MorphismProperty.HasFactorization {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) : Prop

The factorization axiom for two classes of morphisms W₁ and W₂ in a category C. It asserts that any morphism can be factored as a morphism in W₁ followed by a morphism in W₂.

• nonempty_mapFactorizationData : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (W₁.MapFactorizationData W₂ f)

noncomputable def CategoryTheory.MorphismProperty.factorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFactorization W₂] : W₁.FactorizationData W₂

A chosen term in FactorizationData W₁ W₂ when HasFactorization W₁ W₂ holds.

Equations

• W₁.factorizationData W₂ x = ⋯.some

def CategoryTheory.MorphismProperty.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty C

The class of morphisms that are of the form i ≫ p with W₁ i and W₂ p.

Equations

• W₁.comp W₂ f = Nonempty (W₁.MapFactorizationData W₂ f)

theorem CategoryTheory.MorphismProperty.comp_eq_top_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) : W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂

structure CategoryTheory.MorphismProperty.FunctorialFactorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) : Type (max u_1 u_2)

The data of a functorial factorization of any morphism in C as a morphism in W₁ followed by a morphism in W₂.

• Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C

  the intermediate objects in the factorizations

• i : CategoryTheory.Arrow.leftFunc ⟶ self.Z

  the first morphism in the factorizations

• p : self.Z ⟶ CategoryTheory.Arrow.rightFunc

  the second morphism in the factorizations

• fac : CategoryTheory.CategoryStruct.comp self.i self.p = CategoryTheory.Arrow.leftToRight
• hi : ∀ (f : CategoryTheory.Arrow C), W₁ (self.i.app f)
• hp : ∀ (f : CategoryTheory.Arrow C), W₂ (self.p.app f)

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (self : W₁.FunctorialFactorizationData W₂) {Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C} (h : CategoryTheory.Arrow.rightFunc ⟶ Z) : CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.p h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow.leftToRight h

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {f : CategoryTheory.Arrow C} : CategoryTheory.CategoryStruct.comp (data.i.app f) (data.p.app f) = f.hom

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {f : CategoryTheory.Arrow C} {Z : C} (h : CategoryTheory.Arrow.rightFunc.obj f ⟶ Z) : CategoryTheory.CategoryStruct.comp (data.i.app f) (CategoryTheory.CategoryStruct.comp (data.p.app f) h) = CategoryTheory.CategoryStruct.comp f.hom h

def CategoryTheory.MorphismProperty.FunctorialFactorizationData.ofLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {W₁' W₂' : CategoryTheory.MorphismProperty C} (le₁ : W₁ ≤ W₁') (le₂ : W₂ ≤ W₂') : W₁'.FunctorialFactorizationData W₂'

If W₁ ≤ W₁' and W₂ ≤ W₂', then a functorial factorization for W₁ and W₂ induces a functorial factorization for W₁' and W₂'.

Equations

• data.ofLE le₁ le₂ = { Z := data.Z, i := data.i, p := data.p, fac := ⋯, hi := ⋯, hp := ⋯ }

def CategoryTheory.MorphismProperty.FunctorialFactorizationData.factorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) : W₁.FactorizationData W₂

The term in FactorizationData W₁ W₂ that is deduced from a functorial factorization.

Equations

• data.factorizationData f = { Z := data.Z.obj (CategoryTheory.Arrow.mk f), i := data.i.app (CategoryTheory.Arrow.mk f), p := data.p.app (CategoryTheory.Arrow.mk f), fac := ⋯, hi := ⋯, hp := ⋯ }

def CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) : (data.factorizationData f).Z ⟶ (data.factorizationData g).Z

When data : FunctorialFactorizationData W₁ W₂, this is the morphism (data.factorizationData f).Z ⟶ (data.factorizationData g).Z expressing the functoriality of the intermediate objects of the factorizations for φ : Arrow.mk f ⟶ Arrow.mk g.

Equations

• data.mapZ φ = data.Z.map φ

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) : CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (data.mapZ φ) = CategoryTheory.CategoryStruct.comp φ.left (data.factorizationData g).i

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {Z : C} (h : (data.factorizationData g).Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (CategoryTheory.CategoryStruct.comp (data.mapZ φ) h) = CategoryTheory.CategoryStruct.comp φ.left (CategoryTheory.CategoryStruct.comp (data.factorizationData g).i h)

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) : CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.factorizationData g).p = CategoryTheory.CategoryStruct.comp (data.factorizationData f).p φ.right

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {Z : C} (h : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (data.mapZ φ) (CategoryTheory.CategoryStruct.comp (data.factorizationData g).p h) = CategoryTheory.CategoryStruct.comp (data.factorizationData f).p (CategoryTheory.CategoryStruct.comp φ.right h)

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y : C} (f : X ⟶ Y) : data.mapZ (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f)) = CategoryTheory.CategoryStruct.id (data.factorizationData f).Z

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {X'' Y'' : C} {h : X'' ⟶ Y''} (ψ : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk h) : data.mapZ (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.mapZ ψ)

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {X'' Y'' : C} {h : X'' ⟶ Y''} (ψ : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk h) {Z : C} (h✝ : (data.factorizationData h).Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (data.mapZ (CategoryTheory.CategoryStruct.comp φ ψ)) h✝ = CategoryTheory.CategoryStruct.comp (data.mapZ φ) (CategoryTheory.CategoryStruct.comp (data.mapZ ψ) h✝)

def CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] : CategoryTheory.Functor (CategoryTheory.Arrow (CategoryTheory.Functor J C)) (CategoryTheory.Functor J C)

Auxiliary definition for FunctorialFactorizationData.functorCategory.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_map_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Functor J C)} (τ : X✝ ⟶ Y✝) (j : J) : ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).map τ).app j = data.mapZ { left := τ.left.app j, right := τ.right.app j, w := ⋯ }

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] (f : CategoryTheory.Arrow (CategoryTheory.Functor J C)) (j : J) : ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).obj j = (data.factorizationData (f.hom.app j)).Z

@[simp]

theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_obj_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] (f : CategoryTheory.Arrow (CategoryTheory.Functor J C)) {X✝ Y✝ : J} (φ : X✝ ⟶ Y✝) : ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).map φ = data.mapZ { left := f.left.map φ, right := f.right.map φ, w := ⋯ }

def CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] : (W₁.functorCategory J).FunctorialFactorizationData (W₂.functorCategory J)

A functorial factorization in the category C extends to the functor category J ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

class CategoryTheory.MorphismProperty.HasFunctorialFactorization {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) : Prop

The functorial factorization axiom for two classes of morphisms W₁ and W₂ in a category C. It asserts that any morphism can be factored in a functorial manner as a morphism in W₁ followed by a morphism in W₂.

• nonempty_functorialFactorizationData : Nonempty (W₁.FunctorialFactorizationData W₂)

noncomputable def CategoryTheory.MorphismProperty.functorialFactorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFunctorialFactorization W₂] : W₁.FunctorialFactorizationData W₂

A chosen term in FunctorialFactorizationData W₁ W₂ when the functorial factorization axiom HasFunctorialFactorization W₁ W₂ holds.

Equations

• W₁.functorialFactorizationData W₂ = ⋯.some

instance CategoryTheory.MorphismProperty.instHasFactorizationOfHasFunctorialFactorization {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFunctorialFactorization W₂] : W₁.HasFactorization W₂

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.instHasFunctorialFactorizationFunctorFunctorCategory {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFunctorialFactorization W₂] (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] : (W₁.functorCategory J).HasFunctorialFactorization (W₂.functorCategory J)

Equations

• ⋯ = ⋯