Theorems · Definition · category theory

CategoryTheory.Limits.MonoFactorisation.e

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.Limits.MonoFactorisation f) → X ⟶ self.I

A factorisation of a morphism f = e ≫ m, with m monic.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Images

Cited by

39 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.Category