surjective_of_localized_maximal — Mathlib

English

If for every maximal P the localized map is an isomorphism, then the global map is an isomorphism.

Русский

Если для каждого максимального P локализованное отображение изоморфизм, то глобальное тоже изоморфизм.

LaTeX

$$$\\forall P\\,[P.IsMaximal],\\; \\text{Isomorphism}(\\mathrm{map}_{P}(f)) \\Rightarrow \\text{Isomorphism}(f)$$$

Lean4

theorem surjective_of_localized_maximal (h : ∀ (J : Ideal R) [J.IsMaximal], Function.Surjective (map J.primeCompl f)) :
    Function.Surjective f :=
  surjective_of_isLocalized_maximal _ (fun _ _ ↦ mkLinearMap _ _) _ (fun _ _ ↦ mkLinearMap _ _) f h

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