uliftFunctor_additive — Mathlib

English

The universe-lift for commutative additive groups is additive: it preserves addition on Hom-sets, i.e., Ulift(f+g) = Ulift(f) + Ulift(g).

Русский

Функтор подъёма вселенной для коммутативных аддитивных групп является аддитивным: он сохраняет сложение на множестве гомоморфизмов, т.е. Ulift(f+g) = Ulift(f) + Ulift(g).

LaTeX

$$$\forall A,B : \mathrm{AddCommGrpCat},\; \forall f,g : \mathrm{Hom}(A,B),\; \mathrm{Ulift}(f+g) = \mathrm{Ulift}(f) + \mathrm{Ulift}(g)$$$

Lean4

/-- The universe lift for commutative additive groups is additive.
-/
instance uliftFunctor_additive : AddCommGrpCat.uliftFunctor.{u, v}.Additive where

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