Weak factorization systems

In this file, we introduce the notion of weak factorization system, which is a property of two classes of morphisms W₁ and W₂ in a category C. The type class IsWeakFactorizationSystem W₁ W₂ asserts that W₁ is exactly W₂.llp, W₂ is exactly W₁.rlp, and any morphism in C can be factored a i ≫ p with W₁ i and W₂ p.

References

• https://ncatlab.org/nlab/show/weak+factorization+system

class CategoryTheory.MorphismProperty.IsWeakFactorizationSystem {C : Type u} [Category.{v, u} C] (W₁ W₂ : MorphismProperty C) : Prop

Two classes of morphisms W₁ and W₂ in a category C form a weak factorization system if W₁ is exactly W₂.llp, W₂ is exactly W₁.rlp, and any morphism can be factored a i ≫ p with W₁ i and W₂ p.

• rlp : W₁.rlp = W₂
• llp : W₂.llp = W₁
• hasFactorization : W₁.HasFactorization W₂

theorem CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.mk' {C : Type u} [Category.{v, u} C] (W₁ W₂ : MorphismProperty C) [W₁.HasFactorization W₂] [W₁.IsStableUnderRetracts] [W₂.IsStableUnderRetracts] (h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y), W₁ i → W₂ p → HasLiftingProperty i p) : W₁.IsWeakFactorizationSystem W₂

theorem CategoryTheory.MorphismProperty.rlp_eq_of_wfs {C : Type u} [Category.{v, u} C] (W₁ W₂ : MorphismProperty C) [W₁.IsWeakFactorizationSystem W₂] : W₁.rlp = W₂

theorem CategoryTheory.MorphismProperty.llp_eq_of_wfs {C : Type u} [Category.{v, u} C] (W₁ W₂ : MorphismProperty C) [W₁.IsWeakFactorizationSystem W₂] : W₂.llp = W₁

theorem CategoryTheory.MorphismProperty.hasLiftingProperty_of_wfs {C : Type u} [Category.{v, u} C] {W₁ W₂ : MorphismProperty C} [W₁.IsWeakFactorizationSystem W₂] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) (hi : W₁ i) (hp : W₂ p) : HasLiftingProperty i p