mathlib

f4db322f - feat(category_theory/subobject): factoring morphisms through subobjects (#6302)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>