toLocalizedQuotient' — Mathlib

English

The localized version of a submodule M′, i.e., M'.toLocalizedQuotient, carries a localized module structure with respect to p and f.

Русский

Локализованная версия подмодуля M′, то есть M'.toLocalizedQuotient, обладает структурой локализованного модуля относительно p и f.

LaTeX

$$$M'.\mathrm{toLocalizedQuotient}(p,f)$ is a localized_module w.r.t. p and f$$

Lean4

/-- The localization map of a quotient module. -/
def toLocalizedQuotient' : M ⧸ M' →ₗ[R] N ⧸ M'.localized' S p f :=
  Submodule.mapQ M' ((M'.localized' S p f).restrictScalars R) f (fun x hx ↦ ⟨x, hx, 1, by simp⟩)

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