Pseudo-null modules

A module M over a commutative ring A is pseudo-null if it is finitely generated and its localization M_𝔭 vanishes at every prime 𝔭 of height at most one; equivalently, every prime in the support of M has height at least two. Pseudo-null modules are the modules that the structure theory of finitely generated modules over a noetherian normal domain ignores: that theory classifies modules up to maps with pseudo-null kernel and cokernel (pseudo-isomorphisms), and the characteristic ideal of a torsion module only sees its localizations at height-one primes.

Over the Iwasawa algebra Λ = O⟦T⟧ of a complete discrete valuation ring O with finite residue field, a two-dimensional noetherian local ring, the pseudo-null modules are exactly the finite ones (isPseudoNull_iff_finite). The statement is proved for any noetherian local ring of Krull dimension two with finite residue field.

Main definitions

• TauCeti.Iwasawa.IsPseudoNull A M: M is finitely generated and M_𝔭 = 0 for every prime 𝔭 of A of height at most one.

Main results

• TauCeti.Iwasawa.isPseudoNull_iff_support: M is pseudo-null iff it is finitely generated and every prime of its support has height at least two.
• TauCeti.Iwasawa.isPseudoNull_iff_annihilator: the annihilator criterion, every prime containing ann_A M has height at least two; for a quotient A ⧸ I this is TauCeti.Iwasawa.isPseudoNull_quotient_iff. A variant relative to another module N, TauCeti.Iwasawa.isPseudoNull_of_mem_annihilator, needs only one annihilating element lying in no prime of height at most one in the support of N.
• TauCeti.Iwasawa.IsPseudoNull.isTorsion: over a domain, pseudo-null modules are torsion.
• TauCeti.Iwasawa.isPseudoNull_iff_subsingleton: over a ring of dimension at most one, such as a Dedekind domain, only the zero module is pseudo-null.
• TauCeti.Iwasawa.IsPseudoNull.of_injective, TauCeti.Iwasawa.IsPseudoNull.of_surjective and TauCeti.Iwasawa.IsPseudoNull.of_exact: over a noetherian ring, submodules, quotients and extensions of pseudo-null modules are pseudo-null.
• TauCeti.Iwasawa.isPseudoNull_iff_finite: over a noetherian local ring of dimension two with finite residue field, a module is pseudo-null iff it is finite.

The examples at the end of the file check the definition over Λ = ℤ_p⟦T⟧: the module Λ ⧸ (p, T) = 𝔽_p is pseudo-null, while Λ ⧸ (p) is not, because its support contains the height-one prime (p); and over ℤ_p itself, 𝔽_p is not pseudo-null.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (5.1.4) with Remarks 1–4.
• J. Rodrigues Jacinto and C. Williams, An introduction to p-adic L-functions, §13.1.

structure TauCeti.Iwasawa.IsPseudoNull (A : Type u_1) [CommRing A] (M : Type u_2) [AddCommGroup M] [Module A M] : Prop

A module M over a commutative ring A is pseudo-null if it is finitely generated and its localization at every prime of height at most one vanishes.

• finite : Module.Finite A M

  A pseudo-null module is finitely generated.

• subsingleton_localizedModule (𝔭 : PrimeSpectrum A) (h𝔭 : 𝔭.asIdeal.height ≤ 1) : Subsingleton (LocalizedModule 𝔭.asIdeal.primeCompl M)

  The localization of a pseudo-null module at a prime of height at most one vanishes.

theorem TauCeti.Iwasawa.isPseudoNull_iff_support {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] : IsPseudoNull A M ↔ Module.Finite A M ∧ ∀ 𝔭 ∈ Module.support A M, 1 < 𝔭.asIdeal.height

A module is pseudo-null iff it is finitely generated and every prime in its support has height at least two.

theorem TauCeti.Iwasawa.IsPseudoNull.one_lt_height {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] (h : IsPseudoNull A M) {𝔭 : PrimeSpectrum A} (h𝔭 : 𝔭 ∈ Module.support A M) : 1 < 𝔭.asIdeal.height

Every prime in the support of a pseudo-null module has height at least two.

theorem TauCeti.Iwasawa.isPseudoNull_iff_annihilator {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] : IsPseudoNull A M ↔ ∀ (𝔭 : PrimeSpectrum A), Module.annihilator A M ≤ 𝔭.asIdeal → 1 < 𝔭.asIdeal.height

The annihilator criterion: a finitely generated module is pseudo-null iff every prime containing its annihilator has height at least two.

theorem TauCeti.Iwasawa.isPseudoNull_quotient_iff {A : Type u_1} [CommRing A] (I : Ideal A) : IsPseudoNull A (A ⧸ I) ↔ ∀ (𝔭 : PrimeSpectrum A), I ≤ 𝔭.asIdeal → 1 < 𝔭.asIdeal.height

The quotient A ⧸ I is pseudo-null iff every prime containing I has height at least two.

theorem TauCeti.Iwasawa.isPseudoNull_of_mem_annihilator {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {N : Type u_3} [AddCommGroup N] [Module A N] [Module.Finite A M] {a : A} (ha : ∀ 𝔭 ∈ Module.support A N, 𝔭.asIdeal.height ≤ 1 → a ∉ 𝔭.asIdeal) (haM : a ∈ Module.annihilator A M) (hM : Module.support A M ⊆ Module.support A N) : IsPseudoNull A M

A finitely generated module M killed by a, with support inside the support of N, is pseudo-null, provided a lies in no prime of height at most one in the support of N.

theorem TauCeti.Iwasawa.IsPseudoNull.of_subsingleton {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Subsingleton M] : IsPseudoNull A M

The zero module is pseudo-null.

theorem TauCeti.Iwasawa.IsPseudoNull.isTorsion {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsDomain A] (h : IsPseudoNull A M) : Module.IsTorsion A M

Over a domain, a pseudo-null module is torsion: its localization at the height-zero prime ⊥ vanishes.

theorem TauCeti.Iwasawa.isPseudoNull_iff_subsingleton {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Ring.KrullDimLE 1 A] : IsPseudoNull A M ↔ Subsingleton M

Over a ring of Krull dimension at most one, such as a Dedekind domain, only the zero module is pseudo-null.

theorem TauCeti.Iwasawa.IsPseudoNull.of_injective {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsNoetherianRing A] {N : Type u_3} [AddCommGroup N] [Module A N] (h : IsPseudoNull A N) (f : M →ₗ[A] N) (hf : Function.Injective ⇑f) : IsPseudoNull A M

A submodule of a pseudo-null module over a noetherian ring is pseudo-null.

theorem TauCeti.Iwasawa.IsPseudoNull.of_surjective {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {N : Type u_3} [AddCommGroup N] [Module A N] (h : IsPseudoNull A M) (f : M →ₗ[A] N) (hf : Function.Surjective ⇑f) : IsPseudoNull A N

A quotient of a pseudo-null module is pseudo-null.

theorem TauCeti.Iwasawa.IsPseudoNull.of_exact {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {N : Type u_3} {P : Type u_4} [AddCommGroup N] [Module A N] [AddCommGroup P] [Module A P] {f : M →ₗ[A] N} {g : N →ₗ[A] P} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hM : IsPseudoNull A M) (hP : IsPseudoNull A P) : IsPseudoNull A N

An extension of pseudo-null modules is pseudo-null.

theorem TauCeti.Iwasawa.IsPseudoNull.prod {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {N : Type u_3} [AddCommGroup N] [Module A N] (hM : IsPseudoNull A M) (hN : IsPseudoNull A N) : IsPseudoNull A (M × N)

A product of two pseudo-null modules is pseudo-null.

theorem TauCeti.Iwasawa.isPseudoNull_iff_of_exact {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsNoetherianRing A] {N : Type u_3} {P : Type u_4} [AddCommGroup N] [Module A N] [AddCommGroup P] [Module A P] {f : M →ₗ[A] N} {g : N →ₗ[A] P} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : IsPseudoNull A N ↔ IsPseudoNull A M ∧ IsPseudoNull A P

In a short exact sequence over a noetherian ring, the middle term is pseudo-null iff both outer terms are.

theorem TauCeti.Iwasawa.isPseudoNull_iff_finite {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsLocalRing A] [IsNoetherianRing A] [Finite (IsLocalRing.ResidueField A)] (hdim : ringKrullDim A = 2) : IsPseudoNull A M ↔ Finite M

Over a noetherian local ring of dimension two with finite residue field, for example the Iwasawa algebra O⟦T⟧ of a complete discrete valuation ring O with finite residue field, a module is pseudo-null iff it is finite.