# 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, inline]
abbrev 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.

Equations
Instances For
theorem isPrincipalIdealRing_iff (R : Type u) [] :
∀ (S : ),
class IsPrincipalIdealRing (R : Type u) [] :

A ring is a principal ideal ring if all (left) ideals are principal.

• principal : ∀ (S : ),
Instances
theorem IsPrincipalIdealRing.principal {R : Type u} [] [self : ] (S : ) :
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 : ια} :
(ct, f c I)it, 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 : ) :
I 1I
@[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

Equations
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, 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 α} :
xs, x = 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 : S), bI, a * y + b = x
def Ideal.ofRel {α : Type u} [] (r : ααProp) :

The ideal generated by an arbitrary binary relation.

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

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

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

Instances
theorem Ideal.IsPrime.ne_top' {α : Type u} [] {I : } [self : I.IsPrime] :

The prime ideal is not the entire ring.

theorem Ideal.IsPrime.mem_or_mem' {α : Type u} [] {I : } [self : I.IsPrime] {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.

theorem Ideal.isPrime_iff {α : Type u} [] {I : } :
I.IsPrime I ∀ {x y : α}, x * y Ix I y I
theorem Ideal.IsPrime.ne_top {α : Type u} [] {I : } (hI : I.IsPrime) :
theorem Ideal.IsPrime.mem_or_mem {α : Type u} [] {I : } (hI : I.IsPrime) {x : α} {y : α} :
x * y Ix I y I
theorem Ideal.IsPrime.mem_or_mem_of_mul_eq_zero {α : Type u} [] {I : } (hI : I.IsPrime) {x : α} {y : α} (h : x * y = 0) :
x I y I
theorem Ideal.IsPrime.mem_of_pow_mem {α : Type u} [] {I : } (hI : I.IsPrime) {r : α} (n : ) (H : r ^ n I) :
r I
theorem Ideal.not_isPrime_iff {α : Type u} [] {I : } :
¬I.IsPrime I = ∃ (x : α) (_ : xI) (y : α) (_ : yI), x * y I
theorem Ideal.zero_ne_one_of_proper {α : Type u} [] {I : } (h : I ) :
0 1
theorem Ideal.bot_prime {α : Type u} [] [] :
.IsPrime
class Ideal.IsMaximal {α : Type u} [] (I : ) :

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

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

Instances
theorem Ideal.IsMaximal.out {α : Type u} [] {I : } [self : I.IsMaximal] :

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.

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

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

instance Ideal.instNontrivial {α : Type u} [] [] :
Equations
• =
theorem Ideal.maximal_of_no_maximal {α : Type u} [] {P : } (hmax : ∀ (m : ), P < m¬m.IsMaximal) (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 : I.IsMaximal) {x : α} (hx : xI) :
∃ (y : α), iI, 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.

Equations
• I.pi ι = { carrier := {x : ια | ∀ (i : ι), x i I}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
theorem Ideal.mem_pi {α : Type u} [] (I : ) (ι : Type v) (x : ια) :
x I.pi ι ∀ (i : ι), x i I
theorem Ideal.sInf_isPrime_of_isChain {α : Type u} [] {s : Set ()} (hs : s.Nonempty) (hs' : IsChain (fun (x x_1 : ) => x x_1) s) (H : ps, p.IsPrime) :
(sInf s).IsPrime
@[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 : α) :
@[simp]
theorem Ideal.span_singleton_eq_top {α : Type u} [] {x : α} :
theorem Ideal.span_singleton_prime {α : Type u} [] {p : α} (hp : p 0) :
(Ideal.span {p}).IsPrime
theorem Ideal.IsMaximal.isPrime {α : Type u} [] {I : } (H : I.IsMaximal) :
I.IsPrime
@[instance 100]
instance Ideal.IsMaximal.isPrime' {α : Type u} [] (I : ) [_H : I.IsMaximal] :
I.IsPrime
Equations
• =
theorem Ideal.span_singleton_lt_span_singleton {α : Type u} [] [] {x : α} {y : α} :
theorem Ideal.factors_decreasing {α : Type u} [] [] (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.pow_mem_of_pow_mem {α : Type u} {a : α} [] (I : ) {m : } {n : } (ha : a ^ m I) (h : m n) :
a ^ n I
theorem Ideal.add_pow_mem_of_pow_mem_of_le {α : Type u} {a : α} {b : α} [] (I : ) {m : } {n : } {k : } (ha : a ^ m I) (hb : b ^ n I) (hk : m + n k + 1) :
(a + b) ^ k I
theorem Ideal.add_pow_add_pred_mem_of_pow_mem {α : Type u} {a : α} {b : α} [] (I : ) {m : } {n : } (ha : a ^ m I) (hb : b ^ n I) :
(a + b) ^ (m + n - 1) I
theorem Ideal.IsPrime.mul_mem_iff_mem_or_mem {α : Type u} [] {I : } (hI : I.IsPrime) {x : α} {y : α} :
x * y I x I y I
theorem Ideal.IsPrime.pow_mem_iff_mem {α : Type u} [] {I : } (hI : I.IsPrime) {r : α} (n : ) (hn : 0 < n) :
r ^ n I r I
theorem Ideal.pow_multiset_sum_mem_span_pow {α : Type u} [] [] (s : ) (n : ) :
s.sum ^ (Multiset.card s * n + 1) Ideal.span (Multiset.map (fun (x : α) => x ^ (n + 1)) s).toFinset
theorem Ideal.sum_pow_mem_span_pow {α : Type u} [] {ι : Type u_1} (s : ) (f : ια) (n : ) :
(is, f i) ^ (s.card * 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.isPrime_of_maximally_disjoint {α : Type u} [] (I : ) (S : ) (disjoint : Disjoint I S) (maximally_disjoint : ∀ (J : ), I < J¬Disjoint J S) :
I.IsPrime
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.

def Ideal.equivFinTwo (K : Type u) [] [DecidableEq ()] :
Fin 2

A bijection between (left) ideals of a division ring and {0, 1}, sending ⊥ to 0 and ⊤ to 1.

Equations
• = { toFun := fun (I : ) => if I = then 0 else 1, invFun := ![, ], left_inv := , right_inv := }
Instances For
instance Ideal.instFinite {K : Type u} [] :
Equations
• =
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.

Equations
• =
theorem Ideal.eq_bot_of_prime {K : Type u} [] (I : ) [h : I.IsPrime] :
I =
theorem Ideal.bot_isMaximal {K : Type u} [] :
.IsMaximal
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 : R) (_ : x 0), ¬
theorem Ring.not_isField_iff_exists_prime {R : Type u_1} [] [] :
¬ ∃ (p : ), p p.IsPrime

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 : M.IsMaximal) (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 : M.IsMaximal] (non_field : ¬) :
< M
def nonunits (α : Type u) [] :
Set α

The set of non-invertible elements of a monoid.

Equations
• = {a : α | ¬}
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} [] :
1
theorem coe_subset_nonunits {α : Type u} [] {I : } (h : I ) :
I
theorem exists_max_ideal_of_mem_nonunits {α : Type u} {a : α} [] (h : a ) :
∃ (I : ), I.IsMaximal a I