finsuppTensorFinsupp — Mathlib

English

For m ∈ M, p ∈ ι →₀ R, and i ∈ ι, the i-th coordinate of finsuppScalarRight(m ⊗ p) is p(i) · m.

Русский

Для m ∈ M, p ∈ ι →₀ R и i ∈ ι, i-я координата finsuppScalarRight(m ⊗ p) равна p(i) · m.

LaTeX

$$$ finsuppScalarRight R M ι (m \\otimes p) i = p(i) \\cdot m $$$

Lean4

/-- The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`. -/
def finsuppTensorFinsupp : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N :=
  TensorProduct.AlgebraTensorModule.congr (finsuppLEquivDirectSum S M ι) (finsuppLEquivDirectSum R N κ) ≪≫ₗ
    ((TensorProduct.directSum R S (fun _ : ι => M) fun _ : κ => N) ≪≫ₗ
      (finsuppLEquivDirectSum S (M ⊗[R] N) (ι × κ)).symm)

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