# Commit 2021-03-04 07:49 f4db322f

View on Github →feat(category_theory/subobject): factoring morphisms through subobjects (#6302)
The predicate `h : P.factors f`

, for `P : subobject Y`

and `f : X ⟶ Y`

asserts the existence of some `P.factor_thru f : X ⟶ (P : C)`

making the obvious diagram commute.
We provide conditions for `P.factors f`

, when `P`

is a kernel/equalizer/image/inf/sup subobject.