coinvariantsTensorMk — Mathlib

English

The linear map coinvariantsTensorMk is a linear map between the corresponding carriers, respecting SMul structure.

Русский

Линейное отображение coinvariantsTensorMk является линейным отображением между соответствующими носителями и сохраняет структуру SMul.

LaTeX

$$$\\text{coinvariantsTensorMk}: A \\to_ℓ[k] B \\to_ℓ[k] ((\\text{coinvariantsTensor } k G).obj A).obj B$$$

Lean4

/-- The bilinear map sending `a : A, b : B` to `⟦a ⊗ₜ b⟧` in `(A ⊗[k] B)_G`. -/
noncomputable abbrev coinvariantsTensorMk : A →ₗ[k] B →ₗ[k] ((coinvariantsTensor k G).obj A).obj B :=
  (TensorProduct.mk k A B).compr₂ (Coinvariants.mk _)

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