Characteristic ideal of a finitely generated module over a Noetherian ring

Results should be PR into mathlib

theorem Module.IsTorsion.not_disjoint_nonZeroDivisors_of_mem_support {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] (H : IsTorsion A M) (p : PrimeSpectrum A) : p ∈ support A M → ¬Disjoint ↑p.asIdeal ↑(nonZeroDivisors A)

theorem Module.IsTorsion.one_le_primeHeight_of_mem_support {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] (H : IsTorsion A M) (p : PrimeSpectrum A) : p ∈ support A M → 1 ≤ p.asIdeal.primeHeight

theorem Module.isTorsion_iff_subsingleton_localizedModule_nonZeroDivisors {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] : IsTorsion A M ↔ Subsingleton (LocalizedModule (nonZeroDivisors A) M)

theorem Module.IsTorsion.subsingleton_localizedModule_nonZeroDivisors {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] : IsTorsion A M → Subsingleton (LocalizedModule (nonZeroDivisors A) M)

Alias of the forward direction of Module.isTorsion_iff_subsingleton_localizedModule_nonZeroDivisors.

theorem Module.IsTorsion.injective {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {M' : Type u_3} [AddCommGroup M'] [Module A M'] (H : IsTorsion A M') {f : M →ₗ[A] M'} (hf : Function.Injective ⇑f) : IsTorsion A M

theorem Module.IsTorsion.surjective {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {M' : Type u_3} [AddCommGroup M'] [Module A M'] (H : IsTorsion A M) {f : M →ₗ[A] M'} (hf : Function.Surjective ⇑f) : IsTorsion A M'

theorem LinearEquiv.isTorsion {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {M' : Type u_3} [AddCommGroup M'] [Module A M'] (f : M ≃ₗ[A] M') : Module.IsTorsion A M ↔ Module.IsTorsion A M'

theorem Function.Exact.subsingleton {M : Type u_1} {N : Type u_2} {P : Type u_3} {f : M → N} {g : N → P} [Zero P] (H : Exact f g) [Subsingleton M] [Subsingleton P] : Subsingleton N

theorem Module.IsTorsion.exact {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {M' : Type u_3} [AddCommGroup M'] [Module A M'] {M'' : Type u_4} [AddCommGroup M''] [Module A M''] (h1 : IsTorsion A M) (h2 : IsTorsion A M'') (f : M →ₗ[A] M') (g : M' →ₗ[A] M'') (hfg : Function.Exact ⇑f ⇑g) : IsTorsion A M'

theorem Module.IsTorsion.prod {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {M'' : Type u_3} [AddCommGroup M''] [Module A M''] (h1 : IsTorsion A M) (h2 : IsTorsion A M'') : IsTorsion A (M × M'')

Actual contents of the file

theorem Ring.support_quotient {A : Type u} [CommRing A] (I : Ideal A) : Module.support A (A ⧸ I) = PrimeSpectrum.zeroLocus ↑I

theorem Module.IsTorsion.finite_primeHeight_one_support {A : Type u} [CommRing A] [IsNoetherianRing A] {M : Type v} [AddCommGroup M] [Module A M] [Module.Finite A M] (H : IsTorsion A M) : (support A M ∩ {p : PrimeSpectrum A | p.asIdeal.primeHeight = 1}).Finite

There are only finitely many height one primes contained in the support of a finitely generated torsion module over a Noetherian ring.

theorem Module.length_localizedModule_primeCompl_quotient_prime_eq_of_primeHeight_le {A : Type u} [CommRing A] {p q : PrimeSpectrum A} (hp : p.asIdeal.primeHeight ≠ ⊤) (hq : p.asIdeal.primeHeight ≤ q.asIdeal.primeHeight) : length (Localization p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl (A ⧸ q.asIdeal)) = if p = q then 1 else 0

theorem Module.isFiniteLength_localizedModule_primeCompl_quotient_prime_of_primeHeight_le {A : Type u} [CommRing A] {p q : PrimeSpectrum A} (hp : p.asIdeal.primeHeight ≠ ⊤) (hq : p.asIdeal.primeHeight ≤ q.asIdeal.primeHeight) : IsFiniteLength (Localization p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl (A ⧸ q.asIdeal))

theorem Module.IsTorsion.isFiniteLength_localizedModule_of_primeHeight_le_one {A : Type u} [CommRing A] [IsNoetherianRing A] {M : Type v} [AddCommGroup M] [Module A M] [Module.Finite A M] (H : IsTorsion A M) (p : PrimeSpectrum A) (hp : p.asIdeal.primeHeight ≤ 1) : IsFiniteLength (Localization p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M)

Let M be a finitely generated torsion module over a Noetherian ring A. For any prime ideal p of A of height ≤ 1, the Mₚ is of finite length over Aₚ.

noncomputable def Module.charIdeal (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] : Ideal A

The characteristic ideal char(M) of a module M over a ring A. It is mathematically correct if the module is finitely generated torsion over a Noetherian ring.

Equations

• One or more equations did not get rendered due to their size.

theorem Module.charIdeal_eq_prod_of_support_subset (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] (s : Finset (PrimeSpectrum A)) (hh : ∀ p ∈ s, p.asIdeal.primeHeight = 1) (hs : support A M ∩ {p : PrimeSpectrum A | p.asIdeal.primeHeight = 1} ⊆ ↑s) : charIdeal A M = ∏ p ∈ s, p.asIdeal ^ (length (Localization p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M)).toNat

theorem Module.IsTorsion.charIdeal_eq_mul_of_exact {A : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing A] [IsNoetherianRing A] [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [AddCommGroup P] [Module A P] [Module.Finite A N] (H : IsTorsion A N) (f : M →ₗ[A] N) (g : N →ₗ[A] P) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hfg : Function.Exact ⇑f ⇑g) : charIdeal A N = charIdeal A M * charIdeal A P

If 0 → M → N → P → 0 is a short exact sequence of fintely generated torsion modules over a Noetherian ring, then char(N) = char(M) * char(P).

theorem Module.IsTorsion.charIdeal_dvd_of_injective {A : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing A] [IsNoetherianRing A] [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [Module.Finite A N] (H : IsTorsion A N) (f : M →ₗ[A] N) (hf : Function.Injective ⇑f) : charIdeal A M ∣ charIdeal A N

theorem Module.IsTorsion.charIdeal_dvd_of_surjective {A : Type u_1} {N : Type u_2} {P : Type u_3} [CommRing A] [IsNoetherianRing A] [AddCommGroup N] [Module A N] [AddCommGroup P] [Module A P] [Module.Finite A N] (H : IsTorsion A N) (g : N →ₗ[A] P) (hg : Function.Surjective ⇑g) : charIdeal A P ∣ charIdeal A N

theorem Module.IsTorsion.charIdeal_prod {A : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing A] [IsNoetherianRing A] [AddCommGroup M] [Module A M] [AddCommGroup P] [Module A P] [Module.Finite A M] [Module.Finite A P] (HM : IsTorsion A M) (HP : IsTorsion A P) : charIdeal A (M × P) = charIdeal A M * charIdeal A P

theorem Module.charIdeal_eq_one_of_subsingleton (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] [Subsingleton M] : charIdeal A M = 1

theorem LinearEquiv.charIdeal_eq {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {M' : Type u_3} [AddCommGroup M'] [Module A M'] (f : M ≃ₗ[A] M') : Module.charIdeal A M = Module.charIdeal A M'

theorem Module.charIdeal_quotient_prime_eq_of_one_le_primeHeight {A : Type u} [CommRing A] (p : PrimeSpectrum A) (hp : 1 ≤ p.asIdeal.primeHeight) : charIdeal A (A ⧸ p.asIdeal) = if p.asIdeal.primeHeight = 1 then p.asIdeal else 1