Theorems · Theorem · category theory

CategoryTheory.EffectiveEpiStruct.fac

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : Y ⟶ X}
  (self : CategoryTheory.EffectiveEpiStruct f) {W : C} (e : Y ⟶ W)
  (h :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
  CategoryTheory.CategoryStruct.comp f (self.desc e ⋯) = e

...factorizing e through f...

Defined in

Mathlib.CategoryTheory.EffectiveEpi.Basic

Cited by

1 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.Category