English
If for all maximal ideals the localized module is projective, then the original module is projective.
Русский
Если для всех максимальных идеалов локализованный модуль проективен, то исходный модуль проективен.
LaTeX
$$$\\forall p \\text{ maximal}, \\; (M_p) \\text{ projective} \\Rightarrow M \\text{ projective}$$$
Lean4
theorem projective_of_localization_maximal
(H : ∀ (I : Ideal R) (_ : I.IsMaximal), Module.Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M))
[Module.FinitePresentation R M] : Module.Projective R M :=
by
have : Module.Finite R M := by infer_instance
have : (⊤ : Submodule R M).FG := this.fg_top
have : ∃ (s : Finset M), _ := this
obtain ⟨s, hs⟩ := this
let N := s →₀ R
let f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val : s → M)
have hf : Function.Surjective f :=
by
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, Subtype.range_val]
convert hs
have (I : Ideal R) (hI : I.IsMaximal) :=
letI := H I hI
Module.projective_lifting_property (LocalizedModule.map I.primeCompl f) LinearMap.id
(LocalizedModule.map_surjective _ _ hf)
obtain ⟨g, hg⟩ := LinearMap.split_surjective_of_localization_maximal _ this
exact Module.Projective.of_split _ _ hg
