Injective modules over a Noetherian ring

Let R be a Noetherian commutative ring and I an injective R-module. This file proves the algebraic facts about I on which the flasqueness of the associated quasi-coherent sheaf I^~ on Spec R rests.

• For every ideal 𝔞, the 𝔞-primary component Γ_𝔞(I) = {x ∈ I | 𝔞ⁿ x = 0 for some n} (Mathlib's Ideal.primaryComponent) is again an injective module. The proof is Baer's criterion: a map from an ideal 𝔟 to Γ_𝔞(I) is killed by a power 𝔞ⁿ, because 𝔟 is finitely generated, and by the Artin–Rees lemma it therefore vanishes on 𝔞ᵐ ∩ 𝔟 for m large. It extends by zero to 𝔟 + 𝔞ᵐ, hence to R, and the extension takes values in Γ_𝔞(I).
• For every multiplicative subset S, the localization map I → S⁻¹I is surjective. If ann(t) is maximal among the annihilators of elements of S, then ann(ts) = ann(t) for all s ∈ S, so the map (ts) → I, tsr ↦ trx, is well defined; extending it to R produces a preimage of x / s.
• Combining the two, the localization map I → S⁻¹I is also surjective on 𝔞-primary components: an element of S⁻¹I killed by a power of 𝔞 comes from an element of I killed by a power of 𝔞. On Spec R this says that a section of I^~ over D(f) supported on V(𝔞) extends to a global section supported on V(𝔞).

Main declarations

• Ideal.injective_primaryComponent: Γ_𝔞(I) is an injective module;
• Submonoid.surjective_of_isLocalizedModule: every localization map out of I is surjective;
• Ideal.primaryComponent_map_surjective: every localization map out of I is surjective on 𝔞-primary components.

References

• R. Hartshorne, Algebraic Geometry, Chapter III, Lemma 3.2 and Proposition 3.3.

instance Ideal.injective_primaryComponent {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Type v} [AddCommGroup M] [Module R M] [Small.{v, u} R] [Module.Injective R M] (𝔞 : Ideal R) : Module.Injective R ↥(primaryComponent M 𝔞)

The 𝔞-primary component of an injective module over a Noetherian ring is injective (Hartshorne, Algebraic Geometry, Lemma III.3.2).

theorem Submonoid.surjective_of_isLocalizedModule {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Type v} [AddCommGroup M] [Module R M] [Small.{v, u} R] [Module.Injective R M] (S : Submonoid R) {M' : Type u_1} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : Function.Surjective ⇑f

A localization of an injective module over a Noetherian ring is a quotient of it (Hartshorne, Algebraic Geometry, Proposition III.3.3): if M is injective and f : M → M' is a localization map at a multiplicative subset S, then f is surjective.

theorem Ideal.primaryComponent_map_surjective {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Type v} [AddCommGroup M] [Module R M] [Small.{v, u} R] [Module.Injective R M] (𝔞 : Ideal R) (S : Submonoid R) {M' : Type u_1} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : Function.Surjective ⇑(primaryComponent.map 𝔞 f)

Localization of an injective module is surjective on primary components. Let M be an injective module over a Noetherian ring and f : M → M' a localization map at S. Every element of M' killed by a power of an ideal 𝔞 is the image of an element of M killed by a power of 𝔞.