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.free_of_isLocalizedModule {R : Type u_1} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Rₛ : Type u_3} {Mₛ : Type u_4} [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] [Free R M] : Free Rₛ Mₛ

theorem Module.lift_rank_of_isLocalizedModule_of_free {R : Type u_1} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Rₛ : Type uR') {Mₛ : Type uM'} [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] [Free R M] [Nontrivial Rₛ] : Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM', uM} (Module.rank R M)

Also see IsLocalizedModule.lift_rank_eq for a version for non-free modules, but requires S to not contain any zero-divisors.

theorem Module.finrank_of_isLocalizedModule_of_free {R : Type u_1} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Rₛ : Type u_3) {Mₛ : Type u_4} [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] [Free R M] [Nontrivial Rₛ] : finrank Rₛ Mₛ = finrank R M

theorem Module.projective_of_isLocalizedModule {R : Type u_1} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Rₛ : Type u_3} {Mₛ : Type u_4} [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] [Projective R M] : Projective Rₛ Mₛ

instance instProjectiveLocalizationLocalizedModule {R : Type u_1} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (S : Submonoid R) [Module.Projective R M] : Module.Projective (Localization S) (LocalizedModule S M)

instance instProjectiveLocalizationAlgebraMapSubmonoid {R : Type u_1} [CommRing R] (S : Submonoid R) {A : Type u_3} [CommRing A] [Algebra R A] [Module.Projective R A] : Module.Projective (Localization S) (Localization (Algebra.algebraMapSubmonoid A S))

theorem LinearMap.split_surjective_of_localization_maximal {R : Type u_1} {N : Type u_2} {M : Type uM} [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 = id) : ∃ (g : N →ₗ[R] M), f ∘ₗ g = id

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

theorem Module.projective_of_localization_maximal' {R : Type u_1} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3) [(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) → [P.IsMaximal] → Type u_4) [(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), Projective (Rₚ I) (Mₚ I)) [FinitePresentation R M] : Projective R M

A variant of Module.projective_of_localization_maximal that accepts IsLocalizedModule.