mathlib documentation

ring_theory.ideal.operations

More operations on modules and ideals #

source
@[protected, instance]
def submodule.has_smul' {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] :
has_smul (ideal R) (submodule R M)
Equations
source
@[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.

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

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

Equations
source
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
source
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 ≤ submodule.comap (r • linear_map.id) ⊥
source
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) :
r ∈ (submodule.span R s).annihilator ↔ ∀ (n : ↥s), r • ↑n = 0
source
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) :
r ∈ (submodule.span R {g}).annihilator ↔ r • g = 0
source
theorem submodule.annihilator_bot {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] :
⊥.annihilator = ⊤
source
theorem submodule.annihilator_eq_top_iff {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {N : submodule R M} :
N.annihilator = ⊤ ↔ N = ⊥
source
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) :
P.annihilator ≤ N.annihilator
source
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
source
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
source
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
source
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
source
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.

source
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
source
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
source
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
source
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
source
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
source
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) :
submodule.map f I ≤ I • ⊤
source
@[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) :
N.annihilator • N = ⊥
source
@[simp]
theorem submodule.annihilator_mul {R : Type u} [comm_semiring R] (I : ideal R) :
submodule.annihilator I * I = ⊥
source
@[simp]
theorem submodule.mul_annihilator {R : Type u} [comm_semiring R] (I : ideal R) :
I * submodule.annihilator I = ⊥
source
@[simp]
theorem submodule.smul_bot {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (I : ideal R) :
I • ⊥ = ⊥
source
@[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) :
⊥ • N = ⊥
source
@[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
source
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
source
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
source
@[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
source
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₂
source
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
source
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
source
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})
source
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
source
theorem submodule.span_smul_eq {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (r : R) (s : set M) :
submodule.span R (r • s) = r • submodule.span R s
source
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'
source
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.

source
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') :
submodule.map f (I • N) = I • submodule.map f N
source
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})
source
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.

source
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
source
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
source
@[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) :
I • submodule.comap f S ≤ submodule.comap f (I • S)
source
def submodule.colon {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (N P : submodule R M) :
ideal R

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

Equations
source
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
source
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 ≤ submodule.comap (r • linear_map.id) N
source
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₁
source
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)
source
@[simp]
theorem ideal.add_eq_sup {R : Type u} [semiring R] {I J : ideal R} :
I + J = I ⊔ J
source
@[simp]
theorem ideal.zero_eq_bot {R : Type u} [semiring R] :
0 = ⊥
source
@[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
source
@[protected, instance]
def ideal.has_mul {R : Type u} [comm_semiring R] :
has_mul (ideal R)
Equations
source
@[simp]
theorem ideal.one_eq_top {R : Type u} [comm_semiring R] :
1 = ⊤
source
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
source
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
source
theorem ideal.pow_mem_pow {R : Type u} [comm_semiring R] {I : ideal R} {x : R} (hx : x ∈ I) (n : ℕ) :
x ^ n ∈ I ^ n
source
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)
source
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
source
theorem ideal.mul_le_left {R : Type u} [comm_semiring R] {I J : ideal R} :
I * J ≤ J
source
theorem ideal.mul_le_right {R : Type u} [comm_semiring R] {I J : ideal R} :
I * J ≤ I
source
@[simp]
theorem ideal.sup_mul_right_self {R : Type u} [comm_semiring R] {I J : ideal R} :
I ⊔ I * J = I
source
@[simp]
theorem ideal.sup_mul_left_self {R : Type u} [comm_semiring R] {I J : ideal R} :
I ⊔ J * I = I
source
@[simp]
theorem ideal.mul_right_self_sup {R : Type u} [comm_semiring R] {I J : ideal R} :
I * J ⊔ I = I
source
@[simp]
theorem ideal.mul_left_self_sup {R : Type u} [comm_semiring R] {I J : ideal R} :
J * I ⊔ I = I
source
@[protected]
theorem ideal.mul_comm {R : Type u} [comm_semiring R] (I J : ideal R) :
I * J = J * I
source
@[protected]
theorem ideal.mul_assoc {R : Type u} [comm_semiring R] (I J K : ideal R) :
I * J * K = I * (J * K)
source
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})
source
theorem ideal.span_mul_span' {R : Type u} [comm_semiring R] (S T : set R) :
ideal.span S * ideal.span T = ideal.span (S * T)
source
theorem ideal.span_singleton_mul_span_singleton {R : Type u} [comm_semiring R] (r s : R) :
ideal.span {r} * ideal.span {s} = ideal.span {r * s}
source
theorem ideal.span_singleton_pow {R : Type u} [comm_semiring R] (s : R) (n : ℕ) :
ideal.span {s} ^ n = ideal.span {s ^ n}
source
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
source
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
source
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)
source
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
source
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)
source
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
source
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)
source
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))
source
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)}
source
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)}
source
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)}
source
theorem ideal.sup_eq_top_iff_is_coprime {R : Type u_1} [comm_semiring R] (x y : R) :
ideal.span {x} ⊔ ideal.span {y} = ⊤ ↔ is_coprime x y
source
theorem ideal.mul_le_inf {R : Type u} [comm_semiring R] {I J : ideal R} :
I * J ≤ I ⊓ J
source
theorem ideal.multiset_prod_le_inf {R : Type u} [comm_semiring R] {s : multiset (ideal R)} :
s.prod ≤ s.inf
source
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
source
theorem ideal.mul_eq_inf_of_coprime {R : Type u} [comm_semiring R] {I J : ideal R} (h : I ⊔ J = ⊤) :
I * J = I ⊓ J
source
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
source
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
source
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
source
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
source
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) = ⊤
source
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) = ⊤
source
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 = ⊤
source
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 = ⊤
source
theorem ideal.sup_pow_eq_top {R : Type u} [comm_semiring R] {I J : ideal R} {n : ℕ} (h : I ⊔ J = ⊤) :
I ⊔ J ^ n = ⊤
source
theorem ideal.pow_sup_eq_top {R : Type u} [comm_semiring R] {I J : ideal R} {n : ℕ} (h : I ⊔ J = ⊤) :
I ^ n ⊔ J = ⊤
source
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 = ⊤
source
@[simp]
theorem ideal.mul_bot {R : Type u} [comm_semiring R] (I : ideal R) :
I * ⊥ = ⊥
source
@[simp]
theorem ideal.bot_mul {R : Type u} [comm_semiring R] (I : ideal R) :
⊥ * I = ⊥
source
@[simp]
theorem ideal.mul_top {R : Type u} [comm_semiring R] (I : ideal R) :
I * ⊤ = I
source
@[simp]
theorem ideal.top_mul {R : Type u} [comm_semiring R] (I : ideal R) :
⊤ * I = I
source
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
source
theorem ideal.mul_mono_left {R : Type u} [comm_semiring R] {I J K : ideal R} (h : I ≤ J) :
I * K ≤ J * K
source
theorem ideal.mul_mono_right {R : Type u} [comm_semiring R] {I J K : ideal R} (h : J ≤ K) :
I * J ≤ I * K
source
theorem ideal.mul_sup {R : Type u} [comm_semiring R] (I J K : ideal R) :
I * (J ⊔ K) = I * J ⊔ I * K
source
theorem ideal.sup_mul {R : Type u} [comm_semiring R] (I J K : ideal R) :
(I ⊔ J) * K = I * K ⊔ J * K
source
theorem ideal.pow_le_pow {R : Type u} [comm_semiring R] {I : ideal R} {m n : ℕ} (h : m ≤ n) :
I ^ n ≤ I ^ m
source
theorem ideal.pow_le_self {R : Type u} [comm_semiring R] {I : ideal R} {n : ℕ} (hn : n ≠ 0) :
I ^ n ≤ I
source
theorem ideal.pow_mono {R : Type u} [comm_semiring R] {I J : ideal R} (e : I ≤ J) (n : ℕ) :
I ^ n ≤ J ^ n
source
theorem ideal.mul_eq_bot {R : Type u_1} [comm_semiring R] [no_zero_divisors R] {I J : ideal R} :
I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥
source
@[protected, instance]
def ideal.no_zero_divisors {R : Type u_1} [comm_semiring R] [no_zero_divisors R] :
no_zero_divisors (ideal R)
source
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.

source
def ideal.radical {R : Type u} [comm_semiring R] (I : ideal R) :
ideal R

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

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

An ideal is radical if it contains its radical.

Equations
source
theorem ideal.le_radical {R : Type u} [comm_semiring R] {I : ideal R} :
I ≤ I.radical
source
theorem ideal.radical_eq_iff {R : Type u} [comm_semiring R] {I : ideal R} :
I.radical = I ↔ I.is_radical

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

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

Alias of the reverse direction of ideal.radical_eq_iff.

source
theorem ideal.radical_top (R : Type u) [comm_semiring R] :
⊤.radical = ⊤
source
theorem ideal.radical_mono {R : Type u} [comm_semiring R] {I J : ideal R} (H : I ≤ J) :
I.radical ≤ J.radical
source
theorem ideal.radical_is_radical {R : Type u} [comm_semiring R] (I : ideal R) :
I.radical.is_radical
source
@[simp]
theorem ideal.radical_idem {R : Type u} [comm_semiring R] (I : ideal R) :
I.radical.radical = I.radical
source
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
source
theorem ideal.radical_le_radical_iff {R : Type u} [comm_semiring R] {I J : ideal R} :
I.radical ≤ J.radical ↔ I ≤ J.radical
source
theorem ideal.radical_eq_top {R : Type u} [comm_semiring R] {I : ideal R} :
I.radical = ⊤ ↔ I = ⊤
source
theorem ideal.is_prime.is_radical {R : Type u} [comm_semiring R] {I : ideal R} (H : I.is_prime) :
I.is_radical
source
theorem ideal.is_prime.radical {R : Type u} [comm_semiring R] {I : ideal R} (H : I.is_prime) :
I.radical = I
source
theorem ideal.radical_sup {R : Type u} [comm_semiring R] (I J : ideal R) :
(I ⊔ J).radical = (I.radical ⊔ J.radical).radical
source
theorem ideal.radical_inf {R : Type u} [comm_semiring R] (I J : ideal R) :
(I ⊓ J).radical = I.radical ⊓ J.radical
source
theorem ideal.radical_mul {R : Type u} [comm_semiring R] (I J : ideal R) :
(I * J).radical = I.radical ⊓ J.radical
source
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
source
theorem ideal.radical_eq_Inf {R : Type u} [comm_semiring R] (I : ideal R) :
I.radical = has_Inf.Inf {J : ideal R | I ≤ J ∧ J.is_prime}
source
theorem ideal.is_radical_bot_of_no_zero_divisors {R : Type u_1} [comm_semiring R] [no_zero_divisors R] :
⊥.is_radical
source
@[simp]
theorem ideal.radical_bot_of_no_zero_divisors {R : Type u} [comm_semiring R] [no_zero_divisors R] :
⊥.radical = ⊥
source
@[protected, instance]
def ideal.comm_semiring {R : Type u} [comm_semiring R] :
comm_semiring (ideal R)
Equations
source
theorem ideal.top_pow (R : Type u) [comm_semiring R] (n : ℕ) :
⊤ ^ n = ⊤
source
theorem ideal.radical_pow {R : Type u} [comm_semiring R] (I : ideal R) (n : ℕ) (H : n > 0) :
(I ^ n).radical = I.radical
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem ideal.subset_union {R : Type u} [ring R] {I J K : ideal R} :
↑I ⊆ ↑J ∪ ↑K ↔ I ≤ J ∨ I ≤ K
source
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
source
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.

source
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.

source
theorem ideal.is_unit_iff {R : Type u} [comm_semiring R] {I : ideal R} :
is_unit I ↔ I = ⊤
source
@[protected, instance]
def ideal.unique_units {R : Type u} [comm_semiring R] :
unique (ideal R)ˣ
Equations
source
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) :
ideal 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
source
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) :
ideal R

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

Equations
Instances for ideal.comap
source
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) :
ideal.map f I ≤ ideal.map f J
source
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) :
⇑f x ∈ ideal.map f I
source
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) :
⇑f ↑x ∈ ideal.map f I
source
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} :
ideal.map f I ≤ K ↔ I ≤ ideal.comap f K
source
@[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} :
x ∈ ideal.comap f K ↔ ⇑f x ∈ K
source
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) :
ideal.comap f K ≤ ideal.comap f L
source
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 ≠ ⊤) :
ideal.comap f K ≠ ⊤
source
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) :
ideal.map f I ≤ ideal.comap g I
source
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)) :
ideal.comap f I ≤ ideal.map g I
source
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) :
ideal.map f I ≤ ideal.comap g I

The ideal version of set.image_subset_preimage_of_inverse.

source
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) :
ideal.comap f I ≤ ideal.map g I

The ideal version of set.preimage_subset_image_of_inverse.

source
@[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] :
(ideal.comap f K).is_prime
source
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) :
ideal.map f ⊤ = ⊤
source
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) :
galois_connection (ideal.map f) (ideal.comap f)
source
@[simp]
theorem ideal.comap_id {R : Type u} [semiring R] (I : ideal R) :
ideal.comap (ring_hom.id R) I = I
source
@[simp]
theorem ideal.map_id {R : Type u} [semiring R] (I : ideal R) :
ideal.map (ring_hom.id R) I = I
source
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) :
ideal.comap f (ideal.comap g I) = ideal.comap (g.comp f) I
source
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) :
ideal.map g (ideal.map f I) = ideal.map (g.comp f) I
source
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) :
ideal.map f (ideal.span s) = ideal.span (⇑f '' s)
source
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} :
I ≤ ideal.comap f K → ideal.map f I ≤ K
source
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} :
ideal.map f I ≤ K → I ≤ ideal.comap f K
source
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} :
I ≤ ideal.comap f (ideal.map f I)
source
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} :
ideal.map f (ideal.comap f K) ≤ K
source
@[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} :
ideal.comap f ⊤ = ⊤
source
@[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} :
ideal.comap f I = ⊤ ↔ I = ⊤
source
@[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} :
ideal.map f ⊥ = ⊥
source
@[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) :
ideal.map f (ideal.comap f (ideal.map f I)) = ideal.map f I
source
@[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) :
ideal.comap f (ideal.map f (ideal.comap f K)) = ideal.comap f K
source
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) :
ideal.map f (I ⊔ J) = ideal.map f I ⊔ ideal.map f J
source
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) :
ideal.comap f (K ⊓ L) = ideal.comap f K ⊓ ideal.comap f L
source
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)
source
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)
source
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
source
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
source
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
source
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] :
(ideal.comap f K).is_prime
source
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} :
ideal.map f (I ⊓ J) ≤ ideal.map f I ⊓ ideal.map f J
source
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} :
ideal.comap f K ⊔ ideal.comap f L ≤ ideal.comap f (K ⊔ L)
source
@[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) :
I • ⊤ = submodule.restrict_scalars R (ideal.map (algebra_map R S) I)
source
@[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) :
↑(submodule.restrict_scalars R I) = ↑I
source
@[simp]
theorem ideal.restrict_scalars_mul {R : Type u_1} {S : Type u_2} [comm_semiring R] [comm_semiring S] [algebra R S] (I J : ideal S) :
submodule.restrict_scalars R (I * J) = submodule.restrict_scalars R I * submodule.restrict_scalars R J

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

source
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) :
ideal.map f (ideal.comap f I) = I
source
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) :
galois_insertion (ideal.map f) (ideal.comap f)

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

Equations
source
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) :
function.surjective (ideal.map f)
source
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) :
function.injective (ideal.comap f)
source
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) :
ideal.map f (ideal.comap f I ⊔ ideal.comap f J) = I ⊔ J
source
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
source
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) :
ideal.map f (ideal.comap f I ⊓ ideal.comap f J) = I ⊓ J
source
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
source
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) :
y ∈ ⇑f '' ↑I
source
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
source
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) :
ideal.comap f K ≤ I → K ≤ ideal.map f I
source
theorem ideal.map_eq_submodule_map {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) [h : ring_hom_surjective f] (I : ideal R) :
ideal.map f I = submodule.map f.to_semilinear_map I
source
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) :
ideal.comap f ⊥ ≤ I
source
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) :
ideal.comap f (ideal.map f I) = I ⊔ ideal.comap f ⊥
source
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) :
ideal S ≃o {p // ideal.comap f ⊥ ≤ p}

Correspondence theorem

Equations
source
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) :
ideal S ↪o ideal R

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

Equations
source
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) :
ideal.map f I = ⊤ ∨ (ideal.map f I).is_maximal
source
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] :
(ideal.comap f K).is_maximal
source
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) :
ideal.comap f I ≤ ideal.comap f J ↔ I ≤ J
source
@[simp]
theorem ideal.map_of_equiv {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (f : R ≃+* S) :
ideal.map ↑(f.symm) (ideal.map ↑f I) = I

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

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

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

source
theorem ideal.map_comap_of_equiv {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (f : R ≃+* S) :
ideal.map ↑f I = ideal.comap f.symm I

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

source
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) :
ideal S ≃o ideal R

Special case of the correspondence theorem for isomorphic rings

Equations
source
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} :
ideal.comap f K ≤ I ↔ K ≤ ideal.map f I
source
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) :
(ideal.map f I).is_maximal
source
theorem ideal.ring_equiv.bot_maximal_iff {R : Type u} {S : Type v} [ring R] [ring S] (e : R ≃+* S) :
⊥.is_maximal ↔ ⊥.is_maximal
source
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
source
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) :
ideal R →*₀ ideal S

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

Equations
source
@[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) :
⇑(ideal.map_hom f) I = ideal.map f I
source
@[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
source
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) :
ideal.comap f K.radical = (ideal.comap f K).radical
source
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) :
(ideal.comap f K).is_radical
source
@[simp]
theorem ideal.map_quotient_self {R : Type u} [comm_ring R] (I : ideal R) :
ideal.map (ideal.quotient.mk I) I = ⊥
source
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} :
ideal.map f I.radical ≤ (ideal.map f I).radical
source
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} :
ideal.comap f K * ideal.comap f L ≤ ideal.comap f (K * L)
source
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)
source
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
source
theorem ideal.is_prime.is_primary {R : Type u} [comm_semiring R] {I : ideal R} (hi : I.is_prime) :
I.is_primary
source
theorem ideal.mem_radical_of_pow_mem {R : Type u} [comm_semiring R] {I : ideal R} {x : R} {m : ℕ} (hx : x ^ m ∈ I.radical) :
x ∈ I.radical
source
theorem ideal.is_prime_radical {R : Type u} [comm_semiring R] {I : ideal R} (hi : I.is_primary) :
I.radical.is_prime
source
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) :
(I ⊓ J).is_primary
source
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) :
(ι →₀ ↥I) →ₗ[R] M

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

Equations
source
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)
source
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)
source
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} :
linear_map.range (ideal.finsupp_total ι M I v) = I • submodule.span R (set.range v)
source
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
source
@[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 : ι) :
↑(⇑(ideal.basis_span_singleton b hx) i) = x * ⇑b i
source
@[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) :
⇑(b.constr N) (coe ∘ ⇑(ideal.basis_span_singleton b hx)) = ⇑(algebra.lmul R S) x
source
theorem associates.mk_ne_zero' {R : Type u_1} [comm_semiring R] {r : R} :
associates.mk (ideal.span {r}) ≠ 0 ↔ r ≠ 0
source
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.

source
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.

source
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) :
ideal R

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

Equations
Instances for ring_hom.ker
source
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} :
r ∈ ring_hom.ker f ↔ ⇑f r = 0

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

source
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) :
↑(ring_hom.ker f) = ⇑f ⁻¹' {0}
source
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) :
ring_hom.ker f = ideal.comap f ⊥
source
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) :
ideal.comap g (ring_hom.ker f) = ring_hom.ker (f.comp g)
source
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) :
1 ∉ ring_hom.ker f

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

source
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) :
ring_hom.ker f ≠ ⊤
source
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) :
function.injective ⇑f ↔ ring_hom.ker f = ⊥
source
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
source
@[simp]
theorem ring_hom.ker_coe_equiv {R : Type u} {S : Type v} [ring R] [semiring S] (f : R ≃+* S) :
ring_hom.ker ↑f = ⊥
source
@[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') :
ring_hom.ker f = ⊥
source
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
source
def ring_hom.ker_lift {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :
R ⧸ ring_hom.ker f →+* S

The induced map from the quotient by the kernel to the codomain.

This is an isomorphism if f has a right inverse (quotient_ker_equiv_of_right_inverse) / is surjective (quotient_ker_equiv_of_surjective).

Equations
source
@[simp]
theorem ring_hom.ker_lift_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (r : R) :
⇑(f.ker_lift) (⇑(ideal.quotient.mk (ring_hom.ker f)) r) = ⇑f r
source
theorem ring_hom.ker_lift_injective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :
function.injective ⇑(f.ker_lift)

The induced map from the quotient by the kernel is injective.

source
theorem ring_hom.lift_injective_of_ker_le_ideal {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I : ideal R) {f : R →+* S} (H : ∀ (a : R), a ∈ I → ⇑f a = 0) (hI : ring_hom.ker f ≤ I) :
function.injective ⇑(ideal.quotient.lift I f H)
source
def ring_hom.quotient_ker_equiv_of_right_inverse {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S → R} (hf : function.right_inverse g ⇑f) :
R ⧸ ring_hom.ker f ≃+* S

The first isomorphism theorem for commutative rings, computable version.

Equations
source
@[simp]
theorem ring_hom.quotient_ker_equiv_of_right_inverse.apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S → R} (hf : function.right_inverse g ⇑f) (x : R ⧸ ring_hom.ker f) :
⇑(ring_hom.quotient_ker_equiv_of_right_inverse hf) x = ⇑(f.ker_lift) x
source
@[simp]
theorem ring_hom.quotient_ker_equiv_of_right_inverse.symm.apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S → R} (hf : function.right_inverse g ⇑f) (x : S) :
⇑((ring_hom.quotient_ker_equiv_of_right_inverse hf).symm) x = ⇑(ideal.quotient.mk (ring_hom.ker f)) (g x)
source
noncomputable def ring_hom.quotient_ker_equiv_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective ⇑f) :
R ⧸ ring_hom.ker f ≃+* S

The first isomorphism theorem for commutative rings.

Equations
source
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) :
(ring_hom.ker f).is_prime

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

source
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) :
(ring_hom.ker f).is_maximal

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

source
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) :
ideal.map f I = ⊥ ↔ I ≤ ring_hom.ker f
source
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) :
ring_hom.ker f ≤ ideal.comap f K
source
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) :
(∀ (J : ideal R), J ∈ A → ring_hom.ker f ≤ J) → ideal.map f (has_Inf.Inf A) = has_Inf.Inf (ideal.map f '' A)
source
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) :
(ideal.map f I).is_prime
source
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) :
ideal.map f I = ⊥ ↔ I = ⊥
source
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] :
(ideal.map f I).is_prime
source
@[simp]
theorem ideal.mk_ker {R : Type u_1} [comm_ring R] {I : ideal R} :
ring_hom.ker (ideal.quotient.mk I) = I
source
theorem ideal.map_mk_eq_bot_of_le {R : Type u_1} [comm_ring R] {I J : ideal R} (h : I ≤ J) :
ideal.map (ideal.quotient.mk J) I = ⊥
source
theorem ideal.ker_quotient_lift {R : Type u_1} [comm_ring R] {S : Type v} [comm_ring S] {I : ideal R} (f : R →+* S) (H : I ≤ ring_hom.ker f) :
ring_hom.ker (ideal.quotient.lift I f H) = ideal.map (ideal.quotient.mk I) (ring_hom.ker f)
source
theorem ideal.map_eq_iff_sup_ker_eq_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I J : ideal R} (f : R →+* S) (hf : function.surjective ⇑f) :
ideal.map f I = ideal.map f J ↔ I ⊔ ring_hom.ker f = J ⊔ ring_hom.ker f
source
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) :
ideal.map f I.radical = (ideal.map f I).radical
source
@[simp]
theorem ideal.bot_quotient_is_maximal_iff {R : Type u_1} [comm_ring R] (I : ideal R) :
⊥.is_maximal ↔ I.is_maximal
source
@[simp]
theorem ideal.mem_quotient_iff_mem_sup {R : Type u_1} [comm_ring R] {I J : ideal R} {x : R} :
⇑(ideal.quotient.mk I) x ∈ ideal.map (ideal.quotient.mk I) J ↔ x ∈ J ⊔ I

See also ideal.mem_quotient_iff_mem in case I ≤ J.

source
theorem ideal.mem_quotient_iff_mem {R : Type u_1} [comm_ring R] {I J : ideal R} (hIJ : I ≤ J) {x : R} :
⇑(ideal.quotient.mk I) x ∈ ideal.map (ideal.quotient.mk I) J ↔ x ∈ J

See also ideal.mem_quotient_iff_mem_sup if the assumption I ≤ J is not available.

source
@[protected, instance]
def ideal.quotient.algebra (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {I : ideal A} :
algebra R₁ (A ⧸ I)

The R₁-algebra structure on A/I for an R₁-algebra A

Equations
source
@[protected, instance]
def ideal.quotient.is_scalar_tower (R₁ : Type u_4) (R₂ : Type u_5) {A : Type u_6} [comm_semiring R₁] [comm_semiring R₂] [comm_ring A] [algebra R₁ A] [algebra R₂ A] [has_smul R₁ R₂] [is_scalar_tower R₁ R₂ A] (I : ideal A) :
is_scalar_tower R₁ R₂ (A ⧸ I)
source
def ideal.quotient.mkₐ (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
A →ₐ[R₁] A ⧸ I

The canonical morphism A →ₐ[R₁] A ⧸ I as morphism of R₁-algebras, for I an ideal of A, where A is an R₁-algebra.

Equations
source
theorem ideal.quotient.alg_hom_ext (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {I : ideal A} {S : Type u_1} [semiring S] [algebra R₁ S] ⦃f g : A ⧸ I →ₐ[R₁] S⦄ (h : f.comp (ideal.quotient.mkₐ R₁ I) = g.comp (ideal.quotient.mkₐ R₁ I)) :
f = g
source
theorem ideal.quotient.alg_map_eq (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
algebra_map R₁ (A ⧸ I) = (algebra_map A (A ⧸ I)).comp (algebra_map R₁ A)
source
theorem ideal.quotient.mkₐ_to_ring_hom (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
(ideal.quotient.mkₐ R₁ I).to_ring_hom = ideal.quotient.mk I
source
@[simp]
theorem ideal.quotient.mkₐ_eq_mk (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
⇑(ideal.quotient.mkₐ R₁ I) = ⇑(ideal.quotient.mk I)
source
@[simp]
theorem ideal.quotient.algebra_map_eq {R : Type u_1} [comm_ring R] (I : ideal R) :
algebra_map R (R ⧸ I) = ideal.quotient.mk I
source
@[simp]
theorem ideal.quotient.mk_comp_algebra_map (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
(ideal.quotient.mk I).comp (algebra_map R₁ A) = algebra_map R₁ (A ⧸ I)
source
@[simp]
theorem ideal.quotient.mk_algebra_map (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) (x : R₁) :
⇑(ideal.quotient.mk I) (⇑(algebra_map R₁ A) x) = ⇑(algebra_map R₁ (A ⧸ I)) x
source
theorem ideal.quotient.mkₐ_surjective (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
function.surjective ⇑(ideal.quotient.mkₐ R₁ I)

The canonical morphism A →ₐ[R₁] I.quotient is surjective.

source
@[simp]
theorem ideal.quotient.mkₐ_ker (R₁ : Type u_4) {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] (I : ideal A) :
ring_hom.ker ↑(ideal.quotient.mkₐ R₁ I) = I

The kernel of A →ₐ[R₁] I.quotient is I.

source
def ideal.quotient.liftₐ {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (I : ideal A) (f : A →ₐ[R₁] B) (hI : ∀ (a : A), a ∈ I → ⇑f a = 0) :
A ⧸ I →ₐ[R₁] B

ideal.quotient.lift as an alg_hom.

Equations
source
@[simp]
theorem ideal.quotient.liftₐ_apply {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (I : ideal A) (f : A →ₐ[R₁] B) (hI : ∀ (a : A), a ∈ I → ⇑f a = 0) (x : A ⧸ I) :
⇑(ideal.quotient.liftₐ I f hI) x = ⇑(ideal.quotient.lift I ↑f hI) x
source
theorem ideal.quotient.liftₐ_comp {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (I : ideal A) (f : A →ₐ[R₁] B) (hI : ∀ (a : A), a ∈ I → ⇑f a = 0) :
(ideal.quotient.liftₐ I f hI).comp (ideal.quotient.mkₐ R₁ I) = f
source
theorem ideal.ker_lift.map_smul {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) (r : R₁) (x : A ⧸ ring_hom.ker f.to_ring_hom) :
⇑(f.to_ring_hom.ker_lift) (r • x) = r • ⇑(f.to_ring_hom.ker_lift) x
source
def ideal.ker_lift_alg {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) :
A ⧸ ring_hom.ker f.to_ring_hom →ₐ[R₁] B

The induced algebras morphism from the quotient by the kernel to the codomain.

This is an isomorphism if f has a right inverse (quotient_ker_alg_equiv_of_right_inverse) / is surjective (quotient_ker_alg_equiv_of_surjective).

Equations
source
@[simp]
theorem ideal.ker_lift_alg_mk {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) (a : A) :
⇑(ideal.ker_lift_alg f) (⇑(ideal.quotient.mk (ring_hom.ker f.to_ring_hom)) a) = ⇑f a
source
@[simp]
theorem ideal.ker_lift_alg_to_ring_hom {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) :
(ideal.ker_lift_alg f).to_ring_hom = ↑f.ker_lift
source
theorem ideal.ker_lift_alg_injective {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] (f : A →ₐ[R₁] B) :
function.injective ⇑(ideal.ker_lift_alg f)

The induced algebra morphism from the quotient by the kernel is injective.

source
def ideal.quotient_ker_alg_equiv_of_right_inverse {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : function.right_inverse g ⇑f) :
(A ⧸ ring_hom.ker f.to_ring_hom) ≃ₐ[R₁] B

The first isomorphism theorem for algebras, computable version.

Equations
source
@[simp]
theorem ideal.quotient_ker_alg_equiv_of_right_inverse.apply {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : function.right_inverse g ⇑f) (x : A ⧸ ring_hom.ker f.to_ring_hom) :
⇑(ideal.quotient_ker_alg_equiv_of_right_inverse hf) x = ⇑(ideal.ker_lift_alg f) x
source
@[simp]
theorem ideal.quotient_ker_alg_equiv_of_right_inverse_symm.apply {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : function.right_inverse g ⇑f) (x : B) :
⇑((ideal.quotient_ker_alg_equiv_of_right_inverse hf).symm) x = ⇑(ideal.quotient.mkₐ R₁ (ring_hom.ker f.to_ring_hom)) (g x)
source
noncomputable def ideal.quotient_ker_alg_equiv_of_surjective {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {f : A →ₐ[R₁] B} (hf : function.surjective ⇑f) :
(A ⧸ ring_hom.ker f.to_ring_hom) ≃ₐ[R₁] B

The first isomorphism theorem for algebras.

Equations
source
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) (hIJ : I ≤ ideal.comap f J) :
R ⧸ I →+* S ⧸ J

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

Equations
source
@[simp]
theorem ideal.quotient_map_mk {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J ≤ ideal.comap f I} {x : R} :
⇑(I.quotient_map f H) (⇑(ideal.quotient.mk J) x) = ⇑(ideal.quotient.mk I) (⇑f x)
source
@[simp]
theorem ideal.quotient_map_algebra_map {S : Type u_2} [comm_ring S] {R₁ : Type u_4} {A : Type u_6} [comm_semiring R₁] [comm_ring A] [algebra R₁ A] {J : ideal A} {I : ideal S} {f : A →+* S} {H : J ≤ ideal.comap f I} {x : R₁} :
⇑(I.quotient_map f H) (⇑(algebra_map R₁ (A ⧸ J)) x) = ⇑(ideal.quotient.mk I) (⇑f (⇑(algebra_map R₁ A) x))
source
theorem ideal.quotient_map_comp_mk {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} (H : J ≤ ideal.comap f I) :
(I.quotient_map f H).comp (ideal.quotient.mk J) = (ideal.quotient.mk I).comp f
source
@[simp]
theorem ideal.quotient_equiv_symm_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = ideal.map ↑f I) (ᾰ : S ⧸ J) :
⇑((I.quotient_equiv J f hIJ).symm) ᾰ = ⇑(I.quotient_map ↑(f.symm) _) ᾰ
source
def ideal.quotient_equiv {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = ideal.map ↑f I) :
R ⧸ I ≃+* S ⧸ J

The ring equiv R/I ≃+* S/J induced by a ring equiv f : R ≃+** S, where J = f(I).

Equations
source
@[simp]
theorem ideal.quotient_equiv_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = ideal.map ↑f I) (ᾰ : R ⧸ I) :
⇑(I.quotient_equiv J f hIJ) ᾰ = (J.quotient_map ↑f _).to_fun ᾰ
source
@[simp]
theorem ideal.quotient_equiv_mk {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = ideal.map ↑f I) (x : R) :
⇑(I.quotient_equiv J f hIJ) (⇑(ideal.quotient.mk I) x) = ⇑(ideal.quotient.mk J) (⇑f x)
source
@[simp]
theorem ideal.quotient_equiv_symm_mk {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = ideal.map ↑f I) (x : S) :
⇑((I.quotient_equiv J f hIJ).symm) (⇑(ideal.quotient.mk J) x) = ⇑(ideal.quotient.mk I) (⇑(f.symm) x)
source
theorem ideal.quotient_map_injective' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J ≤ ideal.comap f I} (h : ideal.comap f I ≤ J) :
function.injective ⇑(I.quotient_map f H)

H and h are kept as separate hypothesis since H is used in constructing the quotient map.

source
theorem ideal.quotient_map_injective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal S} {f : R →+* S} :
function.injective ⇑(I.quotient_map f le_rfl)

If we take J = I.comap f then quotient_map is injective automatically.

source
theorem ideal.quotient_map_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J ≤ ideal.comap f I} (hf : function.surjective ⇑f) :
function.surjective ⇑(I.quotient_map f H)
source
theorem ideal.comp_quotient_map_eq_of_comp_eq {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {R' : Type u_3} {S' : Type u_4} [comm_ring R'] [comm_ring S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f) (I : ideal S') :
(I.quotient_map g' le_rfl).comp ((ideal.comap g' I).quotient_map f le_rfl) = (I.quotient_map f' le_rfl).comp ((ideal.comap f' I).quotient_map g _)

Commutativity of a square is preserved when taking quotients by an ideal.

source
def ideal.quotient_mapₐ {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {I : ideal A} (J : ideal B) (f : A →ₐ[R₁] B) (hIJ : I ≤ ideal.comap f J) :
A ⧸ I →ₐ[R₁] B ⧸ J

The algebra hom A/I →+* B/J induced by an algebra hom f : A →ₐ[R₁] B with I ≤ f⁻¹(J).

Equations
source
@[simp]
theorem ideal.quotient_map_mkₐ {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {I : ideal A} (J : ideal B) (f : A →ₐ[R₁] B) (H : I ≤ ideal.comap f J) {x : A} :
⇑(J.quotient_mapₐ f H) (⇑(ideal.quotient.mk I) x) = ⇑(ideal.quotient.mkₐ R₁ J) (⇑f x)
source
theorem ideal.quotient_map_comp_mkₐ {R₁ : Type u_4} {A : Type u_6} {B : Type u_7} [comm_semiring R₁] [comm_ring A] [comm_ring B] [algebra R₁ A] [algebra R₁ B] {I : ideal A} (J : ideal B) (f : A →ₐ[R₁] B) (H : I ≤ ideal.comap f J) :
(J.quotient_mapₐ f H).