Commit 2021-03-04 07:49 f4db322fView on Github →
feat(category_theory/subobject): factoring morphisms through subobjects (#6302)
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.