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.

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.

theorem Ideal.isMaximal_def {α : Type u} [Semiring α] {I : Ideal α} : I.IsMaximal ↔ IsCoatom I

theorem Ideal.IsMaximal.ne_top {α : Type u} [Semiring α] {I : Ideal α} (h : I.IsMaximal) : I ≠ ⊤

theorem Ideal.isMaximal_iff {α : Type u} [Semiring α] {I : Ideal α} : I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

theorem Ideal.IsMaximal.eq_of_le {α : Type u} [Semiring α] {I J : Ideal α} (hI : I.IsMaximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J

instance Ideal.instIsCoatomic {α : Type u} [Semiring α] : IsCoatomic (Ideal α)

theorem Ideal.IsMaximal.coprime_of_ne {α : Type u} [Semiring α] {M M' : Ideal α} (hM : M.IsMaximal) (hM' : M'.IsMaximal) (hne : M ≠ M') : M ⊔ M' = ⊤

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.

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

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

theorem Ideal.ne_top_iff_exists_maximal {α : Type u} [Semiring α] {I : Ideal α} : I ≠ ⊤ ↔ ∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M

instance Ideal.instNontrivial {α : Type u} [Semiring α] [Nontrivial α] : Nontrivial (Ideal α)

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

theorem Ideal.IsMaximal.exists_inv {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsMaximal) {x : α} (hx : x ∉ I) : ∃ (y : α), ∃ i ∈ I, y * x + i = 1

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

theorem Ideal.span_singleton_prime {α : Type u} [CommSemiring α] {p : α} (hp : p ≠ 0) : (span {p}).IsPrime ↔ Prime p

theorem Ideal.IsMaximal.isPrime {α : Type u} [CommSemiring α] {I : Ideal α} (H : I.IsMaximal) : I.IsPrime

@[instance 100]

instance Ideal.IsMaximal.isPrime' {α : Type u} [CommSemiring α] (I : Ideal α) [_H : I.IsMaximal] : I.IsPrime

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)

theorem Ideal.span_singleton_lt_span_singleton {α : Type u} [CommSemiring α] [IsDomain α] {x y : α} : span {x} < span {y} ↔ DvdNotUnit y x

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

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

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

@[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.

theorem Ideal.isPrime_iff_of_isPrincipalIdealRing {α : Type u} [CommSemiring α] [IsPrincipalIdealRing α] {P : Ideal α} (hP : P ≠ ⊥) : P.IsPrime ↔ ∃ (p : α), Prime p ∧ P = span {p}

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}

theorem Ideal.bot_isMaximal {K : Type u} [DivisionSemiring K] : ⊥.IsMaximal