surjective_of_isLocalized_maximal

English

If each localized map is surjective, then the global map is surjective.

Русский

Если каждое локализованное отображение сюръективно, тогда глобальное отображение сюръективно.

LaTeX

$$$\\forall P\\,[P.IsMaximal],\\; \\mathrm{map}(P.primeCompl)(f_P)\\text{ surjective} \\Rightarrow f\\text{ surjective}$$$

Lean4

theorem surjective_of_isLocalized_maximal
    (H : ∀ (P : Ideal R) [P.IsMaximal], Function.Surjective (map P.primeCompl (f P) (g P) F)) : Function.Surjective F :=
  range_eq_top.mp <|
    eq_top_of_localization₀_maximal Nₚ g _ <| fun P _ ↦
      (range_localizedMap_eq_localized₀_range _ (f P) (g P) F).symm.trans <| range_eq_top.mpr <| H P

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