Documentation

Mathlib.RingTheory.Ideal.AssociatedPrime

Associated primes of a module #

We provide the definition and related lemmas about associated primes of modules.

Main definition #

Main results #

TODO #

Generalize this to a non-commutative setting once there are annihilator for non-commutative rings.

def IsAssociatedPrime {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] :

IsAssociatedPrime I M if the prime ideal I is the annihilator of some x : M.

Equations
Instances For
    def associatedPrimes (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

    The set of associated primes of a module.

    Equations
    Instances For
      theorem IsAssociatedPrime.isPrime {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (h : IsAssociatedPrime I M) :
      I.IsPrime
      theorem IsAssociatedPrime.map_of_injective {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (h : IsAssociatedPrime I M) (hf : Function.Injective f) :
      theorem LinearEquiv.isAssociatedPrime_iff {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (l : M ≃ₗ[R] M') :
      theorem exists_le_isAssociatedPrime_of_isNoetherianRing (R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [H : IsNoetherianRing R] (x : M) (hx : x 0) :
      ∃ (P : Ideal R), IsAssociatedPrime P M (Submodule.span R {x}).annihilator P
      theorem associatedPrimes.subset_of_injective {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Injective f) :
      theorem LinearEquiv.AssociatedPrimes.eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (l : M ≃ₗ[R] M') :
      theorem associatedPrimes.nonempty (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Nontrivial M] :
      (associatedPrimes R M).Nonempty
      theorem biUnion_associatedPrimes_eq_zero_divisors (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherianRing R] :
      passociatedPrimes R M, p = {r : R | ∃ (x : M), x 0 r x = 0}
      theorem IsAssociatedPrime.annihilator_le {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (h : IsAssociatedPrime I M) :
      .annihilator I
      theorem IsAssociatedPrime.eq_radical {R : Type u_1} [CommRing R] {I : Ideal R} {J : Ideal R} (hI : I.IsPrimary) (h : IsAssociatedPrime J (R I)) :
      J = I.radical
      theorem associatedPrimes.eq_singleton_of_isPrimary {R : Type u_1} [CommRing R] {I : Ideal R} [IsNoetherianRing R] (hI : I.IsPrimary) :
      associatedPrimes R (R I) = {I.radical}