finsuppRight — Mathlib

English

There is a linear equivalence between M ⊗ (ι →₀ N) and ι →₀ (M ⊗ N); it rearranges the tensor factors indexwise.

Русский

Существует линейное эквивалентное отображение между M ⊗ (ι →₀ N) и ι →₀ (M ⊗ N), приводящее к упорядочиванию тензоров по индексам.

LaTeX

$$$ M \\otimes_R (\\iota \\to_0 N) \\cong_ℓ_R \\iota \\to_0 (M \\otimes_R N) $$$

Lean4

/-- The tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N` -/
noncomputable def finsuppRight : M ⊗[R] (ι →₀ N) ≃ₗ[R] ι →₀ M ⊗[R] N :=
  congr (.refl R M) (finsuppLEquivDirectSum R N ι) ≪≫ₗ directSumRight R M (fun _ : ι ↦ N) ≪≫ₗ
    (finsuppLEquivDirectSum R _ ι).symm

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