factorThru_add_sub_factorThru_right

English

In a preadditive category, for f,g: X→Y with w factoring f+g through P and wf factoring f, the difference P.factorThru (f+g) w − P.factorThru f wf equals P.factorThru g (factors_right_of_factors_add f g w wf).

Русский

Слева через факторизацию через f+g минус факторизация через f равна факторизации через g через соответствующее right-анализ.

LaTeX

$$$P.\text{factorThru} (f+g) w - P.\text{factorThru} f wf = P.\text{factorThru} g (\text{factors_right_of_factors_add } f g w wf)$$$

Lean4

@[simp]
theorem factorThru_add_sub_factorThru_right {X Y : C} {P : Subobject Y} (f g : X ⟶ Y) (w : P.Factors (f + g))
    (wg : P.Factors g) :
    P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f (factors_left_of_factors_add f g w wg) :=
  by
  ext
  simp

Похожие утверждения