Being injective is a local property #
Main Results #
Module.injective_of_isLocalizedModule: For moduleMover Noetherian ringR, being injective is preserved under localization.Module.injective_of_localization_maximal: For moduleMover Noetherian ringR, being injective can be checked at localization at maximal ideals.
theorem
Module.injective_of_isLocalizedModule
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
(S : Submonoid R)
[Small.{v, u} R]
[IsNoetherianRing R]
{Rₛ : Type u'}
[Small.{v', u'} Rₛ]
[CommRing Rₛ]
[Algebra R Rₛ]
{Mₛ : Type v'}
[AddCommGroup Mₛ]
[Module R Mₛ]
[Module Rₛ Mₛ]
[IsScalarTower R Rₛ Mₛ]
(f : M →ₗ[R] Mₛ)
[IsLocalization S Rₛ]
[IsLocalizedModule S f]
[Injective R M]
:
Injective Rₛ Mₛ
theorem
Module.injective_of_localization_maximal
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
[Small.{v, u} R]
[IsNoetherianRing R]
(H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M))
:
Injective R M
theorem
Module.injective_of_localization_maximal'
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
(Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u')
[(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)]
[∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (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 v')
[(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)]
[Small.{v, u} R]
[IsNoetherianRing R]
(H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Rₚ I) (Mₚ I))
:
Injective R M
A variant of Module.injective_of_localization_maximal that accepts IsLocalizedModule.