# Ideals over a ring #

This file contains an assortment of definitions and results for `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.

source
class Ideal.IsMaximal {α : Type u} [Semiring α] (I : Ideal α) :
Prop

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

- out : IsCoatom I

  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

source
theorem Ideal.isMaximal_def {α : Type u} [Semiring α] {I : Ideal α} :
I.IsMaximal ↔ IsCoatom I
source
theorem Ideal.IsMaximal.ne_top {α : Type u} [Semiring α] {I : Ideal α} (h : I.IsMaximal) :
I ≠ ⊤
source
theorem Ideal.isMaximal_iff {α : Type u} [Semiring α] {I : Ideal α} :
I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
source
theorem Ideal.IsMaximal.eq_of_le {α : Type u} [Semiring α] {I J : Ideal α} (hI : I.IsMaximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) :
I = J
source
instance Ideal.instIsCoatomic {α : Type u} [Semiring α] :
IsCoatomic (Ideal α)
source
theorem Ideal.IsMaximal.coprime_of_ne {α : Type u} [Semiring α] {M M' : Ideal α} (hM : M.IsMaximal) (hM' : M'.IsMaximal) (hne : M ≠ M') :
M ⊔ M' = ⊤
source
theorem Ideal.exists_le_maximal {α : Type u} [Semiring α] (I : Ideal α) (hI : I ≠ ⊤) :
∃ (M : Ideal α), 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.

source
theorem Ideal.exists_maximal (α : Type u) [Semiring α] [Nontrivial α] :
∃ (M : Ideal α), M.IsMaximal

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

source
theorem Ideal.ne_top_iff_exists_maximal {α : Type u} [Semiring α] {I : Ideal α} :
I ≠ ⊤ ↔ ∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M
source
instance Ideal.instNontrivial {α : Type u} [Semiring α] [Nontrivial α] :
Nontrivial (Ideal α)
source
theorem Ideal.maximal_of_no_maximal {α : Type u} [Semiring α] {P : Ideal α} (hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal) (J : Ideal α) (hPJ : P < J) :
J = ⊤

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

source
theorem Ideal.IsMaximal.exists_inv {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsMaximal) {x : α} (hx : x ∉ I) :
∃ (y : α), ∃ i ∈ I, y * x + i = 1
source
theorem Ideal.sInf_isPrime_of_isChain {α : Type u} [Semiring α] {s : Set (Ideal α)} (hs : s.Nonempty) (hs' : IsChain (fun (x1 x2 : Ideal α) => x1 ≤ x2) s) (H : ∀ p ∈ s, p.IsPrime) :
(sInf s).IsPrime
source
theorem Ideal.span_singleton_prime {α : Type u} [CommSemiring α] {p : α} (hp : p ≠ 0) :
(span {p}).IsPrime ↔ Prime p
source
theorem Ideal.IsMaximal.isPrime {α : Type u} [CommSemiring α] {I : Ideal α} (H : I.IsMaximal) :
I.IsPrime
source
@[instance 100]
instance Ideal.IsMaximal.isPrime' {α : Type u} [CommSemiring α] (I : Ideal α) [_H : I.IsMaximal] :
I.IsPrime
source
theorem Ideal.exists_disjoint_powers_of_span_eq_top {α : Type u} [CommSemiring α] (s : Set α) (hs : span s = ⊤) (I : Ideal α) (hI : I ≠ ⊤) :
∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
source
theorem Ideal.span_singleton_lt_span_singleton {α : Type u} [CommSemiring α] [IsDomain α] {x y : α} :
span {x} < span {y} ↔ DvdNotUnit y x
source
theorem Ideal.isPrime_of_maximally_disjoint {α : Type u} [CommSemiring α] (I : Ideal α) (S : Submonoid α) (disjoint : Disjoint ↑I ↑S) (maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S) :
I.IsPrime
source
theorem Ideal.exists_le_prime_disjoint {α : Type u} [CommSemiring α] (I : Ideal α) (S : Submonoid α) (disjoint : Disjoint ↑I ↑S) :
∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S
source
theorem Ideal.exists_le_prime_notMem_of_isIdempotentElem {α : Type u} [CommSemiring α] (I : Ideal α) (a : α) (ha : IsIdempotentElem a) (haI : a ∉ I) :
∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ a ∉ p
source
@[deprecated Ideal.exists_le_prime_notMem_of_isIdempotentElem (since := "2025-05-24")]
theorem Ideal.exists_le_prime_nmem_of_isIdempotentElem {α : Type u} [CommSemiring α] (I : Ideal α) (a : α) (ha : IsIdempotentElem a) (haI : a ∉ I) :
∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ a ∉ p

Alias of `Ideal.exists_le_prime_notMem_of_isIdempotentElem`.

source
theorem Ideal.isPrime_iff_of_isPrincipalIdealRing {α : Type u} [CommSemiring α] [IsPrincipalIdealRing α] {P : Ideal α} (hP : P ≠ ⊥) :
P.IsPrime ↔ ∃ (p : α), Prime p ∧ P = span {p}
source
theorem Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors {α : Type u} [CommSemiring α] [IsPrincipalIdealRing α] [NoZeroDivisors α] [Nontrivial α] {P : Ideal α} :
P.IsPrime ↔ P = ⊥ ∨ ∃ (p : α), Prime p ∧ P = span {p}
source
theorem Ideal.bot_isMaximal {K : Type u} [DivisionSemiring K] :
⊥.IsMaximal