English
Let A and B be G-representations over k. The canonical coinvariants-tensor construction sends a ∈ A and b ∈ B to the coinvariant class of a ⊗ b in the tensor representation; i.e., the element coinvariantsMk A B a b equals the coinvariant class of a ⊗ b.
Русский
Пусть A и B — представления G над кольцом k. Каноническое отображение коинвариантов тензора отправляет элементы a ∈ A и b ∈ B в класс коинвариантов тензора a ⊗ b; то есть coinvariantsMk A B a b является классом a ⊗ b в коинвариантах.
LaTeX
$$$coinvariantsTensorMk\\;A\\;B\\;a\\;b = \\operatorname{Coinvariants.mk}\\_\\; (a \\otimes_k b)$$$
Lean4
theorem coinvariantsTensorMk_apply (a : A) (b : B) : coinvariantsTensorMk A B a b = Coinvariants.mk _ (a ⊗ₜ[k] b) :=
rfl