Being projective is a local property #
Main results #
LinearMap.split_surjective_of_localization_maximalIfNis finitely presented, thenf : M →ₗ[R] Nbeing split injective can be checked on stalks (of maximal ideals).Module.projective_of_localization_maximalIfMis finitely presented, thenMbeing 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_4}
{Mₛ : Type u_5}
[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.Free R M]
:
Module.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]
[Module.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_4)
{Mₛ : Type u_5}
[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.Free R M]
[Nontrivial Rₛ]
:
Module.finrank Rₛ Mₛ = Module.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_4}
{Mₛ : Type u_5}
[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}
{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 = LinearMap.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), Module.Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M))
[Module.FinitePresentation 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) → [inst : P.IsMaximal] → Type u_4)
[(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_5)
[(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]
:
A variant of Module.projective_of_localization_maximal that accepts IsLocalizedModule.