# mathlib3documentation

ring_theory.ideal.basic

# Ideals over a ring #

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

This file defines ideal R, the type of (left) ideals over a ring R. Note that over commutative rings, left ideals and two-sided ideals are equivalent.

## Implementation notes #

ideal R is implemented using submodule R R, where • is interpreted as *.

## TODO #

Support right ideals, and two-sided ideals over non-commutative rings.

@[reducible]
def ideal (R : Type u) [semiring R] :

A (left) ideal in a semiring R is an additive submonoid s such that a * b ∈ s whenever b ∈ s. If R is a ring, then s is an additive subgroup.

Equations
• = R
@[protected]
theorem ideal.zero_mem {α : Type u} [semiring α] (I : ideal α) :
0 I
@[protected]
theorem ideal.add_mem {α : Type u} [semiring α] (I : ideal α) {a b : α} :
a I b I a + b I
theorem ideal.mul_mem_left {α : Type u} [semiring α] (I : ideal α) (a : α) {b : α} :
b I a * b I
@[ext]
theorem ideal.ext {α : Type u} [semiring α] {I J : ideal α} (h : (x : α), x I x J) :
I = J
theorem ideal.sum_mem {α : Type u} [semiring α] (I : ideal α) {ι : Type u_1} {t : finset ι} {f : ι α} :
( (c : ι), c t f c I) t.sum (λ (i : ι), f i) I
theorem ideal.eq_top_of_unit_mem {α : Type u} [semiring α] (I : ideal α) (x y : α) (hx : x I) (h : y * x = 1) :
I =
theorem ideal.eq_top_of_is_unit_mem {α : Type u} [semiring α] (I : ideal α) {x : α} (hx : x I) (h : is_unit x) :
I =
theorem ideal.eq_top_iff_one {α : Type u} [semiring α] (I : ideal α) :
I = 1 I
theorem ideal.ne_top_iff_one {α : Type u} [semiring α] (I : ideal α) :
I 1 I
@[simp]
theorem ideal.unit_mul_mem_iff_mem {α : Type u} [semiring α] (I : ideal α) {x y : α} (hy : is_unit y) :
y * x I x I
def ideal.span {α : Type u} [semiring α] (s : set α) :

The ideal generated by a subset of a ring

Equations
Instances for ideal.span
@[simp]
theorem ideal.submodule_span_eq {α : Type u} [semiring α] {s : set α} :
@[simp]
theorem ideal.span_empty {α : Type u} [semiring α] :
@[simp]
theorem ideal.span_univ {α : Type u} [semiring α] :
theorem ideal.span_union {α : Type u} [semiring α] (s t : set α) :
theorem ideal.span_Union {α : Type u} [semiring α] {ι : Sort u_1} (s : ι set α) :
ideal.span ( (i : ι), s i) = (i : ι), ideal.span (s i)
theorem ideal.mem_span {α : Type u} [semiring α] {s : set α} (x : α) :
x (p : ideal α), s p x p
theorem ideal.subset_span {α : Type u} [semiring α] {s : set α} :
theorem ideal.span_le {α : Type u} [semiring α] {s : set α} {I : ideal α} :
I s I
theorem ideal.span_mono {α : Type u} [semiring α] {s t : set α} :
s t
@[simp]
theorem ideal.span_eq {α : Type u} [semiring α] (I : ideal α) :
= I
@[simp]
theorem ideal.span_singleton_one {α : Type u} [semiring α] :
theorem ideal.mem_span_insert {α : Type u} [semiring α] {s : set α} {x y : α} :
x (a z : α) (H : z , x = a * y + z
theorem ideal.mem_span_singleton' {α : Type u} [semiring α] {x y : α} :
x ideal.span {y} (a : α), a * y = x
theorem ideal.span_singleton_le_iff_mem {α : Type u} [semiring α] (I : ideal α) {x : α} :
ideal.span {x} I x I
theorem ideal.span_singleton_mul_left_unit {α : Type u} [semiring α] {a : α} (h2 : is_unit a) (x : α) :
theorem ideal.span_insert {α : Type u} [semiring α] (x : α) (s : set α) :
theorem ideal.span_eq_bot {α : Type u} [semiring α] {s : set α} :
(x : α), x s x = 0
@[simp]
theorem ideal.span_singleton_eq_bot {α : Type u} [semiring α] {x : α} :
ideal.span {x} = x = 0
theorem ideal.span_singleton_ne_top {α : Type u_1} {x : α} (hx : ¬) :
@[simp]
theorem ideal.span_zero {α : Type u} [semiring α] :
@[simp]
theorem ideal.span_one {α : Type u} [semiring α] :
theorem ideal.span_eq_top_iff_finite {α : Type u} [semiring α] (s : set α) :
(s' : finset α), s' s
theorem ideal.mem_span_singleton_sup {S : Type u_1} {x y : S} {I : ideal S} :
x ideal.span {y} I (a b : S) (H : b I), a * y + b = x
def ideal.of_rel {α : Type u} [semiring α] (r : α α Prop) :

The ideal generated by an arbitrary binary relation.

Equations
• = {x : α | (a b : α) (h : r a b), x + b = a}
@[class]
structure ideal.is_prime {α : Type u} [semiring α] (I : ideal α) :
Prop

An ideal P of a ring R is prime if P ≠ R and xy ∈ P → x ∈ P ∨ y ∈ P

Instances of this typeclass
theorem ideal.is_prime_iff {α : Type u} [semiring α] {I : ideal α} :
I.is_prime I {x y : α}, x * y I x I y I
theorem ideal.is_prime.ne_top {α : Type u} [semiring α] {I : ideal α} (hI : I.is_prime) :
theorem ideal.is_prime.mem_or_mem {α : Type u} [semiring α] {I : ideal α} (hI : I.is_prime) {x y : α} :
x * y I x I y I
theorem ideal.is_prime.mem_or_mem_of_mul_eq_zero {α : Type u} [semiring α] {I : ideal α} (hI : I.is_prime) {x y : α} (h : x * y = 0) :
x I y I
theorem ideal.is_prime.mem_of_pow_mem {α : Type u} [semiring α] {I : ideal α} (hI : I.is_prime) {r : α} (n : ) (H : r ^ n I) :
r I
theorem ideal.not_is_prime_iff {α : Type u} [semiring α] {I : ideal α} :
¬I.is_prime I = (x : α) (H : x I) (y : α) (H : y I), x * y I
theorem ideal.zero_ne_one_of_proper {α : Type u} [semiring α] {I : ideal α} (h : I ) :
0 1
theorem ideal.bot_prime {R : Type u_1} [ring R] [is_domain R] :
@[class]
structure ideal.is_maximal {α : Type u} [semiring α] (I : ideal α) :
Prop
• out :

An ideal is maximal if it is maximal in the collection of proper ideals.

Instances of this typeclass
theorem ideal.is_maximal_def {α : Type u} [semiring α] {I : ideal α} :
theorem ideal.is_maximal.ne_top {α : Type u} [semiring α] {I : ideal α} (h : I.is_maximal) :
theorem ideal.is_maximal_iff {α : Type u} [semiring α] {I : ideal α} :
I.is_maximal 1 I (J : ideal α) (x : α), I J x I x J 1 J
theorem ideal.is_maximal.eq_of_le {α : Type u} [semiring α] {I J : ideal α} (hI : I.is_maximal) (hJ : J ) (IJ : I J) :
I = J
@[protected, instance]
def ideal.is_coatomic {α : Type u} [semiring α] :
theorem ideal.is_maximal.coprime_of_ne {α : Type u} [semiring α] {M M' : ideal α} (hM : M.is_maximal) (hM' : M'.is_maximal) (hne : M M') :
M M' =
theorem ideal.exists_le_maximal {α : Type u} [semiring α] (I : ideal α) (hI : I ) :
(M : ideal α), M.is_maximal I M

Krull's theorem: if I is an ideal that is not the whole ring, then it is included in some maximal ideal.

theorem ideal.exists_maximal (α : Type u) [semiring α] [nontrivial α] :
(M : ideal α), M.is_maximal

Krull's theorem: a nontrivial ring has a maximal ideal.

@[protected, instance]
def ideal.nontrivial {α : Type u} [semiring α] [nontrivial α] :
theorem ideal.maximal_of_no_maximal {R : Type u} [semiring R] {P : ideal R} (hmax : (m : ideal R), P < m ¬m.is_maximal) (J : ideal R) (hPJ : P < J) :
J =

If P is not properly contained in any maximal ideal then it is not properly contained in any proper ideal

theorem ideal.span_pair_comm {α : Type u} [semiring α] {x y : α} :
ideal.span {x, y} = ideal.span {y, x}
theorem ideal.mem_span_pair {α : Type u} [semiring α] {x y z : α} :
z ideal.span {x, y} (a b : α), a * x + b * y = z
@[simp]
theorem ideal.span_pair_add_mul_left {R : Type u} [comm_ring R] {x y : R} (z : R) :
ideal.span {x + y * z, y} = ideal.span {x, y}
@[simp]
theorem ideal.span_pair_add_mul_right {R : Type u} [comm_ring R] {x y : R} (z : R) :
ideal.span {x, y + x * z} = ideal.span {x, y}
theorem ideal.is_maximal.exists_inv {α : Type u} [semiring α] {I : ideal α} (hI : I.is_maximal) {x : α} (hx : x I) :
(y i : α) (H : i I), y * x + i = 1
theorem ideal.mem_sup_left {R : Type u} [semiring R] {S T : ideal R} {x : R} :
x S x S T
theorem ideal.mem_sup_right {R : Type u} [semiring R] {S T : ideal R} {x : R} :
x T x S T
theorem ideal.mem_supr_of_mem {R : Type u} [semiring R] {ι : Sort u_1} {S : ι } (i : ι) {x : R} :
x S i x supr S
theorem ideal.mem_Sup_of_mem {R : Type u} [semiring R] {S : set (ideal R)} {s : ideal R} (hs : s S) {x : R} :
x s x
theorem ideal.mem_Inf {R : Type u} [semiring R] {s : set (ideal R)} {x : R} :
x ⦃I : ⦄, I s x I
@[simp]
theorem ideal.mem_inf {R : Type u} [semiring R] {I J : ideal R} {x : R} :
x I J x I x J
@[simp]
theorem ideal.mem_infi {R : Type u} [semiring R] {ι : Sort u_1} {I : ι } {x : R} :
x infi I (i : ι), x I i
@[simp]
theorem ideal.mem_bot {R : Type u} [semiring R] {x : R} :
x x = 0
def ideal.pi {α : Type u} [semiring α] (I : ideal α) (ι : Type v) :
ideal α)

I^n as an ideal of R^n.

Equations
theorem ideal.mem_pi {α : Type u} [semiring α] (I : ideal α) (ι : Type v) (x : ι α) :
x I.pi ι (i : ι), x i I
theorem ideal.Inf_is_prime_of_is_chain {α : Type u} [semiring α] {s : set (ideal α)} (hs : s.nonempty) (hs' : s) (H : (p : ideal α), p s p.is_prime) :
@[simp]
theorem ideal.mul_unit_mem_iff_mem {α : Type u} (I : ideal α) {x y : α} (hy : is_unit y) :
x * y I x I
theorem ideal.mem_span_singleton {α : Type u} {x y : α} :
x ideal.span {y} y x
theorem ideal.mem_span_singleton_self {α : Type u} (x : α) :
theorem ideal.span_singleton_le_span_singleton {α : Type u} {x y : α} :
theorem ideal.span_singleton_eq_span_singleton {α : Type u} [comm_ring α] [is_domain α] {x y : α} :
theorem ideal.span_singleton_mul_right_unit {α : Type u} {a : α} (h2 : is_unit a) (x : α) :
theorem ideal.span_singleton_eq_top {α : Type u} {x : α} :
theorem ideal.span_singleton_prime {α : Type u} {p : α} (hp : p 0) :
theorem ideal.is_maximal.is_prime {α : Type u} {I : ideal α} (H : I.is_maximal) :
@[protected, instance]
def ideal.is_maximal.is_prime' {α : Type u} (I : ideal α) [H : I.is_maximal] :
theorem ideal.span_singleton_lt_span_singleton {β : Type v} [comm_ring β] [is_domain β] {x y : β} :
theorem ideal.factors_decreasing {β : Type v} [comm_ring β] [is_domain β] (b₁ b₂ : β) (h₁ : b₁ 0) (h₂ : ¬is_unit b₂) :
ideal.span {b₁ * b₂} < ideal.span {b₁}
theorem ideal.mul_mem_right {α : Type u} {a : α} (b : α) (I : ideal α) (h : a I) :
a * b I
theorem ideal.pow_mem_of_mem {α : Type u} {a : α} (I : ideal α) (ha : a I) (n : ) (hn : 0 < n) :
a ^ n I
theorem ideal.is_prime.mul_mem_iff_mem_or_mem {α : Type u} {I : ideal α} (hI : I.is_prime) {x y : α} :
x * y I x I y I
theorem ideal.is_prime.pow_mem_iff_mem {α : Type u} {I : ideal α} (hI : I.is_prime) {r : α} (n : ) (hn : 0 < n) :
r ^ n I r I
theorem ideal.pow_multiset_sum_mem_span_pow {α : Type u} (s : multiset α) (n : ) :
s.sum ^ * n + 1) ideal.span ((multiset.map (λ (x : α), x ^ (n + 1)) s).to_finset)
theorem ideal.sum_pow_mem_span_pow {α : Type u} {ι : Type u_1} (s : finset ι) (f : ι α) (n : ) :
s.sum (λ (i : ι), f i) ^ (s.card * n + 1) ideal.span ((λ (i : ι), f i ^ (n + 1)) '' s)
theorem ideal.span_pow_eq_top {α : Type u} (s : set α) (hs : = ) (n : ) :
ideal.span ((λ (x : α), x ^ n) '' s) =
@[protected]
theorem ideal.neg_mem_iff {α : Type u} [ring α] (I : ideal α) {a : α} :
-a I a I
@[protected]
theorem ideal.add_mem_iff_left {α : Type u} [ring α] (I : ideal α) {a b : α} :
b I (a + b I a I)
@[protected]
theorem ideal.add_mem_iff_right {α : Type u} [ring α] (I : ideal α) {a b : α} :
a I (a + b I b I)
@[protected]
theorem ideal.sub_mem {α : Type u} [ring α] (I : ideal α) {a b : α} :
a I b I a - b I
theorem ideal.mem_span_insert' {α : Type u} [ring α] {s : set α} {x y : α} :
x (a : α), x + a * y
@[simp]
theorem ideal.span_singleton_neg {α : Type u} [ring α] (x : α) :
theorem ideal.eq_bot_or_top {K : Type u} (I : ideal K) :
I = I =

All ideals in a division (semi)ring are trivial.

@[protected, instance]
def ideal.is_simple_order {K : Type u}  :

Ideals of a division_semiring are a simple order. Thanks to the way abbreviations work, this automatically gives a is_simple_module K instance.

theorem ideal.eq_bot_of_prime {K : Type u} (I : ideal K) [h : I.is_prime] :
I =
theorem ideal.bot_is_maximal {K : Type u}  :
theorem ideal.mul_sub_mul_mem {R : Type u_1} [comm_ring R] (I : ideal R) {a b c d : R} (h1 : a - b I) (h2 : c - d I) :
a * c - b * d I
theorem ring.exists_not_is_unit_of_not_is_field {R : Type u_1} [nontrivial R] (hf : ¬) :
(x : R) (H : x 0), ¬

Also see ideal.is_simple_order for the forward direction as an instance when R is a division (semi)ring.

This result actually holds for all division semirings, but we lack the predicate to state it.

theorem ring.ne_bot_of_is_maximal_of_not_is_field {R : Type u_1} [nontrivial R] {M : ideal R} (max : M.is_maximal) (not_field : ¬) :

When a ring is not a field, the maximal ideals are nontrivial.

theorem ideal.bot_lt_of_maximal {R : Type u} [comm_ring R] [nontrivial R] (M : ideal R) [hm : M.is_maximal] (non_field : ¬) :
< M
def nonunits (α : Type u) [monoid α] :
set α

The set of non-invertible elements of a monoid.

Equations
@[simp]
theorem mem_nonunits_iff {α : Type u} {a : α} [monoid α] :
theorem mul_mem_nonunits_right {α : Type u} {a b : α} [comm_monoid α] :
b a * b
theorem mul_mem_nonunits_left {α : Type u} {a b : α} [comm_monoid α] :
a a * b
theorem zero_mem_nonunits {α : Type u} [semiring α] :
0 0 1
@[simp]
theorem one_not_mem_nonunits {α : Type u} [monoid α] :
1
theorem coe_subset_nonunits {α : Type u} [semiring α] {I : ideal α} (h : I ) :
theorem exists_max_ideal_of_mem_nonunits {α : Type u} {a : α} (h : a ) :
(I : ideal α), I.is_maximal a I