factors_add — Mathlib

English

In a preadditive category, if f,g: X → Y factor through P with wf,wg, then f and g together factor through P for the sum f+g: P.Factors (f+g).

Русский

В прeадитивной категории, если f,g: X → Y факторизуются через P с wf и wg, то через P факторизуется сумма f+g.

LaTeX

$$$P.\!F\actors (f+g)$$$

Lean4

theorem factors_add {X Y : C} {P : Subobject Y} (f g : X ⟶ Y) (wf : P.Factors f) (wg : P.Factors g) :
    P.Factors (f + g) :=
  (factors_iff _ _).mpr
    ⟨P.factorThru f wf + P.factorThru g wg, by simp⟩
      -- This can't be a `simp` lemma as `wf` and `wg` may not exist.
      -- However you can `rw` by it to assert that `f` and `g` factor through `P` separately.

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