eq_of_localization_maximal — Mathlib

English

Let g, g' be M → M1 linear maps. If for every maximal P the localized maps are equal, then g = g'.

Русский

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

LaTeX

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

Lean4

theorem eq_of_localization_maximal (m m' : M) (h : ∀ (P : Ideal R) [P.IsMaximal], f P m = f P m') : m = m' :=
  by
  rw [← one_smul R m, ← one_smul R m']
  by_contra ne
  have ⟨P, mP, le⟩ := (eqIdeal R m m').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
  have ⟨s, hs⟩ := (IsLocalizedModule.eq_iff_exists P.primeCompl _).mp (h P)
  exact s.2 (le hs)

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