piScalarRightHom — Mathlib

English

There is a canonical linear map piRightHom : N ⊗_R (ι → R) →_S (ι → N).

Русский

Существует каноничное линейное отображение piRightHom : N ⊗_R (ι → R) →_S (ι → N).

LaTeX

$$$piRightHom : N \otimes_R (\iota \to R) \to_S (\iota \to N).$$$

Lean4

/-- For any `R`-module `N` and index type `ι`, there is a natural
linear map `N ⊗[R] (ι → R) →ₗ (ι → N)`. This map is an isomorphism if `ι` is finite. -/
def piScalarRightHom : N ⊗[R] (ι → R) →ₗ[S] (ι → N) :=
  AlgebraTensorModule.lift <| piScalarRightHomBil R S N ι

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