mathlib3 documentation

ring_theory.ideal.operations

More operations on modules and ideals #

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

@[protected, instance]
def submodule.has_smul' {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] :
Equations
@[protected]
theorem ideal.smul_eq_mul {R : Type u} [comm_semiring R] (I J : ideal R) :
I J = I * J

This duplicates the global smul_eq_mul, but doesn't have to unfold anywhere near as much to apply.

def submodule.annihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (N : submodule R M) :

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

Equations
theorem submodule.mem_annihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {N : submodule R M} {r : R} :
r N.annihilator (n : M), n N r n = 0
theorem submodule.mem_annihilator_span {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (s : set M) (r : R) :
theorem submodule.mem_annihilator_span_singleton {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (g : M) (r : R) :
theorem submodule.annihilator_mono {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {N P : submodule R M} (h : N P) :
theorem submodule.annihilator_supr {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (ι : Sort w) (f : ι submodule R M) :
( (i : ι), f i).annihilator = (i : ι), (f i).annihilator
theorem submodule.smul_mem_smul {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {I : ideal R} {N : submodule R M} {r : R} {n : M} (hr : r I) (hn : n N) :
r n I N
theorem submodule.smul_le {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {I : ideal R} {N P : submodule R M} :
I N P (r : R), r I (n : M), n N r n P
theorem submodule.smul_induction_on {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {I : ideal R} {N : submodule R M} {p : M Prop} {x : M} (H : x I N) (Hb : (r : R), r I (n : M), n N p (r n)) (H1 : (x y : M), p x p y p (x + y)) :
p x
theorem submodule.smul_induction_on' {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {I : ideal R} {N : submodule R M} {x : M} (hx : x I N) {p : Π (x : M), x I N Prop} (Hb : (r : R) (hr : r I) (n : M) (hn : n N), p (r n) _) (H1 : (x : M) (hx : x I N) (y : M) (hy : y I N), p x hx p y hy p (x + y) _) :
p x hx

Dependent version of submodule.smul_induction_on.

theorem submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] {I J : ideal R} {N P : submodule R M} (hij : I J) (hnp : N P) :
I N J P
theorem submodule.smul_mono_left {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {I J : ideal R} {N : submodule R M} (h : I J) :
I N J N
theorem submodule.smul_mono_right {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {I : ideal R} {N P : submodule R M} (h : N P) :
I N I P
theorem submodule.map_le_smul_top {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I : ideal R) (f : R →ₗ[R] M) :
@[simp]
theorem submodule.annihilator_smul {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (N : submodule R M) :
@[simp]
@[simp]
@[simp]
theorem submodule.smul_bot {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I : ideal R) :
@[simp]
theorem submodule.bot_smul {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (N : submodule R M) :
@[simp]
theorem submodule.top_smul {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (N : submodule R M) :
N = N
theorem submodule.smul_sup {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] (I J : ideal R) (N : submodule R M) :
(I J) N = I N J N
@[protected]
theorem submodule.smul_assoc {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I J : ideal R) (N : submodule R M) :
(I J) N = I J N
theorem submodule.smul_inf_le {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I : ideal R) (M₁ M₂ : submodule R M) :
I (M₁ M₂) I M₁ I M₂
theorem submodule.smul_supr {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_1} {I : ideal R} {t : ι submodule R M} :
I supr t = (i : ι), I t i
theorem submodule.smul_infi_le {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_1} {I : ideal R} {t : ι submodule R M} :
I infi t (i : ι), I t i
theorem submodule.span_smul_span {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid 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.ideal_span_singleton_smul {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (r : R) (N : submodule R M) :
ideal.span {r} N = r N
theorem submodule.mem_of_span_top_of_smul_mem {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (M' : submodule R M) (s : set R) (hs : ideal.span s = ) (x : M) (H : (r : s), r x M') :
x M'
theorem submodule.mem_of_span_eq_top_of_smul_pow_mem {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (M' : submodule R M) (s : set R) (hs : ideal.span s = ) (x : M) (H : (r : s), (n : ), r ^ n x M') :
x M'

Given s, a generating set of R, to check that an x : M falls in a submodule M' of x, we only need to show that r ^ n • x ∈ M' for some n for each r : s.

theorem submodule.map_smul'' {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I : ideal R) (N : submodule R M) {M' : Type w} [add_comm_monoid M'] [module R M'] (f : M →ₗ[R] M') :
theorem submodule.mem_smul_span {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {I : ideal R} {s : set M} {x : M} :
x I submodule.span R s x submodule.span R ( (a : R) (H : a I) (b : M) (H : b s), {a b})
theorem submodule.mem_ideal_smul_span_iff_exists_sum {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I : ideal R) {ι : Type u_1} (f : ι M) (x : M) :
x I submodule.span R (set.range f) (a : ι →₀ R) (ha : (i : ι), a i I), a.sum (λ (i : ι) (c : R), c f i) = x

If x is an I-multiple of the submodule spanned by f '' s, then we can write x as an I-linear combination of the elements of f '' s.

theorem submodule.mem_ideal_smul_span_iff_exists_sum' {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I : ideal R) {ι : Type u_1} (s : set ι) (f : ι M) (x : M) :
x I submodule.span R (f '' s) (a : s →₀ R) (ha : (i : s), a i I), a.sum (λ (i : s) (c : R), c f i) = x
theorem submodule.mem_smul_top_iff {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I : ideal R) (N : submodule R M) (x : N) :
x I x I N
@[simp]
theorem submodule.smul_comap_le_comap_smul {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {M' : Type w} [add_comm_monoid M'] [module R M'] (f : M →ₗ[R] M') (S : submodule R M') (I : ideal R) :
def submodule.colon {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (N P : submodule R M) :

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

Equations
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 P r 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} (hn : N₁ N₂) (hp : 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)
@[simp]
theorem submodule.mem_colon_singleton {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N : submodule R M} {x : M} {r : R} :
r N.colon (submodule.span R {x}) r x N
@[simp]
theorem ideal.mem_colon_singleton {R : Type u} [comm_ring R] {I : ideal R} {x r : R} :
@[simp]
theorem ideal.add_eq_sup {R : Type u} [semiring R] {I J : ideal R} :
I + J = I J
@[simp]
theorem ideal.zero_eq_bot {R : Type u} [semiring R] :
0 =
@[simp]
theorem ideal.sum_eq_sup {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι ideal R) :
s.sum f = s.sup f
@[protected, instance]
def ideal.has_mul {R : Type u} [comm_semiring R] :
Equations
@[simp]
theorem ideal.one_eq_top {R : Type u} [comm_semiring R] :
1 =
theorem ideal.mul_mem_mul {R : Type u} [comm_semiring R] {I J : ideal R} {r s : R} (hr : r I) (hs : s J) :
r * s I * J
theorem ideal.mul_mem_mul_rev {R : Type u} [comm_semiring R] {I J : ideal R} {r s : R} (hr : r I) (hs : s J) :
s * r I * J
theorem ideal.pow_mem_pow {R : Type u} [comm_semiring R] {I : ideal R} {x : R} (hx : x I) (n : ) :
x ^ n I ^ n
theorem ideal.prod_mem_prod {R : Type u} [comm_semiring R] {ι : Type u_1} {s : finset ι} {I : ι ideal R} {x : ι R} :
( (i : ι), i s x i I i) s.prod (λ (i : ι), x i) s.prod (λ (i : ι), I i)
theorem ideal.mul_le {R : Type u} [comm_semiring R] {I J K : ideal R} :
I * J K (r : R), r I (s : R), s J r * s K
theorem ideal.mul_le_left {R : Type u} [comm_semiring R] {I J : ideal R} :
I * J J
theorem ideal.mul_le_right {R : Type u} [comm_semiring R] {I J : ideal R} :
I * J I
@[simp]
theorem ideal.sup_mul_right_self {R : Type u} [comm_semiring R] {I J : ideal R} :
I I * J = I
@[simp]
theorem ideal.sup_mul_left_self {R : Type u} [comm_semiring R] {I J : ideal R} :
I J * I = I
@[simp]
theorem ideal.mul_right_self_sup {R : Type u} [comm_semiring R] {I J : ideal R} :
I * J I = I
@[simp]
theorem ideal.mul_left_self_sup {R : Type u} [comm_semiring R] {I J : ideal R} :
J * I I = I
@[protected]
theorem ideal.mul_comm {R : Type u} [comm_semiring R] (I J : ideal R) :
I * J = J * I
@[protected]
theorem ideal.mul_assoc {R : Type u} [comm_semiring R] (I J K : ideal R) :
I * J * K = I * (J * K)
theorem ideal.span_mul_span {R : Type u} [comm_semiring 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_semiring R] (S T : set R) :
theorem ideal.span_singleton_pow {R : Type u} [comm_semiring R] (s : R) (n : ) :
ideal.span {s} ^ n = ideal.span {s ^ n}
theorem ideal.mem_mul_span_singleton {R : Type u} [comm_semiring R] {x y : R} {I : ideal R} :
x I * ideal.span {y} (z : R) (H : z I), z * y = x
theorem ideal.mem_span_singleton_mul {R : Type u} [comm_semiring R] {x y : R} {I : ideal R} :
x ideal.span {y} * I (z : R) (H : z I), y * z = x
theorem ideal.le_span_singleton_mul_iff {R : Type u} [comm_semiring R] {x : R} {I J : ideal R} :
I ideal.span {x} * J (zI : R), zI I ( (zJ : R) (H : zJ J), x * zJ = zI)
theorem ideal.span_singleton_mul_le_iff {R : Type u} [comm_semiring R] {x : R} {I J : ideal R} :
ideal.span {x} * I J (z : R), z I x * z J
theorem ideal.span_singleton_mul_le_span_singleton_mul {R : Type u} [comm_semiring R] {x y : R} {I J : ideal R} :
ideal.span {x} * I ideal.span {y} * J (zI : R), zI I ( (zJ : R) (H : zJ J), x * zI = y * zJ)
theorem ideal.span_singleton_mul_right_mono {R : Type u} [comm_semiring R] {I J : ideal R} [is_domain R] {x : R} (hx : x 0) :
ideal.span {x} * I ideal.span {x} * J I J
theorem ideal.span_singleton_mul_left_mono {R : Type u} [comm_semiring R] {I J : ideal R} [is_domain R] {x : R} (hx : x 0) :
I * ideal.span {x} J * ideal.span {x} I J
theorem ideal.span_singleton_mul_right_inj {R : Type u} [comm_semiring R] {I J : ideal R} [is_domain R] {x : R} (hx : x 0) :
ideal.span {x} * I = ideal.span {x} * J I = J
theorem ideal.span_singleton_mul_left_inj {R : Type u} [comm_semiring R] {I J : ideal R} [is_domain R] {x : R} (hx : x 0) :
I * ideal.span {x} = J * ideal.span {x} I = J
theorem ideal.span_singleton_mul_left_injective {R : Type u} [comm_semiring R] [is_domain R] {x : R} (hx : x 0) :
function.injective (λ (I : ideal R), I * ideal.span {x})
theorem ideal.eq_span_singleton_mul {R : Type u} [comm_semiring R] {x : R} (I J : ideal R) :
I = ideal.span {x} * J ( (zI : R), zI I ( (zJ : R) (H : zJ J), x * zJ = zI)) (z : R), z J x * z I
theorem ideal.span_singleton_mul_eq_span_singleton_mul {R : Type u} [comm_semiring R] {x y : R} (I J : ideal R) :
ideal.span {x} * I = ideal.span {y} * J ( (zI : R), zI I ( (zJ : R) (H : zJ J), x * zI = y * zJ)) (zJ : R), zJ J ( (zI : R) (H : zI I), x * zI = y * zJ)
theorem ideal.prod_span {R : Type u} [comm_semiring R] {ι : Type u_1} (s : finset ι) (I : ι set R) :
s.prod (λ (i : ι), ideal.span (I i)) = ideal.span (s.prod (λ (i : ι), I i))
theorem ideal.prod_span_singleton {R : Type u} [comm_semiring R] {ι : Type u_1} (s : finset ι) (I : ι R) :
s.prod (λ (i : ι), ideal.span {I i}) = ideal.span {s.prod (λ (i : ι), I i)}
@[simp]
theorem ideal.multiset_prod_span_singleton {R : Type u} [comm_semiring R] (m : multiset R) :
(multiset.map (λ (x : R), ideal.span {x}) m).prod = ideal.span {m.prod}
theorem ideal.finset_inf_span_singleton {R : Type u} [comm_semiring R] {ι : Type u_1} (s : finset ι) (I : ι R) (hI : s.pairwise (is_coprime on I)) :
s.inf (λ (i : ι), ideal.span {I i}) = ideal.span {s.prod (λ (i : ι), I i)}
theorem ideal.infi_span_singleton {R : Type u} [comm_semiring R] {ι : Type u_1} [fintype ι] (I : ι R) (hI : (i j : ι), i j is_coprime (I i) (I j)) :
( (i : ι), ideal.span {I i}) = ideal.span {finset.univ.prod (λ (i : ι), I i)}
theorem ideal.mul_le_inf {R : Type u} [comm_semiring R] {I J : ideal R} :
I * J I J
theorem ideal.prod_le_inf {R : Type u} {ι : Type u_1} [comm_semiring R] {s : finset ι} {f : ι ideal R} :
s.prod f s.inf f
theorem ideal.mul_eq_inf_of_coprime {R : Type u} [comm_semiring R] {I J : ideal R} (h : I J = ) :
I * J = I J
theorem ideal.sup_mul_eq_of_coprime_left {R : Type u} [comm_semiring R] {I J K : ideal R} (h : I J = ) :
I J * K = I K
theorem ideal.sup_mul_eq_of_coprime_right {R : Type u} [comm_semiring R] {I J K : ideal R} (h : I K = ) :
I J * K = I J
theorem ideal.mul_sup_eq_of_coprime_left {R : Type u} [comm_semiring R] {I J K : ideal R} (h : I J = ) :
I * K J = K J
theorem ideal.mul_sup_eq_of_coprime_right {R : Type u} [comm_semiring R] {I J K : ideal R} (h : K J = ) :
I * K J = I J
theorem ideal.sup_prod_eq_top {R : Type u} {ι : Type u_1} [comm_semiring R] {I : ideal R} {s : finset ι} {J : ι ideal R} (h : (i : ι), i s I J i = ) :
I s.prod (λ (i : ι), J i) =
theorem ideal.sup_infi_eq_top {R : Type u} {ι : Type u_1} [comm_semiring R] {I : ideal R} {s : finset ι} {J : ι ideal R} (h : (i : ι), i s I J i = ) :
(I (i : ι) (H : i s), J i) =
theorem ideal.prod_sup_eq_top {R : Type u} {ι : Type u_1} [comm_semiring R] {I : ideal R} {s : finset ι} {J : ι ideal R} (h : (i : ι), i s J i I = ) :
s.prod (λ (i : ι), J i) I =
theorem ideal.infi_sup_eq_top {R : Type u} {ι : Type u_1} [comm_semiring R] {I : ideal R} {s : finset ι} {J : ι ideal R} (h : (i : ι), i s J i I = ) :
( (i : ι) (H : i s), J i) I =
theorem ideal.sup_pow_eq_top {R : Type u} [comm_semiring R] {I J : ideal R} {n : } (h : I J = ) :
I J ^ n =
theorem ideal.pow_sup_eq_top {R : Type u} [comm_semiring R] {I J : ideal R} {n : } (h : I J = ) :
I ^ n J =
theorem ideal.pow_sup_pow_eq_top {R : Type u} [comm_semiring R] {I J : ideal R} {m n : } (h : I J = ) :
I ^ m J ^ n =
@[simp]
theorem ideal.mul_bot {R : Type u} [comm_semiring R] (I : ideal R) :
@[simp]
theorem ideal.bot_mul {R : Type u} [comm_semiring R] (I : ideal R) :
@[simp]
theorem ideal.mul_top {R : Type u} [comm_semiring R] (I : ideal R) :
I * = I
@[simp]
theorem ideal.top_mul {R : Type u} [comm_semiring R] (I : ideal R) :
* I = I
theorem ideal.mul_mono {R : Type u} [comm_semiring R] {I J K L : ideal R} (hik : I K) (hjl : J L) :
I * J K * L
theorem ideal.mul_mono_left {R : Type u} [comm_semiring R] {I J K : ideal R} (h : I J) :
I * K J * K
theorem ideal.mul_mono_right {R : Type u} [comm_semiring R] {I J K : ideal R} (h : J K) :
I * J I * K
theorem ideal.mul_sup {R : Type u} [comm_semiring R] (I J K : ideal R) :
I * (J K) = I * J I * K
theorem ideal.sup_mul {R : Type u} [comm_semiring R] (I J K : ideal R) :
(I J) * K = I * K J * K
theorem ideal.pow_le_pow {R : Type u} [comm_semiring R] {I : ideal R} {m n : } (h : m n) :
I ^ n I ^ m
theorem ideal.pow_le_self {R : Type u} [comm_semiring R] {I : ideal R} {n : } (hn : n 0) :
I ^ n I
theorem ideal.pow_mono {R : Type u} [comm_semiring R] {I J : ideal R} (e : I J) (n : ) :
I ^ n J ^ n
theorem ideal.mul_eq_bot {R : Type u_1} [comm_semiring R] [no_zero_divisors R] {I J : ideal R} :
I * J = I = J =
@[protected, instance]
theorem ideal.prod_eq_bot {R : Type u_1} [comm_ring R] [is_domain R] {s : multiset (ideal R)} :
s.prod = (I : ideal R) (H : I s), I =

A product of ideals in an integral domain is zero if and only if one of the terms is zero.

theorem ideal.span_pair_mul_span_pair {R : Type u} [comm_semiring R] (w x y z : R) :
ideal.span {w, x} * ideal.span {y, z} = ideal.span {w * y, w * z, x * y, x * z}
def ideal.radical {R : Type u} [comm_semiring R] (I : ideal R) :

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

Equations
def ideal.is_radical {R : Type u} [comm_semiring R] (I : ideal R) :
Prop

An ideal is radical if it contains its radical.

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

An ideal is radical iff it is equal to its radical.

theorem ideal.is_radical.radical {R : Type u} [comm_semiring R] {I : ideal R} :

Alias of the reverse direction of ideal.radical_eq_iff.

theorem ideal.radical_mono {R : Type u} [comm_semiring R] {I J : ideal R} (H : I J) :
@[simp]
theorem ideal.radical_idem {R : Type u} [comm_semiring R] (I : ideal R) :
theorem ideal.is_radical.radical_le_iff {R : Type u} [comm_semiring R] {I J : ideal R} (hJ : J.is_radical) :
I.radical J I J
theorem ideal.radical_eq_top {R : Type u} [comm_semiring R] {I : ideal R} :
theorem ideal.is_prime.is_radical {R : Type u} [comm_semiring R] {I : ideal R} (H : I.is_prime) :
theorem ideal.is_prime.radical {R : Type u} [comm_semiring R] {I : ideal R} (H : I.is_prime) :
theorem ideal.radical_sup {R : Type u} [comm_semiring R] (I J : ideal R) :
theorem ideal.radical_inf {R : Type u} [comm_semiring R] (I J : ideal R) :
theorem ideal.radical_mul {R : Type u} [comm_semiring R] (I J : ideal R) :
theorem ideal.is_prime.radical_le_iff {R : Type u} [comm_semiring R] {I J : ideal R} (hJ : J.is_prime) :
I.radical J I J
theorem ideal.radical_eq_Inf {R : Type u} [comm_semiring R] (I : ideal R) :
theorem ideal.top_pow (R : Type u) [comm_semiring R] (n : ) :
theorem ideal.radical_pow {R : Type u} [comm_semiring R] (I : ideal R) (n : ) (H : n > 0) :
(I ^ n).radical = I.radical
theorem ideal.is_prime.mul_le {R : Type u} [comm_semiring R] {I J P : ideal R} (hp : P.is_prime) :
I * J P I P J P
theorem ideal.is_prime.inf_le {R : Type u} [comm_semiring R] {I J P : ideal R} (hp : P.is_prime) :
I J P I P J P
theorem ideal.is_prime.multiset_prod_le {R : Type u} [comm_semiring R] {s : multiset (ideal R)} {P : ideal R} (hp : P.is_prime) (hne : s 0) :
s.prod P (I : ideal R) (H : I s), I P
theorem ideal.is_prime.multiset_prod_map_le {R : Type u} {ι : Type u_1} [comm_semiring R] {s : multiset ι} (f : ι ideal R) {P : ideal R} (hp : P.is_prime) (hne : s 0) :
(multiset.map f s).prod P (i : ι) (H : i s), f i P
theorem ideal.is_prime.prod_le {R : Type u} {ι : Type u_1} [comm_semiring R] {s : finset ι} {f : ι ideal R} {P : ideal R} (hp : P.is_prime) (hne : s.nonempty) :
s.prod f P (i : ι) (H : i s), f i P
theorem ideal.is_prime.inf_le' {R : Type u} {ι : Type u_1} [comm_semiring R] {s : finset ι} {f : ι ideal R} {P : ideal R} (hp : P.is_prime) (hsne : s.nonempty) :
s.inf f P (i : ι) (H : i s), f i P
theorem ideal.subset_union {R : Type u} [ring R] {I J K : ideal R} :
I J K I J I K
theorem ideal.subset_union_prime' {ι : Type u_1} {R : Type u} [comm_ring R] {s : finset ι} {f : ι ideal R} {a b : ι} (hp : (i : ι), i s (f i).is_prime) {I : ideal R} :
(I (f a) (f b) (i : ι) (H : i s), (f i)) I f a I f b (i : ι) (H : i s), I f i
theorem ideal.subset_union_prime {ι : Type u_1} {R : Type u} [comm_ring R] {s : finset ι} {f : ι ideal R} (a b : ι) (hp : (i : ι), i s i a i b (f i).is_prime) {I : ideal R} :
(I (i : ι) (H : i s), (f i)) (i : ι) (H : i s), I f i

Prime avoidance. Atiyah-Macdonald 1.11, Eisenbud 3.3, Stacks 00DS, Matsumura Ex.1.6.

theorem ideal.le_of_dvd {R : Type u} [comm_semiring R] {I J : ideal R} :
I J J I

If I divides J, then I contains J.

In a Dedekind domain, to divide and contain are equivalent, see ideal.dvd_iff_le.

theorem ideal.is_unit_iff {R : Type u} [comm_semiring R] {I : ideal R} :
@[protected, instance]
Equations
def ideal.map {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (I : ideal R) :

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} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (I : ideal S) :

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

Equations
Instances for ideal.comap
theorem ideal.map_mono {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {I J : ideal R} (h : I J) :
theorem ideal.mem_map_of_mem {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {I : ideal R} {x : R} (h : x I) :
theorem ideal.apply_coe_mem_map {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (I : ideal R) (x : I) :
theorem ideal.map_le_iff_le_comap {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {I : ideal R} {K : ideal S} :
@[simp]
theorem ideal.mem_comap {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {K : ideal S} {x : R} :
theorem ideal.comap_mono {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {K L : ideal S} (h : K L) :
theorem ideal.comap_ne_top {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {K : ideal S} (hK : K ) :
theorem ideal.map_le_comap_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {G : Type u_2} [rcg : ring_hom_class G S R] (g : G) (I : ideal R) (hf : set.left_inv_on g f I) :
theorem ideal.comap_le_map_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {G : Type u_2} [rcg : ring_hom_class G S R] (g : G) (I : ideal S) (hf : set.left_inv_on g f (f ⁻¹' I)) :
theorem ideal.map_le_comap_of_inverse {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {G : Type u_2} [rcg : ring_hom_class G S R] (g : G) (I : ideal R) (h : function.left_inverse g f) :

The ideal version of set.image_subset_preimage_of_inverse.

theorem ideal.comap_le_map_of_inverse {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {G : Type u_2} [rcg : ring_hom_class G S R] (g : G) (I : ideal S) (h : function.left_inverse g f) :

The ideal version of set.preimage_subset_image_of_inverse.

@[protected, instance]
def ideal.is_prime.comap {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {K : ideal S} [hK : K.is_prime] :
theorem ideal.map_top {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) :
theorem ideal.gc_map_comap {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) :
@[simp]
theorem ideal.comap_id {R : Type u} [semiring R] (I : ideal R) :
@[simp]
theorem ideal.map_id {R : Type u} [semiring R] (I : ideal R) :
theorem ideal.comap_comap {R : Type u} {S : Type v} [semiring R] [semiring S] {T : Type u_1} [semiring T] {I : ideal T} (f : R →+* S) (g : S →+* T) :
theorem ideal.map_map {R : Type u} {S : Type v} [semiring R] [semiring S] {T : Type u_1} [semiring T] {I : ideal R} (f : R →+* S) (g : S →+* T) :
theorem ideal.map_span {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (s : set R) :
theorem ideal.map_le_of_le_comap {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {I : ideal R} {K : ideal S} :
theorem ideal.le_comap_of_map_le {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {I : ideal R} {K : ideal S} :
theorem ideal.le_comap_map {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {I : ideal R} :
theorem ideal.map_comap_le {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {K : ideal S} :
@[simp]
theorem ideal.comap_top {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} :
@[simp]
theorem ideal.comap_eq_top_iff {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} {I : ideal S} :
@[simp]
theorem ideal.map_bot {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] {f : F} :
@[simp]
theorem ideal.map_comap_map {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (I : ideal R) :
@[simp]
theorem ideal.comap_map_comap {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (K : ideal S) :
theorem ideal.map_sup {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (I J : ideal R) :
theorem ideal.comap_inf {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (K L : ideal S) :
theorem ideal.map_supr {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {ι : Sort u_3} (K : ι ideal R) :
ideal.map f (supr K) = (i : ι), ideal.map f (K i)
theorem ideal.comap_infi {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {ι : Sort u_3} (K : ι ideal S) :
ideal.comap f (infi K) = (i : ι), ideal.comap f (K i)
theorem ideal.map_Sup {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (s : set (ideal R)) :
ideal.map f (has_Sup.Sup s) = (I : ideal R) (H : I s), ideal.map f I
theorem ideal.comap_Inf {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (s : set (ideal S)) :
ideal.comap f (has_Inf.Inf s) = (I : ideal S) (H : I s), ideal.comap f I
theorem ideal.comap_Inf' {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (s : set (ideal S)) :
ideal.comap f (has_Inf.Inf s) = (I : ideal R) (H : I ideal.comap f '' s), I
theorem ideal.comap_is_prime {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (K : ideal S) [H : K.is_prime] :
theorem ideal.map_inf_le {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {I J : ideal R} :
theorem ideal.le_comap_sup {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {K L : ideal S} :
@[simp]
theorem ideal.smul_top_eq_map {R : Type u_1} {S : Type u_2} [comm_semiring R] [comm_semiring S] [algebra R S] (I : ideal R) :
@[simp]
theorem ideal.coe_restrict_scalars {R : Type u_1} {S : Type u_2} [comm_semiring R] [semiring S] [algebra R S] (I : ideal S) :
@[simp]

The smallest S-submodule that contains all x ∈ I * y ∈ J is also the smallest R-submodule that does so.

theorem ideal.map_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.surjective f) (I : ideal S) :
def ideal.gi_map_comap {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.surjective f) :

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

Equations
theorem ideal.map_surjective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.surjective f) :
theorem ideal.comap_injective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.surjective f) :
theorem ideal.map_sup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.surjective f) (I J : ideal S) :
theorem ideal.map_supr_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {ι : Sort u_3} (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} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.surjective f) (I J : ideal S) :
theorem ideal.map_infi_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {ι : Sort u_3} (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} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.surjective f) {I : ideal R} {y : S} (H : y ideal.map f I) :
theorem ideal.mem_map_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.surjective f) {I : ideal R} {y : S} :
y ideal.map f I (x : R), x I f x = y
theorem ideal.le_map_of_comap_le_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {I : ideal R} {K : ideal S} (hf : function.surjective f) :
theorem ideal.comap_bot_le_of_injective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) {I : ideal R} (hf : function.injective f) :
theorem ideal.comap_bot_of_injective {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rc : ring_hom_class F R S] (f : F) (hf : function.injective f) :
theorem ideal.comap_map_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.surjective f) (I : ideal R) :
def ideal.rel_iso_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.surjective f) :

Correspondence theorem

Equations
def ideal.order_embedding_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.surjective f) :

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} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.surjective f) {I : ideal R} (H : I.is_maximal) :
theorem ideal.comap_is_maximal_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.surjective f) {K : ideal S} [H : K.is_maximal] :
theorem ideal.comap_le_comap_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.surjective f) (I J : ideal S) :
@[simp]
theorem ideal.map_of_equiv {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (f : R ≃+* S) :

If f : R ≃+* S is a ring isomorphism and I : ideal R, then map f (map f.symm) = I.

@[simp]
theorem ideal.comap_of_equiv {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (f : R ≃+* S) :

If f : R ≃+* S is a ring isomorphism and I : ideal R, then comap f.symm (comap f) = I.

theorem ideal.map_comap_of_equiv {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (f : R ≃+* S) :

If f : R ≃+* S is a ring isomorphism and I : ideal R, then map f I = comap f.symm I.

def ideal.rel_iso_of_bijective {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.bijective f) :

Special case of the correspondence theorem for isomorphic rings

Equations
theorem ideal.comap_le_iff_le_map {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.bijective f) {I : ideal R} {K : ideal S} :
theorem ideal.map.is_maximal {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [ring_hom_class F R S] (f : F) (hf : function.bijective f) {I : ideal R} (H : I.is_maximal) :
theorem ideal.map_mul {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) (I J : ideal R) :
ideal.map f (I * J) = ideal.map f I * ideal.map f J
def ideal.map_hom {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) :

The pushforward ideal.map as a monoid-with-zero homomorphism.

Equations
@[simp]
theorem ideal.map_hom_apply {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) (I : ideal R) :
@[protected]
theorem ideal.map_pow {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) (I : ideal R) (n : ) :
ideal.map f (I ^ n) = ideal.map f I ^ n
theorem ideal.comap_radical {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) (K : ideal S) :
theorem ideal.is_radical.comap {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) {K : ideal S} (hK : K.is_radical) :
theorem ideal.map_radical_le {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) {I : ideal R} :
theorem ideal.le_comap_mul {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) {K L : ideal S} :
theorem ideal.le_comap_pow {R : Type u} {S : Type v} {F : Type u_1} [comm_ring R] [comm_ring S] [rc : ring_hom_class F R S] (f : F) {K : ideal S} (n : ) :
ideal.comap f K ^ n ideal.comap f (K ^ n)
def ideal.is_primary {R : Type u} [comm_semiring R] (I : ideal R) :
Prop

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

Equations
theorem ideal.is_prime.is_primary {R : Type u} [comm_semiring R] {I : ideal R} (hi : I.is_prime) :
theorem ideal.mem_radical_of_pow_mem {R : Type u} [comm_semiring R] {I : ideal R} {x : R} {m : } (hx : x ^ m I.radical) :
theorem ideal.is_prime_radical {R : Type u} [comm_semiring R] {I : ideal R} (hi : I.is_primary) :
theorem ideal.is_primary_inf {R : Type u} [comm_semiring R] {I J : ideal R} (hi : I.is_primary) (hj : J.is_primary) (hij : I.radical = J.radical) :
noncomputable def ideal.finsupp_total (ι : Type u_1) (M : Type u_2) [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] (I : ideal R) (v : ι M) :

A variant of finsupp.total that takes in vectors valued in I.

Equations
theorem ideal.finsupp_total_apply {ι : Type u_1} {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] (I : ideal R) {v : ι M} (f : ι →₀ I) :
(ideal.finsupp_total ι M I v) f = f.sum (λ (i : ι) (x : I), x v i)
theorem ideal.finsupp_total_apply_eq_of_fintype {ι : Type u_1} {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] (I : ideal R) {v : ι M} [fintype ι] (f : ι →₀ I) :
(ideal.finsupp_total ι M I v) f = finset.univ.sum (λ (i : ι), (f i) v i)
theorem ideal.range_finsupp_total {ι : Type u_1} {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] (I : ideal R) {v : ι M} :
noncomputable def ideal.basis_span_singleton {ι : Type u_1} {R : Type u_2} {S : Type u_3} [comm_semiring R] [comm_ring S] [is_domain S] [algebra R S] (b : basis ι R S) {x : S} (hx : x 0) :
basis ι R (ideal.span {x})

A basis on S gives a basis on ideal.span {x}, by multiplying everything by x.

Equations
@[simp]
theorem ideal.basis_span_singleton_apply {ι : Type u_1} {R : Type u_2} {S : Type u_3} [comm_semiring R] [comm_ring S] [is_domain S] [algebra R S] (b : basis ι R S) {x : S} (hx : x 0) (i : ι) :
@[simp]
theorem ideal.constr_basis_span_singleton {ι : Type u_1} {R : Type u_2} {S : Type u_3} [comm_semiring R] [comm_ring S] [is_domain S] [algebra R S] {N : Type u_4} [semiring N] [module N S] [smul_comm_class R N S] (b : basis ι R S) {x : S} (hx : x 0) :
theorem associates.mk_ne_zero' {R : Type u_1} [comm_semiring R] {r : R} :
theorem basis.mem_ideal_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} [comm_ring R] [comm_ring S] [algebra R S] {I : ideal S} (b : basis ι R I) {x : S} :
x I (c : ι →₀ R), x = c.sum (λ (i : ι) (x : R), x (b i))

If I : ideal S has a basis over R, x ∈ I iff it is a linear combination of basis vectors.

theorem basis.mem_ideal_iff' {ι : Type u_1} {R : Type u_2} {S : Type u_3} [fintype ι] [comm_ring R] [comm_ring S] [algebra R S] {I : ideal S} (b : basis ι R I) {x : S} :
x I (c : ι R), x = finset.univ.sum (λ (i : ι), c i (b i))

If I : ideal S has a finite basis over R, x ∈ I iff it is a linear combination of basis vectors.

def ring_hom.ker {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rcf : ring_hom_class F R S] (f : F) :

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

Equations
theorem ring_hom.mem_ker {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rcf : ring_hom_class F R S] (f : F) {r : R} :

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} {F : Type u_1} [semiring R] [semiring S] [rcf : ring_hom_class F R S] (f : F) :
theorem ring_hom.ker_eq_comap_bot {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rcf : ring_hom_class F R S] (f : F) :
theorem ring_hom.comap_ker {R : Type u} {S : Type v} {T : Type w} [semiring R] [semiring S] [semiring T] (f : S →+* R) (g : T →+* S) :
theorem ring_hom.not_one_mem_ker {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rcf : ring_hom_class F R S] [nontrivial S] (f : F) :

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

theorem ring_hom.ker_ne_top {R : Type u} {S : Type v} {F : Type u_1} [semiring R] [semiring S] [rcf : ring_hom_class F R S] [nontrivial S] (f : F) :
theorem ring_hom.injective_iff_ker_eq_bot {R : Type u} {S : Type v} {F : Type u_1} [ring R] [semiring S] [rc : ring_hom_class F R S] (f : F) :
theorem ring_hom.ker_eq_bot_iff_eq_zero {R : Type u} {S : Type v} {F : Type u_1} [ring R] [semiring S] [rc : ring_hom_class F R S] (f : F) :
ring_hom.ker f = (x : R), f x = 0 x = 0
@[simp]
theorem ring_hom.ker_coe_equiv {R : Type u} {S : Type v} [ring R] [semiring S] (f : R ≃+* S) :
@[simp]
theorem ring_hom.ker_equiv {R : Type u} {S : Type v} [ring R] [semiring S] {F' : Type u_1} [ring_equiv_class F' R S] (f : F') :
theorem ring_hom.sub_mem_ker_iff {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [rc : ring_hom_class F R S] (f : F) {x y : R} :
x - y ring_hom.ker f f x = f y
theorem ring_hom.ker_is_prime {R : Type u} {S : Type v} {F : Type u_1} [ring R] [ring S] [is_domain S] [ring_hom_class F R S] (f : F) :

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

theorem ring_hom.ker_is_maximal_of_surjective {R : Type u_1} {K : Type u_2} {F : Type u_3} [ring R] [field K] [ring_hom_class F R K] (f : F) (hf : function.surjective f) :

The kernel of a homomorphism to a field is a maximal ideal.

theorem ideal.map_eq_bot_iff_le_ker {R : Type u_1} {S : Type u_2} {F : Type u_3} [semiring R] [semiring S] [rc : ring_hom_class F R S] {I : ideal R} (f : F) :
theorem ideal.ker_le_comap {R : Type u_1} {S : Type u_2} {F : Type u_3} [semiring R] [semiring S] [rc : ring_hom_class F R S] {K : ideal S} (f : F) :
theorem ideal.map_Inf {R : Type u_1} {S : Type u_2} {F : Type u_3} [ring R] [ring S] [rc : ring_hom_class F R S] {A : set (ideal R)} {f : F} (hf : function.surjective f) :
theorem ideal.map_is_prime_of_surjective {R : Type u_1} {S : Type u_2} {F : Type u_3} [ring R] [ring S] [rc : ring_hom_class F R S] {f : F} (hf : function.surjective f) {I : ideal R} [H : I.is_prime] (hk : ring_hom.ker f I) :
theorem ideal.map_eq_bot_iff_of_injective {R : Type u_1} {S : Type u_2} {F : Type u_3} [ring R] [ring S] [rc : ring_hom_class F R S] {I : ideal R} {f : F} (hf : function.injective f) :
theorem ideal.map_is_prime_of_equiv {R : Type u_1} {S : Type u_2} [ring R] [ring S] {F' : Type u_3} [ring_equiv_class F' R S] (f : F') {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} (h : ring_hom.ker f I) :
@[protected, instance]
Equations
def ring_hom.lift_of_right_inverse_aux {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B A) (hf : function.right_inverse f_inv f) (g : A →+* C) (hg : ring_hom.ker f ring_hom.ker g) :
B →+* C

Auxiliary definition used to define lift_of_right_inverse

Equations
@[simp]
theorem ring_hom.lift_of_right_inverse_aux_comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B A) (hf : function.right_inverse f_inv f) (g : A →+* C) (hg : ring_hom.ker f ring_hom.ker g) (a : A) :
(f.lift_of_right_inverse_aux f_inv hf g hg) (f a) = g a
def ring_hom.lift_of_right_inverse {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B A) (hf : function.right_inverse f_inv f) :

lift_of_right_inverse f hf g hg is the unique ring homomorphism φ

See ring_hom.eq_lift_of_right_inverse for the uniqueness lemma.

   A .
   |  \
 f |   \ g
   |    \
   v     \⌟
   B ----> C
      ∃!φ
Equations
@[simp, reducible]
noncomputable def ring_hom.lift_of_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (hf : function.surjective f) :

A non-computable version of ring_hom.lift_of_right_inverse for when no computable right inverse is available, that uses function.surj_inv.

theorem ring_hom.lift_of_right_inverse_comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B A) (hf : function.right_inverse f_inv f) (g : {g // ring_hom.ker f ring_hom.ker g}) (x : A) :
((f.lift_of_right_inverse f_inv hf) g) (f x) = g x
theorem ring_hom.lift_of_right_inverse_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B A) (hf : function.right_inverse f_inv f) (g : {g // ring_hom.ker f ring_hom.ker g}) :
((f.lift_of_right_inverse f_inv hf) g).comp f = g
theorem ring_hom.eq_lift_of_right_inverse {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B A) (hf : function.right_inverse f_inv f) (g : A →+* C) (hg : ring_hom.ker f ring_hom.ker g) (h : B →+* C) (hh : h.comp f = g) :
h = (f.lift_of_right_inverse f_inv hf) g, hg⟩