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.notMem_of_isUnit {α : Type u} [Semiring α] (I : Ideal α) [I.IsPrime] {x : α} (hx : IsUnit x) : x ∉ 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

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 Ideal.primeCompl_bot {α : Type u} [Semiring α] [Nontrivial α] [NoZeroDivisors α] : ⊥.primeCompl = nonZeroDivisors α

def Ideal.sInfPrimeCompl {α : Type u} [Semiring α] (S : Set (Ideal α)) (hS : ∀ P ∈ S, P.IsPrime) : Submonoid α

The elements lying outside every ideal in a set of prime ideals form a submonoid.

Equations

• Ideal.sInfPrimeCompl S hS = ⨅ (P : Ideal α), ⨅ (h : P ∈ S), P.primeCompl

theorem Ideal.sInfPrimeCompl_def {α : Type u} [Semiring α] (S : Set (Ideal α)) (hS : ∀ P ∈ S, P.IsPrime) : sInfPrimeCompl S hS = ⨅ (P : Ideal α), ⨅ (h : P ∈ S), P.primeCompl

@[simp]

theorem Ideal.mem_sInfPrimeCompl_iff {α : Type u} [Semiring α] (S : Set (Ideal α)) (hS : ∀ P ∈ S, P.IsPrime) {x : α} : x ∈ sInfPrimeCompl S hS ↔ ∀ P ∈ S, x ∉ P

@[simp]

theorem Ideal.sInfPrimeCompl_empty {α : Type u} [Semiring α] : sInfPrimeCompl ∅ ⋯ = ⊤

@[simp]

theorem Ideal.sInfPrimeCompl_singleton {α : Type u} [Semiring α] (P : Ideal α) [P.IsPrime] : sInfPrimeCompl {P} ⋯ = P.primeCompl

theorem Ideal.sInfPrimeCompl_union {α : Type u} [Semiring α] {S T : Set (Ideal α)} (hST : ∀ P ∈ S ∪ T, P.IsPrime) : sInfPrimeCompl (S ∪ T) hST = sInfPrimeCompl S ⋯ ⊓ sInfPrimeCompl T ⋯

theorem Ideal.sInfPrimeCompl_le_primeCompl {α : Type u} [Semiring α] (S : Set (Ideal α)) (hS : ∀ P ∈ S, P.IsPrime) {P : Ideal α} (hP : P ∈ S) : sInfPrimeCompl S hS ≤ P.primeCompl

theorem Ideal.sInfPrimeCompl_anti {α : Type u} [Semiring α] {S T : Set (Ideal α)} (hST : S ⊆ T) (hP : ∀ P ∈ T, P.IsPrime) : sInfPrimeCompl T hP ≤ sInfPrimeCompl S ⋯

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 = ⊥