fromLocalizedModule — Mathlib

English

There exists a canonical R-linear map from the localized module to M' whose action is given by fromLocalizedModule'.

Русский

Существует каноническое линейное по R отображение от локализованного модуля к M', чьё действие задаётся через fromLocalizedModule'.

LaTeX

$$$$ \mathrm{fromLocalizedModule}: \mathrm{LocalizedModule}(S,M) \to_R M', \quad \text{toFun} = \mathrm{fromLocalizedModule}'(S,f). $$$$

Lean4

/-- If `(M', f : M ⟶ M')` satisfies universal property of localized module, there is a canonical
map `LocalizedModule S M ⟶ M'`.
-/
noncomputable def fromLocalizedModule : LocalizedModule S M →ₗ[R] M'
    where
  toFun := fromLocalizedModule' S f
  map_add' := fromLocalizedModule'_add S f
  map_smul' r x := by rw [fromLocalizedModule'_smul, RingHom.id_apply]

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