# mathlibdocumentation

category_theory.subobject.factor_thru

# Factoring through subobjects #

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.

def category_theory.mono_over.factors {C : Type u₁} {X Y : C} (f : X Y) :
Prop

When f : X ⟶ Y and P : mono_over 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.factor_thru f h.

Equations
theorem category_theory.mono_over.factors_congr {C : Type u₁} {X : C} {f g : category_theory.mono_over X} {Y : C} (h : Y X) (e : f g) :
def category_theory.mono_over.factor_thru {C : Type u₁} {X Y : C} (f : X Y) (h : P.factors f) :
X P

P.factor_thru f h provides a factorisation of f : X ⟶ Y through some P : mono_over Y, given the evidence h : P.factors f that such a factorisation exists.

Equations
def category_theory.subobject.factors {C : Type u₁} {X Y : C} (f : X Y) :
Prop

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.factor_thru f h.

Equations
@[simp]
theorem category_theory.subobject.mk_factors_iff {C : Type u₁} {X Y Z : C} (f : Y X) (g : Z X) :
theorem category_theory.subobject.factors_iff {C : Type u₁} {X Y : C} (f : X Y) :
theorem category_theory.subobject.factors_self {C : Type u₁} {X : C}  :
theorem category_theory.subobject.factors_comp_arrow {C : Type u₁} {X Y : C} (f : X P) :
P.factors (f P.arrow)
theorem category_theory.subobject.factors_of_factors_right {C : Type u₁} {X Y Z : C} (f : X Y) {g : Y Z} (h : P.factors g) :
P.factors (f g)
theorem category_theory.subobject.factors_zero {C : Type u₁} {X Y : C}  :
theorem category_theory.subobject.factors_of_le {C : Type u₁} {Y Z : C} {P Q : category_theory.subobject Y} (f : Z Y) (h : P Q) :
P.factors fQ.factors f
def category_theory.subobject.factor_thru {C : Type u₁} {X Y : C} (f : X Y) (h : P.factors f) :
X P

P.factor_thru 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
@[simp]
theorem category_theory.subobject.factor_thru_arrow {C : Type u₁} {X Y : C} (f : X Y) (h : P.factors f) :
@[simp]
theorem category_theory.subobject.factor_thru_arrow_assoc {C : Type u₁} {X Y : C} (f : X Y) (h : P.factors f) {X' : C} (f' : Y X') :
P.factor_thru f h P.arrow f' = f f'
@[simp]
theorem category_theory.subobject.factor_thru_self {C : Type u₁} {X : C} (h : P.factors P.arrow) :
@[simp]
theorem category_theory.subobject.factor_thru_comp_arrow {C : Type u₁} {X Y : C} (f : X P) (h : P.factors (f P.arrow)) :
P.factor_thru (f P.arrow) h = f
@[simp]
theorem category_theory.subobject.factor_thru_eq_zero {C : Type u₁} {X Y : C} {f : X Y} {h : P.factors f} :
P.factor_thru f h = 0 f = 0
theorem category_theory.subobject.factor_thru_right {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : P.factors g) :
f P.factor_thru g h = P.factor_thru (f g) _
@[simp]
theorem category_theory.subobject.factor_thru_zero {C : Type u₁} {X Y : C} (h : P.factors 0) :
P.factor_thru 0 h = 0
theorem category_theory.subobject.factor_thru_of_le {C : Type u₁} {Y Z : C} {P Q : category_theory.subobject Y} {f : Z Y} (h : P Q) (w : P.factors f) :
Q.factor_thru f _ = P.factor_thru f w P.of_le Q h
theorem category_theory.subobject.factors_add {C : Type u₁} {X Y : C} (f g : X Y) (wf : P.factors f) (wg : P.factors g) :
P.factors (f + g)
theorem category_theory.subobject.factor_thru_add {C : Type u₁} {X Y : C} (f g : X Y) (w : P.factors (f + g)) (wf : P.factors f) (wg : P.factors g) :
P.factor_thru (f + g) w = P.factor_thru f wf + P.factor_thru g wg
theorem category_theory.subobject.factors_left_of_factors_add {C : Type u₁} {X Y : C} (f g : X Y) (w : P.factors (f + g)) (wg : P.factors g) :
@[simp]
theorem category_theory.subobject.factor_thru_add_sub_factor_thru_right {C : Type u₁} {X Y : C} (f g : X Y) (w : P.factors (f + g)) (wg : P.factors g) :
P.factor_thru (f + g) w - P.factor_thru g wg = P.factor_thru f _
theorem category_theory.subobject.factors_right_of_factors_add {C : Type u₁} {X Y : C} (f g : X Y) (w : P.factors (f + g)) (wf : P.factors f) :
@[simp]
theorem category_theory.subobject.factor_thru_add_sub_factor_thru_left {C : Type u₁} {X Y : C} (f g : X Y) (w : P.factors (f + g)) (wf : P.factors f) :
P.factor_thru (f + g) w - P.factor_thru f wf = P.factor_thru g _