# Factoring through subobjects #

The predicate h : P.Factors f, for P : Subobject Y and f : X ⟶ Y asserts the existence of some P.factorThru f : X ⟶ (P : C) making the obvious diagram commute.

def CategoryTheory.MonoOver.Factors {C : Type u₁} [] {X : C} {Y : C} (P : ) (f : X Y) :

When f : X ⟶ Y and P : MonoOver Y, P.Factors f expresses that there exists a factorisation of f through P. Given h : P.Factors f, you can recover the morphism as P.factorThru f h.

Equations
• P.Factors f = ∃ (g : X P.obj.left), = f
Instances For
theorem CategoryTheory.MonoOver.factors_congr {C : Type u₁} [] {X : C} {f : } {g : } {Y : C} (h : Y X) (e : f g) :
f.Factors h g.Factors h
def CategoryTheory.MonoOver.factorThru {C : Type u₁} [] {X : C} {Y : C} (P : ) (f : X Y) (h : P.Factors f) :
X P.obj.left

P.factorThru f h provides a factorisation of f : X ⟶ Y through some P : MonoOver Y, given the evidence h : P.Factors f that such a factorisation exists.

Equations
• P.factorThru f h =
Instances For
def CategoryTheory.Subobject.Factors {C : Type u₁} [] {X : C} {Y : C} (P : ) (f : X Y) :

When f : X ⟶ Y and P : Subobject Y, P.Factors f expresses that there exists a factorisation of f through P. Given h : P.Factors f, you can recover the morphism as P.factorThru f h.

Equations
Instances For
@[simp]
theorem CategoryTheory.Subobject.mk_factors_iff {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : Y X) (g : Z X) :
.Factors g .Factors g
theorem CategoryTheory.Subobject.mk_factors_self {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
.Factors f
theorem CategoryTheory.Subobject.factors_iff {C : Type u₁} [] {X : C} {Y : C} (P : ) (f : X Y) :
P.Factors f (CategoryTheory.Subobject.representative.obj P).Factors f
theorem CategoryTheory.Subobject.factors_self {C : Type u₁} [] {X : C} (P : ) :
P.Factors P.arrow
theorem CategoryTheory.Subobject.factors_comp_arrow {C : Type u₁} [] {X : C} {Y : C} {P : } (f : X CategoryTheory.Subobject.underlying.obj P) :
P.Factors ()
theorem CategoryTheory.Subobject.factors_of_factors_right {C : Type u₁} [] {X : C} {Y : C} {Z : C} {P : } (f : X Y) {g : Y Z} (h : P.Factors g) :
P.Factors
theorem CategoryTheory.Subobject.factors_zero {C : Type u₁} [] {X : C} {Y : C} {P : } :
P.Factors 0
theorem CategoryTheory.Subobject.factors_of_le {C : Type u₁} [] {Y : C} {Z : C} {P : } {Q : } (f : Z Y) (h : P Q) :
P.Factors fQ.Factors f
def CategoryTheory.Subobject.factorThru {C : Type u₁} [] {X : C} {Y : C} (P : ) (f : X Y) (h : P.Factors f) :
X CategoryTheory.Subobject.underlying.obj P

P.factorThru f h provides a factorisation of f : X ⟶ Y through some P : Subobject Y, given the evidence h : P.Factors f that such a factorisation exists.

Equations
• P.factorThru f h =
Instances For
@[simp]
theorem CategoryTheory.Subobject.factorThru_arrow_assoc {C : Type u₁} [] {X : C} {Y : C} (P : ) (f : X Y) (h : P.Factors f) {Z : C} (h : Y Z) :
CategoryTheory.CategoryStruct.comp (P.factorThru f h✝) () =
@[simp]
theorem CategoryTheory.Subobject.factorThru_arrow {C : Type u₁} [] {X : C} {Y : C} (P : ) (f : X Y) (h : P.Factors f) :
CategoryTheory.CategoryStruct.comp (P.factorThru f h) P.arrow = f
@[simp]
theorem CategoryTheory.Subobject.factorThru_self {C : Type u₁} [] {X : C} (P : ) (h : P.Factors P.arrow) :
P.factorThru P.arrow h = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj P)
@[simp]
theorem CategoryTheory.Subobject.factorThru_mk_self {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
.factorThru f =
@[simp]
theorem CategoryTheory.Subobject.factorThru_comp_arrow {C : Type u₁} [] {X : C} {Y : C} {P : } (f : X CategoryTheory.Subobject.underlying.obj P) (h : P.Factors ()) :
P.factorThru () h = f
@[simp]
theorem CategoryTheory.Subobject.factorThru_eq_zero {C : Type u₁} [] {X : C} {Y : C} {P : } {f : X Y} {h : P.Factors f} :
P.factorThru f h = 0 f = 0
theorem CategoryTheory.Subobject.factorThru_right {C : Type u₁} [] {X : C} {Y : C} {Z : C} {P : } (f : X Y) (g : Y Z) (h : P.Factors g) :
CategoryTheory.CategoryStruct.comp f (P.factorThru g h) = P.factorThru
@[simp]
theorem CategoryTheory.Subobject.factorThru_zero {C : Type u₁} [] {X : C} {Y : C} {P : } (h : P.Factors 0) :
P.factorThru 0 h = 0
theorem CategoryTheory.Subobject.factorThru_ofLE {C : Type u₁} [] {Y : C} {Z : C} {P : } {Q : } {f : Z Y} (h : P Q) (w : P.Factors f) :
Q.factorThru f = CategoryTheory.CategoryStruct.comp (P.factorThru f w) (P.ofLE Q h)
theorem CategoryTheory.Subobject.factors_add {C : Type u₁} [] {X : C} {Y : C} {P : } (f : X Y) (g : X Y) (wf : P.Factors f) (wg : P.Factors g) :
P.Factors (f + g)
theorem CategoryTheory.Subobject.factorThru_add {C : Type u₁} [] {X : C} {Y : C} {P : } (f : X Y) (g : X Y) (w : P.Factors (f + g)) (wf : P.Factors f) (wg : P.Factors g) :
P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg
theorem CategoryTheory.Subobject.factors_left_of_factors_add {C : Type u₁} [] {X : C} {Y : C} {P : } (f : X Y) (g : X Y) (w : P.Factors (f + g)) (wg : P.Factors g) :
P.Factors f
@[simp]
theorem CategoryTheory.Subobject.factorThru_add_sub_factorThru_right {C : Type u₁} [] {X : C} {Y : C} {P : } (f : X Y) (g : X Y) (w : P.Factors (f + g)) (wg : P.Factors g) :
P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f
theorem CategoryTheory.Subobject.factors_right_of_factors_add {C : Type u₁} [] {X : C} {Y : C} {P : } (f : X Y) (g : X Y) (w : P.Factors (f + g)) (wf : P.Factors f) :
P.Factors g
@[simp]
theorem CategoryTheory.Subobject.factorThru_add_sub_factorThru_left {C : Type u₁} [] {X : C} {Y : C} {P : } (f : X Y) (g : X Y) (w : P.Factors (f + g)) (wf : P.Factors f) :
P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g