tensorRight_additive — Mathlib

English

For any object X in C, the functor tensorRight X, i.e., Y ↦ Y ⊗ X, is additive. Equivalently, for morphisms f,g: Q → R, (f+g) ⊗ X = f ⊗ X + g ⊗ X.

Русский

Для любого объекта X в C тензорование справа по X, т.е. F(Y) = Y ⊗ X, аддитивно. Эквивалентно, для морфизмов f,g: Q → R выполняется (f+g) ⊗ X = f ⊗ X + g ⊗ X.

LaTeX

$$$ (f+g) \\otimes X = (f \\otimes X) + (g \\otimes X) $$$

Lean4

instance tensorRight_additive (X : C) : (tensorRight X).Additive where

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