eq_zero_of_localization_maximal — Mathlib

English

Let g be a linear map from M to M1. If after localization at every maximal ideal P the localized map is equal to a reference, then g is determined by these localizations (equality of localizations forces equality of maps).

Русский

Пусть g — линейное отображение M в M1. Если локализованные отображения по всем максимальным идеалам определяют g однозначно, значит g равен своей локализации во всех местах.

LaTeX

$$$$\forall P\,[P^{{\mathrm{Max}}}],\; IsLocalizedModule.map\bigl(P, g\bigr) = IsLocalizedModule.map\bigl(P, g'\bigr) \Rightarrow g = g'.$$$$

Lean4

theorem eq_zero_of_localization_maximal (m : M) (h : ∀ (P : Ideal R) [P.IsMaximal], f P m = 0) : m = 0 :=
  eq_of_localization_maximal _ f _ _ fun P _ ↦ by rw [h, map_zero]

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