Prime ideals

This file contains the definition of Ideal.IsPrime for prime ideals.

TODO

Support right ideals, and two-sided ideals over non-commutative rings.

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

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 ∈ I → x ∈ 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} [Semiring α] {I : Ideal α} : I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

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

theorem Ideal.IsPrime.one_notMem {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) : 1 ∉ I

theorem Ideal.one_notMem {α : Type u} [Semiring α] (I : Ideal α) [hI : I.IsPrime] : 1 ∉ I

theorem Ideal.IsPrime.mem_or_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x y : α} : x * y ∈ I → x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.mul_notMem {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x y : α} : x ∉ I → y ∉ I → x * y ∉ I

theorem Ideal.IsPrime.mem_or_mem_of_mul_eq_zero {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.mem_of_pow_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (H : r ^ n ∈ I) : r ∈ I

theorem Ideal.not_isPrime_iff {α : Type u} [Semiring α] {I : Ideal α} : ¬I.IsPrime ↔ I = ⊤ ∨ ∃ (x : α) (_ : x ∉ I) (y : α) (_ : y ∉ I), x * y ∈ I

instance Ideal.isPrime_bot {α : Type u} [Semiring α] [Nontrivial α] [NoZeroDivisors α] : ⊥.IsPrime

@[deprecated Ideal.isPrime_bot (since := "2026-01-10")]

theorem Ideal.bot_prime {α : Type u} [Semiring α] [Nontrivial α] [NoZeroDivisors α] : ⊥.IsPrime

theorem Ideal.IsPrime.mul_mem_iff_mem_or_mem {α : Type u} [Semiring α] {I : Ideal α} [I.IsTwoSided] (hI : I.IsPrime) {x y : α} : x * y ∈ I ↔ x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.pow_mem_iff_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (hn : 0 < n) : r ^ n ∈ I ↔ r ∈ I

theorem Ideal.IsPrime.mul_mem_left_iff {α : Type u} [Semiring α] {I : Ideal α} [I.IsTwoSided] [I.IsPrime] {x y : α} (hx : x ∉ I) : x * y ∈ I ↔ y ∈ I

theorem Ideal.IsPrime.mul_mem_right_iff {α : Type u} [Semiring α] {I : Ideal α} [I.IsTwoSided] [I.IsPrime] {x y : α} (hx : y ∉ I) : x * y ∈ I ↔ x ∈ I

def Ideal.primeCompl {α : Type u} [Semiring α] (P : Ideal α) [hp : P.IsPrime] : Submonoid α

The complement of a prime ideal P ⊆ R is a submonoid of R.

Equations

• P.primeCompl = { carrier := (↑P)ᶜ, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem Ideal.mem_primeCompl_iff {α : Type u} [Semiring α] {P : Ideal α} [P.IsPrime] {x : α} : x ∈ P.primeCompl ↔ x ∉ P

theorem IsDomain.of_bot_isPrime (A : Type u_1) [Ring A] [hbp : ⊥.IsPrime] : IsDomain A

theorem Ideal.eq_bot_of_prime {K : Type u} [DivisionSemiring K] (I : Ideal K) [h : I.IsPrime] : I = ⊥