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.

Estimated changes