injective_of_localized_maximal — Mathlib

English

If all localized maps are isomorphisms, then the global map is an isomorphism.

Русский

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

LaTeX

$$$\\forall J\\;\\text{IsMaximal},\\; \\text{Isomorphism}(\\mathrm{map}_{J}(f)) \\Rightarrow \\text{Isomorphism}(f)$$$

Lean4

theorem injective_of_localized_maximal (h : ∀ (J : Ideal R) [J.IsMaximal], Function.Injective (map J.primeCompl f)) :
    Function.Injective f :=
  injective_of_isLocalized_maximal _ (fun _ _ ↦ mkLinearMap _ _) _ (fun _ _ ↦ mkLinearMap _ _) f h

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