eq_of_localization_maximal — Mathlib

English

Let N1,N2 be submodules of M. If all localizations N1 localized equals N2 localized at every maximal P, then N1 = N2.

Русский

Пусть N1,N2 — подмодули M. Если для каждого максимального идеала P локализации N1 совпадают с локализацией N2, тогда N1 = N2.

LaTeX

$$$$\forall P\,[P^{{\mathrm{Max}}}],\; N1 localized^{P} = N2 localized^{P} \Rightarrow N1 = N2.$$$$

Lean4

theorem eq_of_localization_maximal (g g' : M →ₗ[R] M₁)
    (h :
      ∀ (P : Ideal R) [P.IsMaximal],
        IsLocalizedModule.map P.primeCompl (f P) (f₁ P) g = IsLocalizedModule.map P.primeCompl (f P) (f₁ P) g') :
    g = g' :=
  ext fun x ↦
    Module.eq_of_localization_maximal _ f₁ _ _ fun P _ ↦ by
      simpa only [IsLocalizedModule.map_apply] using DFunLike.congr_fun (h P) (f P x)

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