English
Evaluating tensorDistribEquiv on a simple tensor B1 ⊗ B2 and simple tensors m1 ⊗ m2, m1' ⊗ m2' yields B1 m1 m1' · B2 m2 m2'.
Русский
При применении tensorDistribEquiv к простому тензору B1 ⊗ B2 и простым тензорам m1 ⊗ m2, m1' ⊗ m2' получается B1 m1 m1' · B2 m2 m2'.
LaTeX
$$$$ tensorDistribEquiv\; R\; (M_1 := M_1)\ (M_2 := M_2)\ (B_1 \otimes_\text{tmul} B_2)\ (m_1 \otimes m_2) (m_1' \otimes m_2') = B_1(m_1,m_1') \cdot B_2(m_2,m_2'). $$$$
Lean4
/-- `tensorDistrib` as an equivalence. -/
noncomputable def tensorDistribEquiv : BilinForm R M₁ ⊗[R] BilinForm R M₂ ≃ₗ[R] BilinForm R (M₁ ⊗[R] M₂) :=
-- the same `LinearEquiv`s as from `tensorDistrib`,
-- but with the inner linear map also as an equiv
TensorProduct.congr (TensorProduct.lift.equiv R _ _ _) (TensorProduct.lift.equiv R _ _ _) ≪≫ₗ
TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ
(TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ
(TensorProduct.lift.equiv R _ _ _).symm
