mathlib3documentation

ring_theory.ideal.associated_prime

Associated primes of a module #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definition #

• is_associated_prime: is_associated_prime I M if the prime ideal I is the annihilator of some x : M.
• associated_primes: The set of associated primes of a module.

Main results #

• exists_le_is_associated_prime_of_is_noetherian_ring: In a noetherian ring, any ann(x) is contained in an associated prime for x ≠ 0.
• associated_primes.eq_singleton_of_is_primary: In a noetherian ring, I.radical is the only associated prime of R ⧸ I when I is primary.

Todo #

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

def is_associated_prime {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
Prop

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

Equations
def associated_primes (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] :

The set of associated primes of a module.

Equations
• = {I : |
theorem associate_primes.mem_iff {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] :
I
theorem is_associated_prime.is_prime {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] (h : M) :
theorem is_associated_prime.map_of_injective {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] {M' : Type u_3} [add_comm_group M'] [ M'] (f : M →ₗ[R] M') (h : M) (hf : function.injective f) :
theorem linear_equiv.is_associated_prime_iff {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] {M' : Type u_3} [add_comm_group M'] [ M'] (l : M ≃ₗ[R] M') :
theorem not_is_associated_prime_of_subsingleton {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] [subsingleton M] :
theorem exists_le_is_associated_prime_of_is_noetherian_ring (R : Type u_1) [comm_ring R] {M : Type u_2} [ M] [H : is_noetherian_ring R] (x : M) (hx : x 0) :
(P : ideal R), {x}).annihilator P
theorem associated_primes.subset_of_injective {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {M' : Type u_3} [add_comm_group M'] [ M'] (f : M →ₗ[R] M') (hf : function.injective f) :
theorem linear_equiv.associated_primes.eq {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {M' : Type u_3} [add_comm_group M'] [ M'] (l : M ≃ₗ[R] M') :
=
theorem associated_primes.nonempty (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] [nontrivial M] :
theorem is_associated_prime.annihilator_le {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] (h : M) :
theorem is_associated_prime.eq_radical {R : Type u_1} [comm_ring R] {I J : ideal R} (hI : I.is_primary) (h : (R I)) :
theorem associated_primes.eq_singleton_of_is_primary {R : Type u_1} [comm_ring R] {I : ideal R} (hI : I.is_primary) :