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 Mif the prime idealIis the annihilator of somex : 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, anyann(x)is contained in an associated prime forx ≠ 0.associated_primes.eq_singleton_of_is_primary: In a noetherian ring,I.radicalis the only associated prime ofR ⧸ IwhenIis 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)
[add_comm_group M]
[module R M] :
Prop
is_associated_prime I M if the prime ideal I is the annihilator of some x : M.
Equations
- is_associated_prime I M = (I.is_prime ∧ ∃ (x : M), I = (submodule.span R {x}).annihilator)
The set of associated primes of a module.
Equations
- associated_primes R M = {I : ideal R | is_associated_prime I M}
theorem
associate_primes.mem_iff
{R : Type u_1}
[comm_ring R]
{I : ideal R}
{M : Type u_2}
[add_comm_group M]
[module R M] :
I ∈ associated_primes R M ↔ is_associated_prime I M
theorem
is_associated_prime.is_prime
{R : Type u_1}
[comm_ring R]
{I : ideal R}
{M : Type u_2}
[add_comm_group M]
[module R M]
(h : is_associated_prime I M) :
I.is_prime
theorem
is_associated_prime.map_of_injective
{R : Type u_1}
[comm_ring R]
{I : ideal R}
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
(f : M →ₗ[R] M')
(h : is_associated_prime I M)
(hf : function.injective ⇑f) :
is_associated_prime I M'
theorem
linear_equiv.is_associated_prime_iff
{R : Type u_1}
[comm_ring R]
{I : ideal R}
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
(l : M ≃ₗ[R] M') :
is_associated_prime I M ↔ is_associated_prime I M'
theorem
not_is_associated_prime_of_subsingleton
{R : Type u_1}
[comm_ring R]
{I : ideal R}
{M : Type u_2}
[add_comm_group M]
[module R M]
[subsingleton M] :
theorem
exists_le_is_associated_prime_of_is_noetherian_ring
(R : Type u_1)
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
[H : is_noetherian_ring R]
(x : M)
(hx : x ≠ 0) :
∃ (P : ideal R), is_associated_prime P M ∧ (submodule.span R {x}).annihilator ≤ P
theorem
associated_primes.subset_of_injective
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
(f : M →ₗ[R] M')
(hf : function.injective ⇑f) :
associated_primes R M ⊆ associated_primes R M'
theorem
linear_equiv.associated_primes.eq
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
(l : M ≃ₗ[R] M') :
associated_primes R M = associated_primes R M'
theorem
associated_primes.eq_empty_of_subsingleton
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
[subsingleton M] :
associated_primes R M = ∅
theorem
associated_primes.nonempty
(R : Type u_1)
[comm_ring R]
(M : Type u_2)
[add_comm_group M]
[module R M]
[is_noetherian_ring R]
[nontrivial M] :
(associated_primes R M).nonempty
theorem
is_associated_prime.annihilator_le
{R : Type u_1}
[comm_ring R]
{I : ideal R}
{M : Type u_2}
[add_comm_group M]
[module R M]
(h : is_associated_prime I M) :
⊤.annihilator ≤ I
theorem
is_associated_prime.eq_radical
{R : Type u_1}
[comm_ring R]
{I J : ideal R}
(hI : I.is_primary)
(h : is_associated_prime J (R ⧸ I)) :
theorem
associated_primes.eq_singleton_of_is_primary
{R : Type u_1}
[comm_ring R]
{I : ideal R}
[is_noetherian_ring R]
(hI : I.is_primary) :
associated_primes R (R ⧸ I) = {I.radical}