mathlib documentation

ring_theory.ideal.operations

More operations on modules and ideals

@[instance]
def submodule.has_scalar' {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :

Equations
def submodule.annihilator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :
submodule R Mideal R

N.annihilator is the ideal of all elements r : R such that r • N = 0.

Equations
def submodule.colon {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :
submodule R Msubmodule R Mideal R

N.colon P is the ideal of all elements r : R such that r • P ⊆ N.

Equations
theorem submodule.mem_annihilator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N : submodule R M} {r : R} :
r N.annihilator ∀ (n : M), n Nr n = 0

theorem submodule.mem_annihilator' {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N : submodule R M} {r : R} :

theorem submodule.annihilator_bot {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :

theorem submodule.annihilator_eq_top_iff {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N : submodule R M} :

theorem submodule.annihilator_mono {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N P : submodule R M} :

theorem submodule.annihilator_supr {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (ι : Sort w) (f : ι → submodule R M) :
(⨆ (i : ι), f i).annihilator = ⨅ (i : ι), (f i).annihilator

theorem submodule.mem_colon {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N P : submodule R M} {r : R} :
r N.colon P ∀ (p : M), p Pr p N

theorem submodule.mem_colon' {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N P : submodule R M} {r : R} :

theorem submodule.colon_mono {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N₁ N₂ P₁ P₂ : submodule R M} :
N₁ N₂P₁ P₂N₁.colon P₂ N₂.colon P₁

theorem submodule.infi_colon_supr {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (ι₁ : Sort w) (f : ι₁ → submodule R M) (ι₂ : Sort x) (g : ι₂ → submodule R M) :
(⨅ (i : ι₁), f i).colon (⨆ (j : ι₂), g j) = ⨅ (i : ι₁) (j : ι₂), (f i).colon (g j)

theorem submodule.smul_mem_smul {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N : submodule R M} {r : R} {n : M} :
r In Nr n I N

theorem submodule.smul_le {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N P : submodule R M} :
I N P ∀ (r : R), r I∀ (n : M), n Nr n P

theorem submodule.smul_induction_on {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N : submodule R M} {p : M → Prop} {x : M} :
x I N(∀ (r : R), r I∀ (n : M), n Np (r n))p 0(∀ (x y : M), p xp yp (x + y))(∀ (c : R) (n : M), p np (c n))p x

theorem submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {m x : M} :
x I submodule.span R {m} ∃ (y : R) (H : y I), y m = x

theorem submodule.smul_le_right {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N : submodule R M} :
I N N

theorem submodule.smul_mono {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I J : ideal R} {N P : submodule R M} :
I JN PI N J P

theorem submodule.smul_mono_left {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I J : ideal R} {N : submodule R M} :
I JI N J N

theorem submodule.smul_mono_right {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N P : submodule R M} :
N PI N I P

@[simp]
theorem submodule.smul_bot {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) :

@[simp]
theorem submodule.bot_smul {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (N : submodule R M) :

@[simp]
theorem submodule.top_smul {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (N : submodule R M) :
N = N

theorem submodule.smul_sup {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (N P : submodule R M) :
I (N P) = I N I P

theorem submodule.sup_smul {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I J : ideal R) (N : submodule R M) :
(I J) N = I N J N

theorem submodule.smul_assoc {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I J : ideal R) (N : submodule R M) :
(I J) N = I J N

theorem submodule.span_smul_span {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (S : set R) (T : set M) :
ideal.span S submodule.span R T = submodule.span R (⋃ (s : R) (H : s S) (t : M) (H : t T), {s t})

theorem submodule.map_smul'' {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (N : submodule R M) {M' : Type w} [add_comm_group M'] [module R M'] (f : M →ₗ[R] M') :

theorem ideal.exists_sub_one_mem_and_mem {R : Type u} [comm_ring R] {ι : Type v} (s : finset ι) {f : ι → ideal R} (hf : ∀ (i : ι), i s∀ (j : ι), j si jf i f j = ) (i : ι) :
i s(∃ (r : R), r - 1 f i ∀ (j : ι), j sj ir f j)

theorem ideal.exists_sub_mem {R : Type u} [comm_ring R] {ι : Type v} [fintype ι] {f : ι → ideal R} (hf : ∀ (i j : ι), i jf i f j = ) (g : ι → R) :
∃ (r : R), ∀ (i : ι), r - g i f i

def ideal.quotient_inf_to_pi_quotient {R : Type u} [comm_ring R] {ι : Type v} (f : ι → ideal R) :
(⨅ (i : ι), f i).quotient →+* Π (i : ι), (f i).quotient

The homomorphism from R/(⋂ i, f i) to ∏ i, (R / f i) featured in the Chinese Remainder Theorem. It is bijective if the ideals f i are comaximal.

Equations
theorem ideal.quotient_inf_to_pi_quotient_bijective {R : Type u} [comm_ring R] {ι : Type v} [fintype ι] {f : ι → ideal R} :
(∀ (i j : ι), i jf i f j = )function.bijective (ideal.quotient_inf_to_pi_quotient f)

def ideal.quotient_inf_ring_equiv_pi_quotient {R : Type u} [comm_ring R] {ι : Type v} [fintype ι] (f : ι → ideal R) :
(∀ (i j : ι), i jf i f j = )((⨅ (i : ι), f i).quotient ≃+* Π (i : ι), (f i).quotient)

Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT

Equations
@[instance]
def ideal.has_mul {R : Type u} [comm_ring R] :

Equations
theorem ideal.mul_mem_mul {R : Type u} [comm_ring R] {I J : ideal R} {r s : R} :
r Is Jr * s I * J

theorem ideal.mul_mem_mul_rev {R : Type u} [comm_ring R] {I J : ideal R} {r s : R} :
r Is Js * r I * J

theorem ideal.mul_le {R : Type u} [comm_ring R] {I J K : ideal R} :
I * J K ∀ (r : R), r I∀ (s : R), s Jr * s K

theorem ideal.mul_le_left {R : Type u} [comm_ring R] {I J : ideal R} :
I * J J

theorem ideal.mul_le_right {R : Type u} [comm_ring R] {I J : ideal R} :
I * J I

@[simp]
theorem ideal.sup_mul_right_self {R : Type u} [comm_ring R] {I J : ideal R} :
I I * J = I

@[simp]
theorem ideal.sup_mul_left_self {R : Type u} [comm_ring R] {I J : ideal R} :
I J * I = I

@[simp]
theorem ideal.mul_right_self_sup {R : Type u} [comm_ring R] {I J : ideal R} :
I * J I = I

@[simp]
theorem ideal.mul_left_self_sup {R : Type u} [comm_ring R] {I J : ideal R} :
J * I I = I

theorem ideal.mul_comm {R : Type u} [comm_ring R] (I J : ideal R) :
I * J = J * I

theorem ideal.mul_assoc {R : Type u} [comm_ring R] (I J K : ideal R) :
(I * J) * K = I * J * K

theorem ideal.span_mul_span {R : Type u} [comm_ring R] (S T : set R) :
(ideal.span S) * ideal.span T = ideal.span (⋃ (s : R) (H : s S) (t : R) (H : t T), {s * t})

theorem ideal.span_mul_span' {R : Type u} [comm_ring R] (S T : set R) :

theorem ideal.span_singleton_mul_span_singleton {R : Type u} [comm_ring R] (r s : R) :

theorem ideal.mul_le_inf {R : Type u} [comm_ring R] {I J : ideal R} :
I * J I J

theorem ideal.mul_eq_inf_of_coprime {R : Type u} [comm_ring R] {I J : ideal R} :
I J = I * J = I J

theorem ideal.mul_bot {R : Type u} [comm_ring R] (I : ideal R) :

theorem ideal.bot_mul {R : Type u} [comm_ring R] (I : ideal R) :

theorem ideal.mul_top {R : Type u} [comm_ring R] (I : ideal R) :
I * = I

theorem ideal.top_mul {R : Type u} [comm_ring R] (I : ideal R) :
* I = I

theorem ideal.mul_mono {R : Type u} [comm_ring R] {I J K L : ideal R} :
I KJ LI * J K * L

theorem ideal.mul_mono_left {R : Type u} [comm_ring R] {I J K : ideal R} :
I JI * K J * K

theorem ideal.mul_mono_right {R : Type u} [comm_ring R] {I J K : ideal R} :
J KI * J I * K

theorem ideal.mul_sup {R : Type u} [comm_ring R] (I J K : ideal R) :
I * (J K) = I * J I * K

theorem ideal.sup_mul {R : Type u} [comm_ring R] (I J K : ideal R) :
(I J) * K = I * K J * K

theorem ideal.pow_le_pow {R : Type u} [comm_ring R] {I : ideal R} {m n : } :
m nI ^ n I ^ m

theorem ideal.mul_eq_bot {R : Type u_1} [integral_domain R] {I J : ideal R} :
I * J = I = J =

def ideal.radical {R : Type u} [comm_ring R] :
ideal Rideal R

The radical of an ideal I consists of the elements r such that r^n ∈ I for some n.

Equations
theorem ideal.le_radical {R : Type u} [comm_ring R] {I : ideal R} :

theorem ideal.radical_top (R : Type u) [comm_ring R] :

theorem ideal.radical_mono {R : Type u} [comm_ring R] {I J : ideal R} :
I JI.radical J.radical

theorem ideal.radical_idem {R : Type u} [comm_ring R] (I : ideal R) :

theorem ideal.radical_eq_top {R : Type u} [comm_ring R] {I : ideal R} :

theorem ideal.is_prime.radical {R : Type u} [comm_ring R] {I : ideal R} :
I.is_primeI.radical = I

theorem ideal.radical_sup {R : Type u} [comm_ring R] (I J : ideal R) :

theorem ideal.radical_inf {R : Type u} [comm_ring R] (I J : ideal R) :

theorem ideal.radical_mul {R : Type u} [comm_ring R] (I J : ideal R) :

theorem ideal.is_prime.radical_le_iff {R : Type u} [comm_ring R] {I J : ideal R} :
J.is_prime(I.radical J I J)

theorem ideal.radical_eq_Inf {R : Type u} [comm_ring R] (I : ideal R) :
I.radical = Inf {J : ideal R | I J J.is_prime}

@[simp]
theorem ideal.add_eq_sup {R : Type u} [comm_ring R] {I J : ideal R} :
I + J = I J

@[simp]
theorem ideal.zero_eq_bot {R : Type u} [comm_ring R] :
0 =

@[simp]
theorem ideal.one_eq_top {R : Type u} [comm_ring R] :
1 =

theorem ideal.top_pow (R : Type u) [comm_ring R] (n : ) :

theorem ideal.radical_pow {R : Type u} [comm_ring R] (I : ideal R) (n : ) :
n > 0(I ^ n).radical = I.radical

def ideal.map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] :
(R →+* S)ideal Rideal S

I.map f is the span of the image of the ideal I under f, which may be bigger than the image itself.

Equations
def ideal.comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] :
(R →+* S)ideal Sideal R

I.comap f is the preimage of I under f.

Equations
theorem ideal.map_mono {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I J : ideal R} :
I Jideal.map f I ideal.map f J

theorem ideal.mem_map_of_mem {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} {x : R} :
x If x ideal.map f I

theorem ideal.map_le_iff_le_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :

@[simp]
theorem ideal.mem_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {K : ideal S} {x : R} :

theorem ideal.comap_mono {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {K L : ideal S} :
K Lideal.comap f K ideal.comap f L

theorem ideal.comap_ne_top {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K : ideal S} :

theorem ideal.is_prime.comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K : ideal S} [hK : K.is_prime] :

theorem ideal.map_top {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

theorem ideal.map_mul {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (I J : ideal R) :
ideal.map f (I * J) = (ideal.map f I) * ideal.map f J

theorem ideal.gc_map_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

@[simp]
theorem ideal.comap_id {R : Type u} [comm_ring R] (I : ideal R) :

@[simp]
theorem ideal.map_id {R : Type u} [comm_ring R] (I : ideal R) :

theorem ideal.comap_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {T : Type u_1} [comm_ring T] {I : ideal T} (f : R →+* S) (g : S →+* T) :

theorem ideal.map_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {T : Type u_1} [comm_ring T] {I : ideal R} (f : R →+* S) (g : S →+* T) :

theorem ideal.map_le_of_le_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :
I ideal.comap f Kideal.map f I K

theorem ideal.le_comap_of_map_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :
ideal.map f I KI ideal.comap f K

theorem ideal.le_comap_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} :

theorem ideal.map_comap_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {K : ideal S} :

@[simp]
theorem ideal.comap_top {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} :

@[simp]
theorem ideal.comap_eq_top_iff {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal S} :

@[simp]
theorem ideal.map_bot {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} :

@[simp]
theorem ideal.map_comap_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (I : ideal R) :

@[simp]
theorem ideal.comap_map_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K : ideal S) :

theorem ideal.map_sup {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (I J : ideal R) :

theorem ideal.comap_inf {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K L : ideal S) :

theorem ideal.map_supr {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {ι : Sort u_1} (K : ι → ideal R) :
ideal.map f (supr K) = ⨆ (i : ι), ideal.map f (K i)

theorem ideal.comap_infi {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {ι : Sort u_1} (K : ι → ideal S) :
ideal.comap f (infi K) = ⨅ (i : ι), ideal.comap f (K i)

theorem ideal.map_Sup {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (s : set (ideal R)) :
ideal.map f (Sup s) = ⨆ (I : ideal R) (H : I s), ideal.map f I

theorem ideal.comap_Inf {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (s : set (ideal S)) :
ideal.comap f (Inf s) = ⨅ (I : ideal S) (H : I s), ideal.comap f I

theorem ideal.comap_Inf' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (s : set (ideal S)) :
ideal.comap f (Inf s) = ⨅ (I : ideal R) (H : I ideal.comap f '' s), I

theorem ideal.comap_radical {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K : ideal S) :

theorem ideal.comap_is_prime {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K : ideal S) [H : K.is_prime] :

@[simp]
theorem ideal.map_quotient_self {R : Type u} [comm_ring R] (I : ideal R) :

theorem ideal.map_inf_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I J : ideal R} :

theorem ideal.map_radical_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :

theorem ideal.le_comap_sup {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K L : ideal S} :

theorem ideal.le_comap_mul {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K L : ideal S} :

theorem ideal.map_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective f) (I : ideal S) :

def ideal.gi_map_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

map and comap are adjoint, and the composition map f ∘ comap f is the identity

Equations
theorem ideal.map_sup_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective f) (I J : ideal S) :

theorem ideal.map_supr_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {ι : Sort u_1} (hf : function.surjective f) (K : ι → ideal S) :
ideal.map f (⨆ (i : ι), ideal.comap f (K i)) = supr K

theorem ideal.map_inf_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective f) (I J : ideal S) :

theorem ideal.map_infi_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {ι : Sort u_1} (hf : function.surjective f) (K : ι → ideal S) :
ideal.map f (⨅ (i : ι), ideal.comap f (K i)) = infi K

theorem ideal.mem_image_of_mem_map_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective f) {I : ideal R} {y : S} :
y ideal.map f Iy f '' I

theorem ideal.mem_map_iff_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective f) {I : ideal R} {y : S} :
y ideal.map f I ∃ (x : R), x I f x = y

theorem ideal.comap_map_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective f) (I : ideal R) :

theorem ideal.le_map_of_comap_le_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} {K : ideal S} :

def ideal.rel_iso_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

Correspondence theorem

Equations
def ideal.order_embedding_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

The map on ideals induced by a surjective map preserves inclusion.

Equations
theorem ideal.map_eq_top_or_is_maximal_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :

theorem ideal.comap_is_maximal_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K : ideal S} (hf : function.surjective f) [H : K.is_maximal] :

theorem ideal.mem_quotient_iff_mem {R : Type u} [comm_ring R] {I J : ideal R} (hIJ : I J) {x : R} :

theorem ideal.comap_bot_le_of_injective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :

def ideal.rel_iso_of_bijective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

Special case of the correspondence theorem for isomorphic rings

Equations
theorem ideal.comap_le_iff_le_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} {K : ideal S} :

theorem ideal.map.is_maximal {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :

def ideal.is_primary {R : Type u} [comm_ring R] :
ideal R → Prop

A proper ideal I is primary iff xy ∈ I implies x ∈ I or y ∈ radical I.

Equations
theorem ideal.is_primary.to_is_prime {R : Type u} [comm_ring R] (I : ideal R) :

theorem ideal.mem_radical_of_pow_mem {R : Type u} [comm_ring R] {I : ideal R} {x : R} {m : } :
x ^ m I.radicalx I.radical

theorem ideal.is_prime_radical {R : Type u} [comm_ring R] {I : ideal R} :

theorem ideal.is_primary_inf {R : Type u} [comm_ring R] {I J : ideal R} :
I.is_primaryJ.is_primaryI.radical = J.radical(I J).is_primary

def ring_hom.ker {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] :
(R →+* S)ideal R

Kernel of a ring homomorphism as an ideal of the domain.

Equations
theorem ring_hom.mem_ker {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {r : R} :
r f.ker f r = 0

An element is in the kernel if and only if it maps to zero.

theorem ring_hom.ker_eq {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

theorem ring_hom.ker_eq_comap_bot {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

theorem ring_hom.injective_iff_ker_eq_bot {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

theorem ring_hom.ker_eq_bot_iff_eq_zero {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :
f.ker = ∀ (x : R), f x = 0x = 0

theorem ring_hom.not_one_mem_ker {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [nontrivial S] (f : R →+* S) :
1 f.ker

If the target is not the zero ring, then one is not in the kernel.

@[simp]
theorem ring_hom.ker_coe_equiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R ≃+* S) :

theorem ring_hom.ker_is_prime {R : Type u} {S : Type v} [comm_ring R] [integral_domain S] (f : R →+* S) :

The kernel of a homomorphism to an integral domain is a prime ideal.

theorem ideal.map_eq_bot_iff_le_ker {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal R} (f : R →+* S) :

@[simp]
theorem ideal.mk_ker {R : Type u_1} [comm_ring R] {I : ideal R} :

theorem ideal.ker_le_comap {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {K : ideal S} (f : R →+* S) :

theorem ideal.map_Inf {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {A : set (ideal R)} {f : R →+* S} :
function.surjective f(∀ (J : ideal R), J Af.ker J)ideal.map f (Inf A) = Inf (ideal.map f '' A)

theorem ideal.map_is_prime_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective f) {I : ideal R} [H : I.is_prime] :
f.ker I(ideal.map f I).is_prime

theorem ideal.map_is_prime_of_equiv {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R ≃+* S) {I : ideal R} [I.is_prime] :

theorem ideal.map_radical_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective f) {I : ideal R} :

def ideal.quotient_map {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal R} (J : ideal S) (f : R →+* S) :

The ring hom R/f⁻¹(I) →+* S/I induced by a ring hom f : R →+* S

Equations
@[instance]
def ideal.quotient_algebra {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal S} [algebra R S] :

Equations
def ring_hom.lift_of_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (hf : function.surjective f) (g : A →+* C) :
f.ker g.kerB →+* C

lift_of_surjective f hf g hg is the unique ring homomorphism φ

  • such that φ.comp f = g (lift_of_surjective_comp),
  • where f : A →+* B is surjective (hf),
  • and g : B →+* C satisfies hg : f.ker ≤ g.ker.

See lift_of_surjective_eq for the uniqueness lemma.

   A .
   |  \
 f |   \ g
   |    \
   v     \⌟
   B ----> C
      ∃!φ
Equations
@[simp]
theorem ring_hom.lift_of_surjective_comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (hf : function.surjective f) (g : A →+* C) (hg : f.ker g.ker) (a : A) :
(f.lift_of_surjective hf g hg) (f a) = g a

@[simp]
theorem ring_hom.lift_of_surjective_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (hf : function.surjective f) (g : A →+* C) (hg : f.ker g.ker) :
(f.lift_of_surjective hf g hg).comp f = g

theorem ring_hom.eq_lift_of_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (hf : function.surjective f) (g : A →+* C) (hg : f.ker g.ker) (h : B →+* C) :
h.comp f = gh = f.lift_of_surjective hf g hg