Theorems · Definition · category theory

CategoryTheory.MorphismProperty.FunctorialFactorizationData.ofLE

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      W₁.FunctorialFactorizationData W₂ →
        {W₁' W₂' : CategoryTheory.MorphismProperty C} → W₁ ≤ W₁' → 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₂'.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Factorization

Cited by

0 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category