map_add — Mathlib

English

Let L be a localization functor from a preadditive category C to a category D with a compatible left calculus of fractions. Then L preserves addition of morphisms: for any f1, f2: X → Y in C, L.map(f1 + f2) = L.map f1 + L.map f2.

Русский

Пусть L — локализационный функтор от прeадитивной категории C в категорию D, совместимый с левым калькулами дробей. Тогда L сохраняет сложение морфизмов: для любых f1, f2: X → Y в C выполняется L.map(f1 + f2) = L.map f1 + L.map f2.

LaTeX

$$$L.map\left(f_1 + f_2\right) = L.map\left(f_1\right) + L.map\left(f_2\right)$$$

Lean4

theorem map_add (f₁ f₂ : X ⟶ Y) :
    letI := addCommGroup L W (L.obj X) (L.obj Y)
    L.map (f₁ + f₂) = L.map f₁ + L.map f₂ :=
  by
  rw [add_eq W (Iso.refl _) (Iso.refl _) (L.map f₁) (L.map f₂)]
  simp [add]

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