English
The bilinear map sending a ∈ A and b ∈ B to the class ⟦a ⊗ b⟧ in (coinvariantsTensor k G).obj A).obj B defines a linear map from A × B to the coinvariants tensor object.
Русский
Билинейное отображение, отправляющее a ∈ A и b ∈ B в класс ⟦a ⊗ b⟧ в (coinvariantsTensor k G).obj A) .obj B, задаёт линейное отображение.
LaTeX
$$$\\text{coinvariantsTensorMk}: A \\to L[k] B \\to L[k] ((\\text{coinvariantsTensor } k G).obj A).obj B$$$
Lean4
/-- The functor sending `A, B` to `(A ⊗[k] B)_G`. This is naturally isomorphic to the functor
sending `A, B` to `A ⊗[k[G]] B`, where we give `A` the `k[G]ᵐᵒᵖ`-module structure defined by
`g • a := A.ρ g⁻¹ a`. -/
noncomputable abbrev coinvariantsTensor : Rep k G ⥤ Rep k G ⥤ ModuleCat k :=
(Functor.postcompose₂.obj (coinvariantsFunctor k G)).obj (MonoidalCategory.curriedTensor _)
