Being projective is a local property

Main results

• LinearMap.split_surjective_of_localization_maximal If N is finitely presented, then f : M →ₗ[R] N being split injective can be checked on stalks (of maximal ideals).
• Module.projective_of_localization_maximal If M is finitely presented, then M being projective can be checked on stalks (of maximal ideals).

TODO

• Show that being projective is Zariski-local (very hard)

theorem Module.projective_of_isLocalizedModule {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {Rₛ : Type u_1} {Mₛ : Type u_2} [AddCommGroup Mₛ] [Module R Mₛ] [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S : Submonoid R) (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ] [IsLocalizedModule S f] [Module.Projective R M] : Module.Projective Rₛ Mₛ

theorem LinearMap.split_surjective_of_localization_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) [Module.FinitePresentation R N] (H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ (g : LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I] LocalizedModule I.primeCompl M), (LocalizedModule.map I.primeCompl) f ∘ₗ g = LinearMap.id) : ∃ (g : N →ₗ[R] M), f ∘ₗ g = LinearMap.id

theorem Module.projective_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (H : ∀ (I : Ideal R) (x : I.IsMaximal), Module.Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)) [Module.FinitePresentation R M] : Module.Projective R M

theorem Module.projective_of_localization_maximal' {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_1) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (H : ∀ (I : Ideal R) (x : I.IsMaximal), Module.Projective (Rₚ I) (Mₚ I)) [Module.FinitePresentation R M] : Module.Projective R M

A variant of Module.projective_of_localization_maximal that accepts IsLocalizedModule.