mathlib3 documentation

category_theory.subobject.factor_thru

Factoring through subobjects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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₁} [category_theory.category C] {X Y : C} (P : category_theory.mono_over Y) (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₁} [category_theory.category C] {X : C} {f g : category_theory.mono_over X} {Y : C} (h : Y X) (e : f g) :
noncomputable def category_theory.mono_over.factor_thru {C : Type u₁} [category_theory.category C] {X Y : C} (P : category_theory.mono_over Y) (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₁} [category_theory.category C] {X Y : C} (P : category_theory.subobject Y) (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
theorem category_theory.subobject.factors_of_factors_right {C : Type u₁} [category_theory.category C] {X Y Z : C} {P : category_theory.subobject Z} (f : X Y) {g : Y Z} (h : P.factors g) :
P.factors (f g)
theorem category_theory.subobject.factors_of_le {C : Type u₁} [category_theory.category C] {Y Z : C} {P Q : category_theory.subobject Y} (f : Z Y) (h : P Q) :
noncomputable def category_theory.subobject.factor_thru {C : Type u₁} [category_theory.category C] {X Y : C} (P : category_theory.subobject Y) (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₁} [category_theory.category C] {X Y : C} (P : category_theory.subobject Y) (f : X Y) (h : P.factors f) :
@[simp]
theorem category_theory.subobject.factor_thru_arrow_assoc {C : Type u₁} [category_theory.category C] {X Y : C} (P : category_theory.subobject Y) (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_right {C : Type u₁} [category_theory.category C] {X Y Z : C} {P : category_theory.subobject Z} (f : X Y) (g : Y Z) (h : P.factors g) :
f P.factor_thru g h = P.factor_thru (f g) _
theorem category_theory.subobject.factor_thru_of_le {C : Type u₁} [category_theory.category C] {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₁} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {P : category_theory.subobject Y} (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₁} [category_theory.category C] [category_theory.preadditive C] {X Y : C} {P : category_theory.subobject Y} (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