module — Mathlib

English

The localization operation defines a module structure on the localized module over A via an isomorphism to End_R(M').

Русский

Операция локализации задаёт структуру модуля над A на локализованном модуле через изоморфизм к End_R(M').

LaTeX

$$$$ \\text{module }(f) : \\text{LocalizedModule } S f \\to \\text{Module } A (LocalizedModule S M) $$$$

Lean4

/-- If `M'` is the localization of `M` at `S` and `A = S⁻¹R`, then
`M' is an `A`-module. -/
@[reducible]
noncomputable def module (f : M →ₗ[R] M') [IsLocalizedModule S f] : Module A M' :=
  (IsLocalizedModule.iso S f).symm.toAddEquiv.module A

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