range_localizedMap_eq_localized₀_range

English

There is a canonical isomorphism between the localized quotient and the quotient in the localized module: localizedQuotientEquiv.

Русский

Существует каноническое изоморфизм между локализованной частной и частной в локализованном модуле: localizedQuotientEquiv.

LaTeX

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

Lean4

theorem range_localizedMap_eq_localized₀_range (g : M →ₗ[R] P) : range (map p f f' g) = (range g).localized₀ p f' := by
  ext; simp [mem_localized₀, mem_range, (mk'_surjective p f).exists]

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