English
If for every maximal P there is an exact localization, then there is a global exact sequence.
Русский
Если для каждого максимального P существует локализованная точность, то существует глобальная точность последовательности.
LaTeX
$$$\\forall J\\subseteq R,[J.IsMaximal],\\;\\text{Exact}(\\mathrm{map}_{J}(f),\\mathrm{map}_{J}(g))\\Rightarrow \\text{Exact}(f,g)$$$
Lean4
theorem exact_of_isLocalized_maximal
(H :
∀ (J : Ideal R) [J.IsMaximal], Function.Exact (map J.primeCompl (f J) (g J) F) (map J.primeCompl (g J) (h J) G)) :
Function.Exact F G := by
simp only [LinearMap.exact_iff] at H ⊢
apply eq_of_localization₀_maximal Nₚ g
intro J hJ
rw [← LinearMap.range_localizedMap_eq_localized₀_range _ (f J) (g J) F, ←
LinearMap.ker_localizedMap_eq_localized₀_ker J.primeCompl (g J) (h J) G]
have := SetLike.ext_iff.mp <| H J
ext x
simp only [mem_range, mem_ker] at this ⊢
exact this x
