Theorems · Inductive type · category theory

CategoryTheory.MorphismProperty.MapFactorizationData

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → {X Y : C} → (X ⟶ Y) → Type (max u_1 v_1)

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.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Factorization

Cited by

63 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category