Factorizations through subobjects

This file records two elementary forms of the universal property of a subobject. Factoring is unchanged by precomposition with an equality-induced isomorphism, and a factorization through a subobject is unique because its representing arrow is a monomorphism.

Main declarations

• CategoryTheory.Subobject.factors_eqToHom_comp_iff: precomposition by an equality-induced isomorphism does not change whether a morphism factors through a subobject.
• CategoryTheory.Subobject.factors_iff_existsUnique: factoring through a subobject is equivalent to the existence of a unique lift.

theorem CategoryTheory.Subobject.factors_eqToHom_comp_iff {C : Type u} [Category.{v, u} C] {X Y Z : C} (P : Subobject Z) (hXY : X = Y) (f : Y ⟶ Z) : P.Factors (CategoryStruct.comp (eqToHom hXY) f) ↔ P.Factors f

Factoring through a subobject is unchanged after precomposing with the isomorphism induced by an equality of source objects.

theorem CategoryTheory.Subobject.factors_iff_existsUnique {C : Type u} [Category.{v, u} C] {X Y : C} (P : Subobject Y) (f : X ⟶ Y) : P.Factors f ↔ ∃! g : X ⟶ underlying.obj P, CategoryStruct.comp g P.arrow = f

A morphism factors through a subobject exactly when it has a unique lift through the subobject's representing arrow.