toLocalizedQuotient — Mathlib

English

The localization map of a quotient module is a linear map from M/M′ to the localized quotient of the target, i.e., toLocalizedQuotient': M ⧸ M′ →_R LocalizedModule p M ⧸ M'.localized p.

Русский

Локализационная карта по отношению к частичному модулю представляет собой линейное отображение M/M′ в локализованную часть модуля: toLocalizedQuotient': M ⧸ M′ →_R LocalizedModule p M ⧸ M'.localized p.

LaTeX

$$$\mathrm{toLocalizedQuotient}': M / M' \to_R \mathrm{LocalizedModule}_p M / M'.localized(p)$$$

Lean4

/-- The localization map of a quotient module. -/
noncomputable abbrev toLocalizedQuotient : M ⧸ M' →ₗ[R] LocalizedModule p M ⧸ M'.localized p :=
  M'.toLocalizedQuotient' (Localization p) p (LocalizedModule.mkLinearMap p M)

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