Primes of small height in the support of a torsion module

A finitely generated torsion module M over a noetherian ring A vanishes at every minimal prime of A, so every prime of height at most one in its support is minimal over the annihilator of M. Hence there are only finitely many such primes (Module.IsTorsion.finite_setOf_mem_support_height_le_one). Over a noetherian normal domain these are the height-one primes at which the characteristic divisor of M is supported, and the finiteness is what makes prime avoidance available for them (Module.IsTorsion.exists_mem_forall_notMem_of_forall_not_le).

The localization of M at a prime of height at most one is a finitely generated module over a noetherian local ring of dimension at most one, killed by a non-zero-divisor, so it has finite length (Module.IsTorsion.isFiniteLength_localizedModule). These local lengths are the multiplicities of the characteristic divisor.

Every prime in the support of a finite product ∏ᵢ A ⧸ 𝔭 ^ nᵢ contains 𝔭 (Module.le_of_mem_support_pi_quotient_pow).

A finite module each of whose elements is killed by an element outside a prime P is killed by a single element outside P (Module.exists_notMem_forall_smul_eq_zero).

theorem Module.IsTorsion.notMem_support_of_mem_minimalPrimes {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] (hM : IsTorsion A M) {𝔭 : PrimeSpectrum A} (h𝔭 : 𝔭.asIdeal ∈ minimalPrimes A) : 𝔭 ∉ support A M

A torsion module vanishes at every minimal prime of the ring: elements of a minimal prime are zero divisors.

theorem Module.IsTorsion.finite_setOf_mem_support_height_le_one {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [IsNoetherianRing A] [Module.Finite A M] (hM : IsTorsion A M) : {𝔭 : PrimeSpectrum A | 𝔭 ∈ support A M ∧ 𝔭.asIdeal.height ≤ 1}.Finite

A finitely generated torsion module over a noetherian ring has only finitely many primes of height at most one in its support.

theorem Module.IsTorsion.exists_mem_forall_notMem_of_forall_not_le {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [IsNoetherianRing A] [Module.Finite A M] (hM : IsTorsion A M) {I : Ideal A} (hI : ∀ 𝔭 ∈ support A M, 𝔭.asIdeal.height ≤ 1 → ¬I ≤ 𝔭.asIdeal) : ∃ a ∈ I, ∀ 𝔭 ∈ support A M, 𝔭.asIdeal.height ≤ 1 → a ∉ 𝔭.asIdeal

Prime avoidance for the primes of height at most one in the support of a finitely generated torsion module over a noetherian ring: an ideal contained in none of them has an element lying in none of them.

theorem Module.IsTorsion.isFiniteLength_localizedModule {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [IsNoetherianRing A] [Module.Finite A M] (hM : IsTorsion A M) {𝔭 : PrimeSpectrum A} (h𝔭 : 𝔭.asIdeal.height ≤ 1) : IsFiniteLength (Localization.AtPrime 𝔭.asIdeal) (LocalizedModule 𝔭.asIdeal.primeCompl M)

The localization of a finitely generated torsion module over a noetherian ring at a prime of height at most one has finite length.

theorem Module.le_of_mem_support_pi_quotient_pow {A : Type u_1} [CommRing A] {ι : Type u_2} [Finite ι] {𝔭 : Ideal A} {n : ι → ℕ} {𝔮 : PrimeSpectrum A} (h : 𝔮 ∈ support A ((i : ι) → A ⧸ 𝔭 ^ n i)) : 𝔭 ≤ 𝔮.asIdeal

A prime in the support of ∏ᵢ A ⧸ 𝔭 ^ nᵢ contains 𝔭.

theorem Module.exists_notMem_forall_smul_eq_zero {A : Type u_1} [CommRing A] {P : Ideal A} [P.IsPrime] (M : Type u_2) [AddCommGroup M] [Module A M] [Module.Finite A M] (h : ∀ (m : M), ∃ r ∉ P, r • m = 0) : ∃ r ∉ P, ∀ (m : M), r • m = 0

A finite module each of whose elements is killed by an element outside the prime P is killed by a single element outside P: the module vanishes at P, so its annihilator is not contained in P.