bijective_of_isLocalized_maximal — Mathlib

English

If for every maximal P the localized sequence is exact, then the global sequence is exact.

Русский

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

LaTeX

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

Lean4

theorem bijective_of_isLocalized_maximal
    (H : ∀ (P : Ideal R) [P.IsMaximal], Function.Bijective (map P.primeCompl (f P) (g P) F)) : Function.Bijective F :=
  ⟨injective_of_isLocalized_maximal Mₚ f Nₚ g F fun J _ ↦ (H J).1,
    surjective_of_isLocalized_maximal Mₚ f Nₚ g F fun J _ ↦ (H J).2⟩

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