Theorems · Definition · category theory

CategoryTheory.MonoOver.Factors

{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → CategoryTheory.MonoOver Y → (X ⟶ Y) → Prop

When f : X ⟶ Y and P : MonoOver Y, P.Factors f expresses that there exists a factorisation of f through P. Given h : P.Factors f, you can recover the morphism as P.factorThru f h.

Defined in

Mathlib.CategoryTheory.Subobject.FactorThru

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category