English
The tensor distribution map assigns to a pair of bilinear forms B1,B2 a bilinear form on tensor products, in A-scalar linear fashion, respecting the algebraic structures involved.
Русский
Тензорное распределение отображает пару билинейных форм B1,B2 в билинейную форму на тензорных произведениях, сохраняя структуру и совместимость с алгеброй.
LaTeX
$$$tensorDistrib\\: BilinMap A M_1 N_1 \\otimes [R] BilinMap R M_2 N_2 \\to BilinMap A (M_1 \\otimes_R M_2) (N_1 \\otimes_R N_2)$$$
Lean4
/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products.
Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra
over the ring in which the right bilinear form is valued. -/
def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) :=
(AlgebraTensorModule.rid R A A).congrRight₂.toLinearMap ∘ₗ (BilinMap.tensorDistrib R A)
