# mathlibdocumentation

ring_theory.ideal.basic

# Ideals over a ring

This file defines ideal R, the type of ideals over a commutative ring R.

## Implementation notes

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

## TODO

Support one-sided ideals, and ideals over non-commutative rings.

See algebra.ring_quot for quotients of non-commutative rings.

def ideal (R : Type u) [comm_ring R] :
Type u

Ideal in a commutative ring is an additive subgroup s such that a * b ∈ s whenever b ∈ s.

Equations
• = R
theorem ideal.zero_mem {α : Type u} [comm_ring α] (I : ideal α) :
0 I

theorem ideal.add_mem {α : Type u} [comm_ring α] (I : ideal α) {a b : α} :
a Ib Ia + b I

theorem ideal.neg_mem_iff {α : Type u} [comm_ring α] (I : ideal α) {a : α} :
-a I a I

theorem ideal.add_mem_iff_left {α : Type u} [comm_ring α] (I : ideal α) {a b : α} :
b I(a + b I a I)

theorem ideal.add_mem_iff_right {α : Type u} [comm_ring α] (I : ideal α) {a b : α} :
a I(a + b I b I)

theorem ideal.sub_mem {α : Type u} [comm_ring α] (I : ideal α) {a b : α} :
a Ib Ia - b I

theorem ideal.mul_mem_left {α : Type u} [comm_ring α] (I : ideal α) (a : α) {b : α} :
b Ia * b I

theorem ideal.mul_mem_right {α : Type u} [comm_ring α] (I : ideal α) {a : α} (b : α) (h : a I) :
a * b I

@[ext]
theorem ideal.ext {α : Type u} [comm_ring α] {I J : ideal α} (h : ∀ (x : α), x I x J) :
I = J

theorem ideal.eq_top_of_unit_mem {α : Type u} [comm_ring α] (I : ideal α) (x y : α) (hx : x I) (h : y * x = 1) :
I =

theorem ideal.eq_top_of_is_unit_mem {α : Type u} [comm_ring α] (I : ideal α) {x : α} (hx : x I) (h : is_unit x) :
I =

theorem ideal.eq_top_iff_one {α : Type u} [comm_ring α] (I : ideal α) :
I = 1 I

theorem ideal.ne_top_iff_one {α : Type u} [comm_ring α] (I : ideal α) :
I 1 I

theorem ideal.exists_mem_ne_zero_iff_ne_bot {α : Type u} [comm_ring α] (I : ideal α) :
(∃ (p : α) (H : p I), p 0) I

theorem ideal.exists_mem_ne_zero_of_ne_bot {α : Type u} [comm_ring α] (I : ideal α) (hI : I ) :
∃ (p : α) (H : p I), p 0

@[simp]
theorem ideal.unit_mul_mem_iff_mem {α : Type u} [comm_ring α] (I : ideal α) {x y : α} (hy : is_unit y) :
y * x I x I

@[simp]
theorem ideal.mul_unit_mem_iff_mem {α : Type u} [comm_ring α] (I : ideal α) {x y : α} (hy : is_unit y) :
x * y I x I

def ideal.span {α : Type u} [comm_ring α] (s : set α) :

The ideal generated by a subset of a ring

Equations
theorem ideal.subset_span {α : Type u} [comm_ring α] {s : set α} :

theorem ideal.span_le {α : Type u} [comm_ring α] {s : set α} {I : ideal α} :
I s I

theorem ideal.span_mono {α : Type u} [comm_ring α] {s t : set α} :
s t

@[simp]
theorem ideal.span_eq {α : Type u} [comm_ring α] (I : ideal α) :
= I

@[simp]
theorem ideal.span_singleton_one {α : Type u} [comm_ring α] :

theorem ideal.mem_span_insert {α : Type u} [comm_ring α] {s : set α} {x y : α} :
x ideal.span (insert y s) ∃ (a z : α) (H : z , x = a * y + z

theorem ideal.mem_span_insert' {α : Type u} [comm_ring α] {s : set α} {x y : α} :
x ideal.span (insert y s) ∃ (a : α), x + a * y

theorem ideal.mem_span_singleton' {α : Type u} [comm_ring α] {x y : α} :
x ideal.span {y} ∃ (a : α), a * y = x

theorem ideal.mem_span_singleton {α : Type u} [comm_ring α] {x y : α} :
x ideal.span {y} y x

theorem ideal.span_singleton_le_span_singleton {α : Type u} [comm_ring α] {x y : α} :

theorem ideal.span_singleton_eq_span_singleton {α : Type u} {x y : α} :

theorem ideal.span_eq_bot {α : Type u} [comm_ring α] {s : set α} :
∀ (x : α), x sx = 0

@[simp]
theorem ideal.span_singleton_eq_bot {α : Type u} [comm_ring α] {x : α} :
ideal.span {x} = x = 0

@[simp]
theorem ideal.span_zero {α : Type u} [comm_ring α] :

theorem ideal.span_singleton_eq_top {α : Type u} [comm_ring α] {x : α} :

theorem ideal.span_singleton_mul_right_unit {α : Type u} [comm_ring α] {a : α} (h2 : is_unit a) (x : α) :

theorem ideal.span_singleton_mul_left_unit {α : Type u} [comm_ring α] {a : α} (h2 : is_unit a) (x : α) :

def ideal.of_rel {α : Type u} [comm_ring α] (r : α → α → Prop) :

The ideal generated by an arbitrary binary relation.

Equations
• = {x : α | ∃ (a b : α) (h : r a b), x = a - b}
@[class]
def ideal.is_prime {α : Type u} [comm_ring α] (I : ideal α) :
Prop

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

Equations
Instances
theorem ideal.is_prime.mem_or_mem {α : Type u} [comm_ring α] {I : ideal α} (hI : I.is_prime) {x y : α} :
x * y Ix I y I

theorem ideal.is_prime.mem_or_mem_of_mul_eq_zero {α : Type u} [comm_ring α] {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} [comm_ring α] {I : ideal α} (hI : I.is_prime) {r : α} (n : ) (H : r ^ n I) :
r I

theorem ideal.not_is_prime_iff {α : Type u} [comm_ring α] {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} [comm_ring α] {I : ideal α} (h : I ) :
0 1

theorem ideal.span_singleton_prime {α : Type u} [comm_ring α] {p : α} (hp : p 0) :

theorem ideal.bot_prime {R : Type u_1}  :

@[class]
def ideal.is_maximal {α : Type u} [comm_ring α] (I : ideal α) :
Prop

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

Equations
Instances
theorem ideal.is_maximal_iff {α : Type u} [comm_ring α] {I : ideal α} :
I.is_maximal 1 I ∀ (J : ideal α) (x : α), I Jx Ix J1 J

theorem ideal.is_maximal.eq_of_le {α : Type u} [comm_ring α] {I J : ideal α} (hI : I.is_maximal) (hJ : J ) (IJ : I J) :
I = J

theorem ideal.is_maximal.exists_inv {α : Type u} [comm_ring α] {I : ideal α} (hI : I.is_maximal) {x : α} (hx : x I) :
∃ (y : α), y * x - 1 I

theorem ideal.is_maximal.is_prime {α : Type u} [comm_ring α] {I : ideal α} (H : I.is_maximal) :

@[instance]
def ideal.is_maximal.is_prime' {α : Type u} [comm_ring α] (I : ideal α) [H : I.is_maximal] :

theorem ideal.exists_le_maximal {α : Type u} [comm_ring α] (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} [comm_ring α] [nontrivial α] :
∃ (M : ideal α), M.is_maximal

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

theorem ideal.maximal_of_no_maximal {R : Type u} [comm_ring 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.mem_span_pair {α : Type u} [comm_ring α] {x y z : α} :
z ideal.span {x, y} ∃ (a b : α), a * x + b * y = z

theorem ideal.span_singleton_lt_span_singleton {β : Type v} {x y : β} :

theorem ideal.factors_decreasing {β : Type v} (b₁ b₂ : β) (h₁ : b₁ 0) (h₂ : ¬is_unit b₂) :
ideal.span {b₁ * b₂} < ideal.span {b₁}

def ideal.quotient {α : Type u} [comm_ring α] (I : ideal α) :
Type u

The quotient R/I of a ring R by an ideal I.

Equations
@[instance]
def ideal.quotient.has_one {α : Type u} [comm_ring α] (I : ideal α) :

Equations
@[instance]
def ideal.quotient.has_mul {α : Type u} [comm_ring α] (I : ideal α) :

Equations
@[instance]
def ideal.quotient.comm_ring {α : Type u} [comm_ring α] (I : ideal α) :

Equations
def ideal.quotient.mk {α : Type u} [comm_ring α] (I : ideal α) :

The ring homomorphism from a ring R to a quotient ring R/I.

Equations
@[instance]
def ideal.quotient.inhabited {α : Type u} [comm_ring α] {I : ideal α} :

Equations
theorem ideal.quotient.eq {α : Type u} [comm_ring α] {I : ideal α} {x y : α} :
x = y x - y I

@[simp]
theorem ideal.quotient.mk_eq_mk {α : Type u} [comm_ring α] {I : ideal α} (x : α) :

theorem ideal.quotient.eq_zero_iff_mem {α : Type u} {a : α} [comm_ring α] {I : ideal α} :
a = 0 a I

theorem ideal.quotient.zero_eq_one_iff {α : Type u} [comm_ring α] {I : ideal α} :
0 = 1 I =

theorem ideal.quotient.zero_ne_one_iff {α : Type u} [comm_ring α] {I : ideal α} :
0 1 I

theorem ideal.quotient.nontrivial {α : Type u} [comm_ring α] {I : ideal α} (hI : I ) :

theorem ideal.quotient.mk_surjective {α : Type u} [comm_ring α] {I : ideal α} :

@[instance]
def ideal.quotient.integral_domain {α : Type u} [comm_ring α] (I : ideal α) [hI : I.is_prime] :

Equations
theorem ideal.quotient.is_integral_domain_iff_prime {α : Type u} [comm_ring α] (I : ideal α) :

theorem ideal.quotient.exists_inv {α : Type u} [comm_ring α] {I : ideal α} [hI : I.is_maximal] {a : I.quotient} :
a 0(∃ (b : I.quotient), a * b = 1)

def ideal.quotient.field {α : Type u} [comm_ring α] (I : ideal α) [hI : I.is_maximal] :

quotient by maximal ideal is a field. def rather than instance, since users will have computable inverses in some applications

Equations
theorem ideal.quotient.maximal_of_is_field {α : Type u} [comm_ring α] (I : ideal α) (hqf : is_field I.quotient) :

If the quotient by an ideal is a field, then the ideal is maximal.

theorem ideal.quotient.maximal_ideal_iff_is_field_quotient {α : Type u} [comm_ring α] (I : ideal α) :

The quotient of a ring by an ideal is a field iff the ideal is maximal.

def ideal.quotient.lift {α : Type u} {β : Type v} [comm_ring α] [comm_ring β] (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a Sf a = 0) :

Given a ring homomorphism f : α →+* β sending all elements of an ideal to zero, lift it to the quotient by this ideal.

Equations
@[simp]
theorem ideal.quotient.lift_mk {α : Type u} {β : Type v} {a : α} [comm_ring α] [comm_ring β] (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a Sf a = 0) :
H) ( a) = f a

@[simp]
theorem ideal.quotient.lift_comp_mk {α : Type u} {β : Type v} [comm_ring α] [comm_ring β] (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a Sf a = 0) :
H).comp = f

theorem ideal.quotient.lift_surjective {α : Type u} {β : Type v} [comm_ring α] [comm_ring β] (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a Sf a = 0) (hf : function.surjective f) :

theorem ideal.mem_sup_left {R : Type u} [comm_ring R] {S T : ideal R} {x : R} :
x Sx S T

theorem ideal.mem_sup_right {R : Type u} [comm_ring R] {S T : ideal R} {x : R} :
x Tx S T

theorem ideal.mem_supr_of_mem {R : Type u} [comm_ring R] {ι : Type u_1} {S : ι → } (i : ι) {x : R} :
x S ix supr S

theorem ideal.mem_Sup_of_mem {R : Type u} [comm_ring R] {S : set (ideal R)} {s : ideal R} (hs : s S) {x : R} :
x sx Sup S

theorem ideal.mem_Inf {R : Type u} [comm_ring R] {s : set (ideal R)} {x : R} :
x Inf s ∀ ⦃I : ⦄, I sx I

@[simp]
theorem ideal.mem_inf {R : Type u} [comm_ring R] {I J : ideal R} {x : R} :
x I J x I x J

@[simp]
theorem ideal.mem_infi {R : Type u} [comm_ring R] {ι : Type u_1} {I : ι → } {x : R} :
x infi I ∀ (i : ι), x I i

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

theorem ideal.eq_bot_or_top {K : Type u} [field K] (I : ideal K) :
I = I =

All ideals in a field are trivial.

theorem ideal.eq_bot_of_prime {K : Type u} [field K] (I : ideal K) [h : I.is_prime] :
I =

theorem ideal.bot_is_maximal {K : Type u} [field K] :

def ideal.pi {α : Type u} [comm_ring α] (I : ideal α) (ι : Type v) :
ideal (ι → α)

I^n as an ideal of R^n.

Equations
theorem ideal.mem_pi {α : Type u} [comm_ring α] (I : ideal α) (ι : Type v) (x : ι → α) :
x I.pi ι ∀ (i : ι), x i I

@[instance]
def ideal.module_pi {α : Type u} [comm_ring α] (I : ideal α) (ι : Type v) :
(I.pi ι).quotient

R^n/I^n is a R/I-module.

Equations
def ideal.pi_quot_equiv {α : Type u} [comm_ring α] (I : ideal α) (ι : Type v) :

R^n/I^n is isomorphic to (R/I)^n as an R/I-module.

Equations
theorem ideal.map_pi {α : Type u} [comm_ring α] (I : ideal α) {ι : Type u_1} [fintype ι] {ι' : Type w} (x : ι → α) (hi : ∀ (i : ι), x i I) (f : (ι → α) →ₗ[α] ι' → α) (i : ι') :
f x i I

If f : R^n → R^m is an R-linear map and I ⊆ R is an ideal, then the image of I^n is contained in I^m.

theorem ring.not_is_field_of_subsingleton {R : Type u_1} [ring R] [subsingleton R] :

theorem ring.exists_not_is_unit_of_not_is_field {R : Type u_1} [comm_ring R] [nontrivial R] (hf : ¬) :
∃ (x : R) (H : x 0), ¬

theorem ring.not_is_field_iff_exists_prime {R : Type u_1} [comm_ring R] [nontrivial R] :
∃ (p : ideal R), p p.is_prime

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 : α} [comm_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} [comm_ring α] {I : ideal α} (h : I ) :

theorem exists_max_ideal_of_mem_nonunits {α : Type u} {a : α} [comm_ring α] (h : a ) :
∃ (I : ideal α), I.is_maximal a I

@[class]
structure local_ring (α : Type u) [comm_ring α] :
Prop
• to_nontrivial :
• is_local : ∀ (a : α), is_unit (1 - a)

A commutative ring is local if it has a unique maximal ideal. Note that local_ring is a predicate.

Instances
theorem local_ring.is_unit_or_is_unit_one_sub_self {α : Type u} [comm_ring α] [local_ring α] (a : α) :
is_unit (1 - a)

theorem local_ring.is_unit_of_mem_nonunits_one_sub_self {α : Type u} [comm_ring α] [local_ring α] (a : α) (h : 1 - a ) :

theorem local_ring.is_unit_one_sub_self_of_mem_nonunits {α : Type u} [comm_ring α] [local_ring α] (a : α) (h : a ) :
is_unit (1 - a)

theorem local_ring.nonunits_add {α : Type u} [comm_ring α] [local_ring α] {x y : α} (hx : x ) (hy : y ) :
x + y

def local_ring.maximal_ideal (α : Type u) [comm_ring α] [local_ring α] :

The ideal of elements that are not units.

Equations
@[instance]

theorem local_ring.maximal_ideal_unique (α : Type u) [comm_ring α] [local_ring α] :
∃! (I : ideal α), I.is_maximal

theorem local_ring.eq_maximal_ideal {α : Type u} [comm_ring α] [local_ring α] {I : ideal α} (hI : I.is_maximal) :

theorem local_ring.le_maximal_ideal {α : Type u} [comm_ring α] [local_ring α] {J : ideal α} (hJ : J ) :

@[simp]
theorem local_ring.mem_maximal_ideal {α : Type u} [comm_ring α] [local_ring α] (x : α) :
x

theorem local_of_nonunits_ideal {α : Type u} [comm_ring α] (hnze : 0 1) (h : ∀ (x y : α), x y x + y ) :

theorem local_of_unique_max_ideal {α : Type u} [comm_ring α] (h : ∃! (I : ideal α), I.is_maximal) :

theorem local_of_unique_nonzero_prime (R : Type u) [comm_ring R] (h : ∃! (P : ideal R), P P.is_prime) :

theorem local_of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [local_ring A] [comm_ring B] [nontrivial B] (f : A →+* B) (hf : function.surjective f) :

@[class]
structure is_local_ring_hom {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) :
Prop
• map_nonunit : ∀ (a : α), is_unit (f a)

A local ring homomorphism is a homomorphism between local rings such that the image of the maximal ideal of the source is contained within the maximal ideal of the target.

Instances
@[instance]
def is_local_ring_hom_id (A : Type u_1) [semiring A] :

@[simp]
theorem is_unit_map_iff {A : Type u_1} {B : Type u_2} [semiring A] [semiring B] (f : A →+* B) (a : A) :

@[instance]
def is_local_ring_hom_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [semiring A] [semiring B] [semiring C] (g : B →+* C) (f : A →+* B)  :

@[simp]
theorem is_unit_of_map_unit {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) (a : α) (h : is_unit (f a)) :

theorem of_irreducible_map {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) [h : is_local_ring_hom f] {x : α} (hfx : irreducible (f x)) :

theorem map_nonunit {α : Type u} {β : Type v} [comm_ring α] [local_ring α] [comm_ring β] [local_ring β] (f : α →+* β) (a : α) (h : a ) :

def local_ring.residue_field (α : Type u) [comm_ring α] [local_ring α] :
Type u

The residue field of a local ring is the quotient of the ring by its maximal ideal.

Equations
@[instance]
def local_ring.residue_field.field (α : Type u) [comm_ring α] [local_ring α] :

Equations
@[instance]

Equations
def local_ring.residue (α : Type u) [comm_ring α] [local_ring α] :

The quotient map from a local ring to its residue field.

Equations
def local_ring.residue_field.map {α : Type u} {β : Type v} [comm_ring α] [local_ring α] [comm_ring β] [local_ring β] (f : α →+* β)  :

The map on residue fields induced by a local homomorphism between local rings

Equations
@[instance]
def field.local_ring {α : Type u} [field α] :