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.ne_top' {α : Type u} : ∀ {inst : Semiring α} {I : Ideal α} [self : I.IsPrime], I ≠ ⊤

The prime ideal is not the entire ring.

theorem Ideal.IsPrime.mem_or_mem' {α : Type u} : ∀ {inst : Semiring α} {I : Ideal α} [self : I.IsPrime] {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.mem_or_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x : α} {y : α} : x * y ∈ I → x ∈ I ∨ 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

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

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

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

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