piScalarRight — Mathlib

English

There is a canonical linear isomorphism piScalarRight : N ⊗_R (ι → R) ≃_S (ι → N).

Русский

Существует канонический линейный изоморфизм piScalarRight : N ⊗_R (ι → R) ≃_S (ι → N).

LaTeX

$$$piScalarRight : N \otimes_R (\iota \to R) \cong_S (\iota \to N).$$$

Lean4

/-- For any `R`-module `N` and finite index type `ι`, `N ⊗[R] (ι → R)` is canonically
isomorphic to `ι → N`. -/
def piScalarRight : N ⊗[R] (ι → R) ≃ₗ[S] (ι → N) :=
  LinearEquiv.ofLinear (piScalarRightHom R S N ι) (piScalarRightInv R S N ι) (by ext i x j; simp [Pi.single_apply])
    (by ext x i; simp [Pi.single_apply_smul])

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