Theorems · Theorem · category theory

CategoryTheory.Preregular.exists_fac

∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Preregular C] {X Y Z : C}
  (f : X ⟶ Y) (g : Z ⟶ Y) [CategoryTheory.EffectiveEpi g],
  ∃ W h,
    ∃ (_ : CategoryTheory.EffectiveEpi h),
      ∃ i, CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.comp h f

For X, Y, Z, f, g like in the diagram, where g is an effective epi, there exists an object W, an effective epi h : W ⟶ X and a morphism i : W ⟶ Z making the diagram commute. `` W --i-→ Z | | h g ↓ ↓ X --f-→ Y ``

Defined in

Mathlib.CategoryTheory.Sites.Coherent.Basic

Cited by

1 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.PreregularCategoryTheory.EffectiveEpi