localized'_range_eq_range_localizedMap

English

Localization commutes with quotients and scalar extension; the localizedQuotientEquiv is compatible with the extension to Localization p.

Русский

Локализация совместима с квартификацией и скалярным расширением; локализующая эквивалентность совместима с расширением до Localization p.

LaTeX

$$$\mathrm{localizedQuotientEquiv}: (\mathrm{LocalizedModule}_p M / M'.localized(p)) \cong_{\mathrm{Localization}(p)} \mathrm{LocalizedModule}_p (M / M')$$$

Lean4

/-- Localization commutes with ranges. -/
theorem localized'_range_eq_range_localizedMap (g : M →ₗ[R] P) :
    (range g).localized' S p f' = range ((map p f f' g).extendScalarsOfIsLocalization p S) :=
  SetLike.ext (by apply SetLike.ext_iff.mp (f.range_localizedMap_eq_localized₀_range p f' g).symm)

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