factorThru_add — Mathlib

English

In a preadditive category, for f,g: X → Y with w factoring f+g through P, wf through f, wg through g, the factorThrough of the sum equals the sum of the factorThroughs.

Русский

В предадитивной категории факторизация через сумму равна сумме факторизаций: P.factorThru (f+g) w = P.factorThru f wf + P.factorThru g wg.

LaTeX

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

Lean4

theorem factorThru_add {X Y : C} {P : Subobject Y} (f 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 :=
  by
  ext
  simp

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