Finite length at a minimal prime of a finite module

This file isolates the commutative-algebra localization statement used later: if P is minimal over the annihilator of a finite module, then localization at P is nonzero and has finite length.

theorem AlgebraicAnalysis.MinimalPrimeFiniteLengthLocalization.finiteLength_of_maximalIdeal_pow_smul_eq_bot {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [IsLocalRing A] [IsNoetherianRing A] [Module.Finite A M] {n : ℕ} (hpow : IsLocalRing.maximalIdeal A ^ n • ⊤ = ⊥) : IsFiniteLength A M

A finite module over a Noetherian local ring has finite length as soon as a power of the maximal ideal annihilates it.

theorem AlgebraicAnalysis.MinimalPrimeFiniteLengthLocalization.localizedModule_finite {R : Type u_3} {G : Type u_4} [CommRing R] [AddCommGroup G] [Module R G] [Module.Finite R G] (P : Ideal R) [P.IsPrime] : Module.Finite (Localization P.primeCompl) (LocalizedModule P.primeCompl G)

Localization preserves finite generation for the canonical localized module.

theorem AlgebraicAnalysis.MinimalPrimeFiniteLengthLocalization.localizedModule_nontrivial {R : Type u_3} {G : Type u_4} [CommRing R] [AddCommGroup G] [Module R G] [Module.Finite R G] (P : Ideal R) [P.IsPrime] (hP : P ∈ (Module.annihilator R G).minimalPrimes) : Nontrivial (LocalizedModule P.primeCompl G)

A minimal prime over the annihilator belongs to the support, so the corresponding localization is nonzero.

theorem AlgebraicAnalysis.MinimalPrimeFiniteLengthLocalization.maximalIdeal_le_radical_map_annihilator {R : Type u_3} {G : Type u_4} [CommRing R] [AddCommGroup G] [Module R G] (P : Ideal R) [P.IsPrime] (hP : P ∈ (Module.annihilator R G).minimalPrimes) : IsLocalRing.maximalIdeal (Localization P.primeCompl) ≤ (Ideal.map (algebraMap R (Localization P.primeCompl)) (Module.annihilator R G)).radical

At a minimal prime over the module annihilator, the localized maximal ideal lies in the radical of the mapped annihilator.

theorem AlgebraicAnalysis.MinimalPrimeFiniteLengthLocalization.map_annihilator_le_localized_annihilator {R : Type u_3} {G : Type u_4} [CommRing R] [AddCommGroup G] [Module R G] (P : Ideal R) [P.IsPrime] : Ideal.map (algebraMap R (Localization P.primeCompl)) (Module.annihilator R G) ≤ Module.annihilator (Localization P.primeCompl) (LocalizedModule P.primeCompl G)

Mapping the original annihilator into the localization gives elements that annihilate every localized fraction.

theorem AlgebraicAnalysis.MinimalPrimeFiniteLengthLocalization.exists_maximalIdeal_pow_le_localized_annihilator {R : Type u_3} {G : Type u_4} [CommRing R] [AddCommGroup G] [Module R G] [IsNoetherianRing R] (P : Ideal R) [P.IsPrime] (hP : P ∈ (Module.annihilator R G).minimalPrimes) : ∃ (n : ℕ), IsLocalRing.maximalIdeal (Localization P.primeCompl) ^ n ≤ Module.annihilator (Localization P.primeCompl) (LocalizedModule P.primeCompl G)

A power of the localized maximal ideal annihilates the localized finite module.

theorem AlgebraicAnalysis.MinimalPrimeFiniteLengthLocalization.localizedModule_isFiniteLength {R : Type u_3} {G : Type u_4} [CommRing R] [AddCommGroup G] [Module R G] [IsNoetherianRing R] [Module.Finite R G] (P : Ideal R) [P.IsPrime] (hP : P ∈ (Module.annihilator R G).minimalPrimes) : IsFiniteLength (Localization P.primeCompl) (LocalizedModule P.primeCompl G)

The localized module at a minimal prime over its annihilator has finite length over the local ring.

theorem AlgebraicAnalysis.MinimalPrimeFiniteLengthLocalization.localizedModule_nontrivial_and_isFiniteLength {R : Type u_3} {G : Type u_4} [CommRing R] [AddCommGroup G] [Module R G] [IsNoetherianRing R] [Module.Finite R G] (P : Ideal R) [P.IsPrime] (hP : P ∈ (Module.annihilator R G).minimalPrimes) : Nontrivial (LocalizedModule P.primeCompl G) ∧ IsFiniteLength (Localization P.primeCompl) (LocalizedModule P.primeCompl G)

The load-bearing package: localization at a minimal prime over the annihilator is simultaneously nonzero and of finite length.