colimit_add_mk_eq — Mathlib

English

The sum of two colimit representatives corresponds to the sum in the target object using the same connecting morphisms.

Русский

Сумма двух представителей колимита соответствует сумме в целевом объекте через те же отображения связей.

LaTeX

$$$$ M.{\\text{mk}} F \\langle k, F.map f x \\rangle + M.{\\text{mk}} F \\langle j, F.map g y \\rangle = M.{\\text{mk}} F \\langle k, F.map f x + F.map g y \\rangle $$$$

Lean4

theorem colimit_add_mk_eq (x y : Σ j, F.obj j) (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k) :
    M.mk _ x + M.mk _ y = M.mk _ ⟨k, F.map f x.2 + F.map g y.2⟩ := by apply AddMonCat.FilteredColimits.colimit_add_mk_eq

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