Mathlib.RingTheory.Ideal.Prime

Ideal.IsPrime structure

(I : Ideal α)

Full source

/-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/
class IsPrime (I : Ideal α) : Prop where
  /-- The prime ideal is not the entire ring. -/
  ne_top' : I ≠ ⊤
  /-- If a product lies in the prime ideal, then at least one element lies in the prime ideal. -/
  mem_or_mem' : ∀ {x y : α}, x * y ∈ I → x ∈ Ix ∈ I ∨ y ∈ I

Prime ideal

Informal description

An ideal $ P $ of a ring $ R $ is called a prime ideal if $ P \neq R $ and for any $ x, y \in R $, the product $ xy \in P $ implies that either $ x \in P $ or $ y \in P $.

Ideal.isPrime_iff theorem

{I : Ideal α} : IsPrime I ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

Full source

theorem isPrime_iff {I : Ideal α} : IsPrimeIsPrime I ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I :=
  ⟨fun h => ⟨h.1, h.2⟩, fun h => ⟨h.1, h.2⟩⟩

Characterization of Prime Ideals in Terms of Multiplicative Closure

Informal description

An ideal $I$ in a ring $\alpha$ is prime if and only if $I$ is not equal to the entire ring (i.e., $I \neq \top$) and for any elements $x, y \in \alpha$, if $x * y \in I$, then either $x \in I$ or $y \in I$.

Ideal.IsPrime.ne_top theorem

{I : Ideal α} (hI : I.IsPrime) : I ≠ ⊤

Full source

theorem IsPrime.ne_top {I : Ideal α} (hI : I.IsPrime) : I ≠ ⊤ :=
  hI.1

Prime Ideal is Proper

Informal description

For any prime ideal $I$ in a ring $\alpha$, $I$ is not equal to the entire ring (i.e., $I \neq \top$).

Ideal.IsPrime.mem_or_mem theorem

{I : Ideal α} (hI : I.IsPrime) {x y : α} : x * y ∈ I → x ∈ I ∨ y ∈ I

Full source

theorem IsPrime.mem_or_mem {I : Ideal α} (hI : I.IsPrime) {x y : α} : x * y ∈ I → x ∈ Ix ∈ I ∨ y ∈ I :=
  hI.2

Prime Ideal Property: $xy \in I \Rightarrow x \in I \lor y \in I$

Informal description

Let $I$ be a prime ideal in a ring $\alpha$. For any elements $x, y \in \alpha$, if the product $x \cdot y$ belongs to $I$, then either $x \in I$ or $y \in I$.

Ideal.IsPrime.mul_not_mem theorem

{I : Ideal α} (hI : I.IsPrime) {x y : α} : x ∉ I → y ∉ I → x * y ∉ I

Full source

theorem IsPrime.mul_not_mem {I : Ideal α} (hI : I.IsPrime) {x y : α} :
    x ∉ I → y ∉ I → x * y ∉ I := fun hx hy h ↦
  hy ((hI.mem_or_mem h).resolve_left hx)

Prime Ideal Property: $x, y \notin I \Rightarrow xy \notin I$

Informal description

Let $I$ be a prime ideal in a ring $\alpha$. For any elements $x, y \in \alpha$, if $x \notin I$ and $y \notin I$, then their product $x \cdot y \notin I$.

Ideal.IsPrime.mem_or_mem_of_mul_eq_zero theorem

{I : Ideal α} (hI : I.IsPrime) {x y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I

Full source

theorem IsPrime.mem_or_mem_of_mul_eq_zero {I : Ideal α} (hI : I.IsPrime) {x y : α} (h : x * y = 0) :
    x ∈ Ix ∈ I ∨ y ∈ I :=
  hI.mem_or_mem (h.symm ▸ I.zero_mem)

Prime Ideal Property for Zero Divisors: $xy = 0 \Rightarrow x \in I \lor y \in I$

Informal description

Let $I$ be a prime ideal in a ring $R$. For any elements $x, y \in R$ such that $x \cdot y = 0$, either $x \in I$ or $y \in I$.

Ideal.IsPrime.mem_of_pow_mem theorem

{I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (H : r ^ n ∈ I) : r ∈ I

Full source

theorem IsPrime.mem_of_pow_mem {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (H : r ^ n ∈ I) :
    r ∈ I := by
  induction n with
  | zero =>
    rw [pow_zero] at H
    exact (mt (eq_top_iff_one _).2 hI.1).elim H
  | succ n ih =>
    rw [pow_succ] at H
    exact Or.casesOn (hI.mem_or_mem H) ih id

Prime Ideal Property: $r^n \in I \Rightarrow r \in I$

Informal description

Let $I$ be a prime ideal in a ring $\alpha$. For any element $r \in \alpha$ and natural number $n$, if $r^n \in I$, then $r \in I$.

Ideal.not_isPrime_iff theorem

{I : Ideal α} : ¬I.IsPrime ↔ I = ⊤ ∨ ∃ (x : α) (_hx : x ∉ I) (y : α) (_hy : y ∉ I), x * y ∈ I

Full source

theorem not_isPrime_iff {I : Ideal α} :
    ¬I.IsPrime¬I.IsPrime ↔ I = ⊤ ∨ ∃ (x : α) (_hx : x ∉ I) (y : α) (_hy : y ∉ I), x * y ∈ I := by
  simp_rw [Ideal.isPrime_iff, not_and_or, Ne, Classical.not_not, not_forall, not_or]
  exact
    or_congr Iff.rfl
      ⟨fun ⟨x, y, hxy, hx, hy⟩ => ⟨x, hx, y, hy, hxy⟩, fun ⟨x, hx, y, hy, hxy⟩ =>
        ⟨x, y, hxy, hx, hy⟩⟩

Characterization of Non-Prime Ideals

Informal description

An ideal $I$ of a ring $\alpha$ is not prime if and only if either $I$ is the entire ring, or there exist elements $x, y \notin I$ such that their product $x * y$ is in $I$.

Ideal.bot_prime theorem

[Nontrivial α] [NoZeroDivisors α] : (⊥ : Ideal α).IsPrime

Full source

theorem bot_prime [Nontrivial α] [NoZeroDivisors α] : (⊥ : Ideal α).IsPrime :=
  ⟨fun h => one_ne_zero (α := α) (by rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h), fun h =>
    mul_eq_zero.mp (by simpa only [Submodule.mem_bot] using h)⟩

Zero Ideal is Prime in Nontrivial Ring Without Zero Divisors

Informal description

In a nontrivial ring $\alpha$ with no zero divisors, the zero ideal $(0)$ is a prime ideal.

Ideal.IsPrime.mul_mem_iff_mem_or_mem theorem

{I : Ideal α} [I.IsTwoSided] (hI : I.IsPrime) : ∀ {x y : α}, x * y ∈ I ↔ x ∈ I ∨ y ∈ I

Full source

theorem IsPrime.mul_mem_iff_mem_or_mem {I : Ideal α} [I.IsTwoSided] (hI : I.IsPrime) :
    ∀ {x y : α}, x * y ∈ Ix * y ∈ I ↔ x ∈ I ∨ y ∈ I := @fun x y =>
  ⟨hI.mem_or_mem, by
    rintro (h | h)
    exacts [I.mul_mem_right y h, I.mul_mem_left x h]⟩

Prime Ideal Characterization: $xy \in I \leftrightarrow x \in I \lor y \in I$

Informal description

Let $I$ be a two-sided prime ideal in a ring $\alpha$. For any elements $x, y \in \alpha$, the product $x \cdot y$ belongs to $I$ if and only if either $x \in I$ or $y \in I$.

Ideal.IsPrime.pow_mem_iff_mem theorem

{I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (hn : 0 < n) : r ^ n ∈ I ↔ r ∈ I

Full source

theorem IsPrime.pow_mem_iff_mem {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (hn : 0 < n) :
    r ^ n ∈ Ir ^ n ∈ I ↔ r ∈ I :=
  ⟨hI.mem_of_pow_mem n, fun hr => I.pow_mem_of_mem hr n hn⟩

Prime Ideal Power Membership Criterion: $r^n \in I \leftrightarrow r \in I$ for $n > 0$

Informal description

Let $I$ be a prime ideal in a ring $\alpha$. For any element $r \in \alpha$ and positive integer $n$, the $n$-th power $r^n$ belongs to $I$ if and only if $r$ belongs to $I$.

Ideal.primeCompl definition

(P : Ideal α) [hp : P.IsPrime] : Submonoid α

Full source

/-- The complement of a prime ideal `P ⊆ R` is a submonoid of `R`. -/
def primeCompl (P : Ideal α) [hp : P.IsPrime] : Submonoid α where
  carrier := (Pᶜ : Set α)
  one_mem' := by convert P.ne_top_iff_one.1 hp.1
  mul_mem' {_ _} hnx hny hxy := Or.casesOn (hp.mem_or_mem hxy) hnx hny

Complement of a prime ideal as a submonoid

Informal description

Given a prime ideal $ P $ of a ring $ \alpha $, the complement $ P^c $ forms a submonoid of $ \alpha $. Specifically: - The multiplicative identity $ 1 $ is in $ P^c $ (since $ P \neq \alpha $), - For any $ x, y \in P^c $, their product $ xy $ is also in $ P^c $ (by the prime ideal property).

IsDomain.of_bot_isPrime theorem

(A : Type*) [Ring A] [hbp : (⊥ : Ideal A).IsPrime] : IsDomain A

Full source

theorem IsDomain.of_bot_isPrime (A : Type*) [Ring A] [hbp : (⊥ : Ideal A).IsPrime] : IsDomain A :=
  @NoZeroDivisors.to_isDomain A _
    ⟨1, 0, fun h => hbp.ne_top ((Ideal.eq_top_iff_one ⊥).mpr h)⟩ ⟨fun h => hbp.2 h⟩

Prime Zero Ideal Implies Integral Domain

Informal description

Let $A$ be a ring. If the zero ideal $(0)$ is a prime ideal in $A$, then $A$ is an integral domain.

TODO