# Documentation

Mathlib.RingTheory.Ideal.Basic

# Ideals over a ring #

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) [] :

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.

Instances For
theorem Ideal.zero_mem {α : Type u} [] (I : ) :
0 I
theorem Ideal.add_mem {α : Type u} [] (I : ) {a : α} {b : α} :
a Ib Ia + b I
theorem Ideal.mul_mem_left {α : Type u} [] (I : ) (a : α) {b : α} :
b Ia * b I
theorem Ideal.ext {α : Type u} [] {I : } {J : } (h : ∀ (x : α), x I x J) :
I = J
theorem Ideal.sum_mem {α : Type u} [] (I : ) {ι : Type u_1} {t : } {f : ια} :
(∀ (c : ι), c tf c I) → (Finset.sum t fun i => f i) I
theorem Ideal.eq_top_of_unit_mem {α : Type u} [] (I : ) (x : α) (y : α) (hx : x I) (h : y * x = 1) :
I =
theorem Ideal.eq_top_of_isUnit_mem {α : Type u} [] (I : ) {x : α} (hx : x I) (h : ) :
I =
theorem Ideal.eq_top_iff_one {α : Type u} [] (I : ) :
I = 1 I
theorem Ideal.ne_top_iff_one {α : Type u} [] (I : ) :
@[simp]
theorem Ideal.unit_mul_mem_iff_mem {α : Type u} [] (I : ) {x : α} {y : α} (hy : ) :
y * x I x I
def Ideal.span {α : Type u} [] (s : Set α) :

The ideal generated by a subset of a ring

Instances For
@[simp]
theorem Ideal.submodule_span_eq {α : Type u} [] {s : Set α} :
@[simp]
theorem Ideal.span_empty {α : Type u} [] :
@[simp]
theorem Ideal.span_univ {α : Type u} [] :
Ideal.span Set.univ =
theorem Ideal.span_union {α : Type u} [] (s : Set α) (t : Set α) :
theorem Ideal.span_iUnion {α : Type u} [] {ι : Sort u_1} (s : ιSet α) :
Ideal.span (⋃ (i : ι), s i) = ⨆ (i : ι), Ideal.span (s i)
theorem Ideal.mem_span {α : Type u} [] {s : Set α} (x : α) :
x ∀ (p : ), s px p
theorem Ideal.subset_span {α : Type u} [] {s : Set α} :
s ↑()
theorem Ideal.span_le {α : Type u} [] {s : Set α} {I : } :
I s I
theorem Ideal.span_mono {α : Type u} [] {s : Set α} {t : Set α} :
s t
@[simp]
theorem Ideal.span_eq {α : Type u} [] (I : ) :
= I
@[simp]
theorem Ideal.span_singleton_one {α : Type u} [] :
theorem Ideal.mem_span_insert {α : Type u} [] {s : Set α} {x : α} {y : α} :
x Ideal.span (insert y s) a z, z x = a * y + z
theorem Ideal.mem_span_singleton' {α : Type u} [] {x : α} {y : α} :
x Ideal.span {y} a, a * y = x
theorem Ideal.span_singleton_le_iff_mem {α : Type u} [] (I : ) {x : α} :
Ideal.span {x} I x I
theorem Ideal.span_singleton_mul_left_unit {α : Type u} [] {a : α} (h2 : ) (x : α) :
theorem Ideal.span_insert {α : Type u} [] (x : α) (s : Set α) :
theorem Ideal.span_eq_bot {α : Type u} [] {s : Set α} :
∀ (x : α), x sx = 0
@[simp]
theorem Ideal.span_singleton_eq_bot {α : Type u} [] {x : α} :
Ideal.span {x} = x = 0
theorem Ideal.span_singleton_ne_top {α : Type u_1} [] {x : α} (hx : ¬) :
@[simp]
theorem Ideal.span_zero {α : Type u} [] :
@[simp]
theorem Ideal.span_one {α : Type u} [] :
theorem Ideal.span_eq_top_iff_finite {α : Type u} [] (s : Set α) :
s', s' s Ideal.span s' =
theorem Ideal.mem_span_singleton_sup {S : Type u_1} [] {x : S} {y : S} {I : } :
x Ideal.span {y} I a b, b I a * y + b = x
def Ideal.ofRel {α : Type u} [] (r : ααProp) :

The ideal generated by an arbitrary binary relation.

Instances For
class Ideal.IsPrime {α : Type u} [] (I : ) :
• ne_top' : I

The prime ideal is not the entire ring.

• mem_or_mem' : ∀ {x y : α}, x * y Ix I y I

If a product lies in the prime ideal, then at least one element lies in the prime ideal.

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

Instances
theorem Ideal.isPrime_iff {α : Type u} [] {I : } :
I ∀ {x y : α}, x * y Ix I y I
theorem Ideal.IsPrime.ne_top {α : Type u} [] {I : } (hI : ) :
theorem Ideal.IsPrime.mem_or_mem {α : Type u} [] {I : } (hI : ) {x : α} {y : α} :
x * y Ix I y I
theorem Ideal.IsPrime.mem_or_mem_of_mul_eq_zero {α : Type u} [] {I : } (hI : ) {x : α} {y : α} (h : x * y = 0) :
x I y I
theorem Ideal.IsPrime.mem_of_pow_mem {α : Type u} [] {I : } (hI : ) {r : α} (n : ) (H : r ^ n I) :
r I
theorem Ideal.not_isPrime_iff {α : Type u} [] {I : } :
I = x _hx y _hy, x * y I
theorem Ideal.zero_ne_one_of_proper {α : Type u} [] {I : } (h : I ) :
0 1
theorem Ideal.bot_prime {R : Type u_1} [Ring R] [] :
class Ideal.IsMaximal {α : Type u} [] (I : ) :
• out :

The maximal ideal is a coatom in the ordering on ideals; that is, it is not the entire ring, and there are no other proper ideals strictly containing it.

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

Instances
theorem Ideal.isMaximal_def {α : Type u} [] {I : } :
theorem Ideal.IsMaximal.ne_top {α : Type u} [] {I : } (h : ) :
theorem Ideal.isMaximal_iff {α : Type u} [] {I : } :
¬1 I ∀ (J : ) (x : α), I J¬x Ix J1 J
theorem Ideal.IsMaximal.eq_of_le {α : Type u} [] {I : } {J : } (hI : ) (hJ : J ) (IJ : I J) :
I = J
theorem Ideal.IsMaximal.coprime_of_ne {α : Type u} [] {M : } {M' : } (hM : ) (hM' : ) (hne : M M') :
M M' =
theorem Ideal.exists_le_maximal {α : Type u} [] (I : ) (hI : I ) :
M, 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) [] [] :
M,

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

instance Ideal.instNontrivialIdeal {α : Type u} [] [] :
theorem Ideal.maximal_of_no_maximal {R : Type u} [] {P : } (hmax : ∀ (m : ), P < m) (J : ) (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} [] {x : α} {y : α} :
Ideal.span {x, y} = Ideal.span {y, x}
theorem Ideal.mem_span_pair {α : Type u} [] {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} [] {x : R} {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} [] {x : R} {y : R} (z : R) :
Ideal.span {x, y + x * z} = Ideal.span {x, y}
theorem Ideal.IsMaximal.exists_inv {α : Type u} [] {I : } (hI : ) {x : α} (hx : ¬x I) :
y i, i I y * x + i = 1
theorem Ideal.mem_sup_left {R : Type u} [] {S : } {T : } {x : R} :
x Sx S T
theorem Ideal.mem_sup_right {R : Type u} [] {S : } {T : } {x : R} :
x Tx S T
theorem Ideal.mem_iSup_of_mem {R : Type u} [] {ι : Sort u_1} {S : ι} (i : ι) {x : R} :
x S ix iSup S
theorem Ideal.mem_sSup_of_mem {R : Type u} [] {S : Set ()} {s : } (hs : s S) {x : R} :
x sx sSup S
theorem Ideal.mem_sInf {R : Type u} [] {s : Set ()} {x : R} :
x sInf s ∀ ⦃I : ⦄, I sx I
@[simp]
theorem Ideal.mem_inf {R : Type u} [] {I : } {J : } {x : R} :
x I J x I x J
@[simp]
theorem Ideal.mem_iInf {R : Type u} [] {ι : Sort u_1} {I : ι} {x : R} :
x iInf I ∀ (i : ι), x I i
@[simp]
theorem Ideal.mem_bot {R : Type u} [] {x : R} :
x x = 0
def Ideal.pi {α : Type u} [] (I : ) (ι : Type v) :
Ideal (ια)

I^n as an ideal of R^n.

Instances For
theorem Ideal.mem_pi {α : Type u} [] (I : ) (ι : Type v) (x : ια) :
x Ideal.pi I ι ∀ (i : ι), x i I
theorem Ideal.sInf_isPrime_of_isChain {α : Type u} [] {s : Set ()} (hs : ) (hs' : IsChain (fun x x_1 => x x_1) s) (H : ∀ (p : ), p s) :
@[simp]
theorem Ideal.mul_unit_mem_iff_mem {α : Type u} [] (I : ) {x : α} {y : α} (hy : ) :
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} [] [] {x : α} {y : α} :
theorem Ideal.span_singleton_mul_right_unit {α : Type u} [] {a : α} (h2 : ) (x : α) :
theorem Ideal.span_singleton_eq_top {α : Type u} [] {x : α} :
theorem Ideal.span_singleton_prime {α : Type u} [] {p : α} (hp : p 0) :
theorem Ideal.IsMaximal.isPrime {α : Type u} [] {I : } (H : ) :
instance Ideal.IsMaximal.isPrime' {α : Type u} [] (I : ) [_H : ] :
theorem Ideal.span_singleton_lt_span_singleton {β : Type v} [] [] {x : β} {y : β} :
theorem Ideal.factors_decreasing {β : Type v} [] [] (b₁ : β) (b₂ : β) (h₁ : b₁ 0) (h₂ : ¬IsUnit b₂) :
Ideal.span {b₁ * b₂} < Ideal.span {b₁}
theorem Ideal.mul_mem_right {α : Type u} {a : α} (b : α) [] (I : ) (h : a I) :
a * b I
theorem Ideal.pow_mem_of_mem {α : Type u} {a : α} [] (I : ) (ha : a I) (n : ) (hn : 0 < n) :
a ^ n I
theorem Ideal.IsPrime.mul_mem_iff_mem_or_mem {α : Type u} [] {I : } (hI : ) {x : α} {y : α} :
x * y I x I y I
theorem Ideal.IsPrime.pow_mem_iff_mem {α : Type u} [] {I : } (hI : ) {r : α} (n : ) (hn : 0 < n) :
r ^ n I r I
theorem Ideal.pow_multiset_sum_mem_span_pow {α : Type u} [] [] (s : ) (n : ) :
^ (Multiset.card s * n + 1) Ideal.span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
theorem Ideal.sum_pow_mem_span_pow {α : Type u} [] {ι : Type u_1} (s : ) (f : ια) (n : ) :
(Finset.sum s fun i => f i) ^ ( * n + 1) Ideal.span ((fun i => f i ^ (n + 1)) '' s)
theorem Ideal.span_pow_eq_top {α : Type u} [] (s : Set α) (hs : ) (n : ) :
Ideal.span ((fun x => x ^ n) '' s) =
theorem Ideal.neg_mem_iff {α : Type u} [Ring α] (I : ) {a : α} :
-a I a I
theorem Ideal.add_mem_iff_left {α : Type u} [Ring α] (I : ) {a : α} {b : α} :
b I → (a + b I a I)
theorem Ideal.add_mem_iff_right {α : Type u} [Ring α] (I : ) {a : α} {b : α} :
a I → (a + b I b I)
theorem Ideal.sub_mem {α : Type u} [Ring α] (I : ) {a : α} {b : α} :
a Ib Ia - b I
theorem Ideal.mem_span_insert' {α : Type u} [Ring α] {s : Set α} {x : α} {y : α} :
x Ideal.span (insert y s) a, x + a * y
@[simp]
theorem Ideal.span_singleton_neg {α : Type u} [Ring α] (x : α) :
theorem Ideal.eq_bot_or_top {K : Type u} [] (I : ) :
I = I =

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

instance Ideal.isSimpleOrder {K : Type u} [] :

Ideals of a DivisionSemiring are a simple order. Thanks to the way abbreviations work, this automatically gives an IsSimpleModule K instance.

theorem Ideal.eq_bot_of_prime {K : Type u} [] (I : ) [h : ] :
I =
theorem Ideal.bot_isMaximal {K : Type u} [] :
theorem Ideal.mul_sub_mul_mem {R : Type u_1} [] (I : ) {a : R} {b : R} {c : R} {d : R} (h1 : a - b I) (h2 : c - d I) :
a * c - b * d I
theorem Ring.exists_not_isUnit_of_not_isField {R : Type u_1} [] [] (hf : ¬) :
x _hx, ¬
theorem Ring.not_isField_iff_exists_prime {R : Type u_1} [] [] :
¬ p, p

Also see Ideal.isSimpleOrder 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_isMaximal_of_not_isField {R : Type u_1} [] [] {M : } (max : ) (not_field : ¬) :

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

theorem Ideal.bot_lt_of_maximal {R : Type u} [] [] (M : ) [hm : ] (non_field : ¬) :
< M
def nonunits (α : Type u) [] :
Set α

The set of non-invertible elements of a monoid.

Instances For
@[simp]
theorem mem_nonunits_iff {α : Type u} {a : α} [] :
theorem mul_mem_nonunits_right {α : Type u} {a : α} {b : α} [] :
b a * b
theorem mul_mem_nonunits_left {α : Type u} {a : α} {b : α} [] :
a a * b
theorem zero_mem_nonunits {α : Type u} [] :
0 0 1
@[simp]
theorem one_not_mem_nonunits {α : Type u} [] :
theorem coe_subset_nonunits {α : Type u} [] {I : } (h : I ) :
I
theorem exists_max_ideal_of_mem_nonunits {α : Type u} {a : α} [] (h : a ) :
I, a I