coinvariantsTensorMk_apply — Mathlib

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

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