mathlib documentation

ring_theory.ideal.associated_prime

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 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
def associated_primes (R : Type u_1) [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :

The set of associated primes of a module.

Equations
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] :
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) :
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) :
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') :
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) :
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') :
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)) :