Annihilators of finite modules commute with localization

Let M be a finitely generated module over a commutative ring R, and let M' be its localization at a submonoid S, a module over the localization A of R at S. Then

Ann_A(M') = Ann_R(M) A.

An element r / s annihilates M' exactly when every generator of M is killed by r after multiplication by some element of S; the product of these finitely many elements of S then multiplies r into Ann_R(M). Without finite generation only the inclusion ⊇ holds.

This is the compatibility that lets the annihilators of the modules of sections of a quasi-coherent module of finite type glue to an ideal sheaf.

Main results

• IsLocalizedModule.map_annihilator_le: Ann_R(M) A ≤ Ann_A(M') for an arbitrary module M.
• IsLocalizedModule.annihilator_eq_map: Ann_A(M') = Ann_R(M) A for a finite module M.

References

• M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Proposition 3.14.

theorem IsLocalizedModule.map_annihilator_le {R : Type u_1} [CommRing R] (S : Submonoid R) (A : Type u_2) [CommRing A] [Algebra R A] {M : Type u_3} {M' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : Ideal.map (algebraMap R A) (Module.annihilator R M) ≤ Module.annihilator A M'

The extension of the annihilator of M annihilates every localization of M. This holds without any finiteness assumption on M, and for any R-algebra A acting compatibly on M'.

theorem IsLocalizedModule.annihilator_eq_map {R : Type u_1} [CommRing R] (S : Submonoid R) (A : Type u_2) [CommRing A] [Algebra R A] [IsLocalization S A] {M : Type u_3} {M' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [Module.Finite R M] : Module.annihilator A M' = Ideal.map (algebraMap R A) (Module.annihilator R M)

Annihilators of finite modules commute with localization. If M is a finite R-module and f : M → M' is the localization of M at a submonoid S, with A the localization of R at S, then the annihilator of M' over A is the extension of the annihilator of M.