finsuppLeft — Mathlib

English

There is a natural linear equivalence between (ι →₀ M) ⊗ N and ι →₀ (M ⊗ N).

Русский

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

LaTeX

$$$(\\iota \\mapsto M)\\!\\_⊗ R 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 finsuppLeft : (ι →₀ M) ⊗[R] N ≃ₗ[R] ι →₀ M ⊗[R] N :=
  congr (finsuppLEquivDirectSum R M ι) (.refl R N) ≪≫ₗ directSumLeft R (fun _ ↦ M) N ≪≫ₗ
    (finsuppLEquivDirectSum R _ ι).symm

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