doc-next-gen

Mathlib.RingTheory.Ideal.Maximal

Module docstring

{"# 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. "}

Ideal.IsMaximal structure
(I : Ideal α)
Full source 
/-- An ideal is maximal if it is maximal in the collection of proper ideals. -/
class IsMaximal (I : Ideal α) : Prop where
  /-- 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. -/
  out : IsCoatom I
Maximal ideal of a ring
Informal description
An ideal $I$ of a ring $\alpha$ is called maximal if it is a proper ideal (i.e., $I \neq \alpha$) and there is no other proper ideal strictly containing $I$.
Ideal.isMaximal_def theorem
{I : Ideal α} : I.IsMaximal ↔ IsCoatom I
Full source 
theorem isMaximal_def {I : Ideal α} : I.IsMaximal ↔ IsCoatom I :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩
Maximal Ideal iff Coatom in Ideal Lattice
Informal description
An ideal $I$ of a ring $\alpha$ is maximal if and only if $I$ is a coatom in the lattice of ideals of $\alpha$, i.e., $I \neq \top$ and for any ideal $J$, if $I < J$ then $J = \top$.
Ideal.IsMaximal.ne_top theorem
{I : Ideal α} (h : I.IsMaximal) : I ≠ ⊤
Full source 
theorem IsMaximal.ne_top {I : Ideal α} (h : I.IsMaximal) : I ≠ ⊤ :=
  (isMaximal_def.1 h).1
Maximal ideals are proper
Informal description
For any maximal ideal $I$ of a ring $\alpha$, $I$ is not equal to the entire ring $\alpha$.
Ideal.isMaximal_iff theorem
{I : Ideal α} : I.IsMaximal ↔ (1 : α) ∉ I ∧ ∀ (J : Ideal α) (x), I ≤ J → x ∉ I → x ∈ J → (1 : α) ∈ J
Full source 
theorem isMaximal_iff {I : Ideal α} :
    I.IsMaximal ↔ (1 : α) ∉ I ∧ ∀ (J : Ideal α) (x), I ≤ J → x ∉ I → x ∈ J → (1 : α) ∈ J := by
  simp_rw [isMaximal_def, SetLike.isCoatom_iff, Ideal.ne_top_iff_one, ← Ideal.eq_top_iff_one]
Characterization of Maximal Ideals in Terms of Unit Inclusion
Informal description
An ideal $I$ of a ring $\alpha$ is maximal if and only if the following two conditions hold: 1. The multiplicative identity $1$ is not in $I$. 2. For any ideal $J$ and any element $x \in \alpha$, if $I \subseteq J$ and $x \notin I$ but $x \in J$, then $1 \in J$.
Ideal.IsMaximal.coprime_of_ne theorem
{M M' : Ideal α} (hM : M.IsMaximal) (hM' : M'.IsMaximal) (hne : M ≠ M') : M ⊔ M' = ⊤
Full source 
theorem IsMaximal.coprime_of_ne {M M' : Ideal α} (hM : M.IsMaximal) (hM' : M'.IsMaximal)
    (hne : M ≠ M') : M ⊔ M' = ⊤ := by
  contrapose! hne with h
  exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)
Sum of Distinct Maximal Ideals is the Whole Ring
Informal description
For any two distinct maximal ideals $M$ and $M'$ of a ring $\alpha$, their supremum $M \sqcup M'$ is equal to the entire ring $\alpha$, i.e., $M + M' = \alpha$.
Ideal.exists_le_maximal theorem
(I : Ideal α) (hI : I ≠ ⊤) : ∃ M : Ideal α, M.IsMaximal ∧ I ≤ M
Full source 
/-- **Krull's theorem**: if `I` is an ideal that is not the whole ring, then it is included in some
    maximal ideal. -/
theorem exists_le_maximal (I : Ideal α) (hI : I ≠ ⊤) : ∃ M : Ideal α, M.IsMaximal ∧ I ≤ M :=
  let ⟨m, hm⟩ := (eq_top_or_exists_le_coatom I).resolve_left hI
  ⟨m, ⟨⟨hm.1⟩, hm.2⟩⟩
Krull's Theorem on Existence of Maximal Ideals Containing Proper Ideals
Informal description
For any proper ideal $I$ of a ring $\alpha$ (i.e., $I \neq \alpha$), there exists a maximal ideal $M$ of $\alpha$ such that $I \subseteq M$.
Ideal.instNontrivial instance
[Nontrivial α] : Nontrivial (Ideal α)
Full source 
instance [Nontrivial α] : Nontrivial (Ideal α) := by
  rcases@exists_maximal α _ _ with ⟨M, hM, _⟩
  exact nontrivial_of_ne M ⊤ hM
Nontriviality of the Ideal Lattice in Nontrivial Rings
Informal description
For any nontrivial ring $\alpha$, the type of ideals of $\alpha$ is also nontrivial.
Ideal.maximal_of_no_maximal theorem
{P : Ideal α} (hmax : ∀ m : Ideal α, P < m → ¬IsMaximal m) (J : Ideal α) (hPJ : P < J) : J = ⊤
Full source 
/-- If P is not properly contained in any maximal ideal then it is not properly contained
  in any proper ideal -/
theorem maximal_of_no_maximal {P : Ideal α}
    (hmax : ∀ m : Ideal α, P < m → ¬IsMaximal m) (J : Ideal α) (hPJ : P < J) : J = ⊤ := by
  by_contra hnonmax
  rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩
  exact hmax M (lt_of_lt_of_le hPJ hM2) hM1
Characterization of Ideals Not Contained in Any Maximal Ideal
Informal description
Let $P$ be an ideal in a ring $\alpha$ such that $P$ is not properly contained in any maximal ideal. Then for any ideal $J$ properly containing $P$, we have $J = \alpha$.
Ideal.IsMaximal.exists_inv theorem
{I : Ideal α} (hI : I.IsMaximal) {x} (hx : x ∉ I) : ∃ y, ∃ i ∈ I, y * x + i = 1
Full source 
theorem IsMaximal.exists_inv {I : Ideal α} (hI : I.IsMaximal) {x} (hx : x ∉ I) :
    ∃ y, ∃ i ∈ I, y * x + i = 1 := by
  obtain ⟨H₁, H₂⟩ := isMaximal_iff.1 hI
  rcases mem_span_insert.1
      (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx
        (subset_span (mem_insert _ _))) with
    ⟨y, z, hz, hy⟩
  refine ⟨y, z, ?_, hy.symm⟩
  rwa [← span_eq I]
Existence of Multiplicative Inverse Modulo a Maximal Ideal
Informal description
Let $I$ be a maximal ideal in a ring $\alpha$ and let $x \in \alpha$ be an element not in $I$. Then there exists an element $y \in \alpha$ and an element $i \in I$ such that $y \cdot x + i = 1$.
Ideal.sInf_isPrime_of_isChain theorem
{s : Set (Ideal α)} (hs : s.Nonempty) (hs' : IsChain (· ≤ ·) s) (H : ∀ p ∈ s, p.IsPrime) : (sInf s).IsPrime
Full source 
theorem sInf_isPrime_of_isChain {s : Set (Ideal α)} (hs : s.Nonempty) (hs' : IsChain (· ≤ ·) s)
    (H : ∀ p ∈ s, p.IsPrime) : (sInf s).IsPrime :=
  ⟨fun e =>
    let ⟨x, hx⟩ := hs
    (H x hx).ne_top (eq_top_iff.mpr (e.symm.trans_le (sInf_le hx))),
    fun e =>
    or_iff_not_imp_left.mpr fun hx => by
      rw [Ideal.mem_sInf] at hx e ⊢
      push_neg at hx
      obtain ⟨I, hI, hI'⟩ := hx
      intro J hJ
      rcases hs'.total hI hJ with h | h
      · exact h (((H I hI).mem_or_mem (e hI)).resolve_left hI')
      · exact ((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x⟩
Intersection of a Chain of Prime Ideals is Prime
Informal description
Let $s$ be a nonempty chain of ideals in a commutative ring $\alpha$ with respect to the inclusion relation $\leq$, and suppose every ideal in $s$ is prime. Then the intersection $\bigcap s$ is also a prime ideal.
Ideal.span_singleton_prime theorem
{p : α} (hp : p ≠ 0) : IsPrime (span ({ p } : Set α)) ↔ Prime p
Full source 
theorem span_singleton_prime {p : α} (hp : p ≠ 0) : IsPrimeIsPrime (span ({p} : Set α)) ↔ Prime p := by
  simp [isPrime_iff, Prime, span_singleton_eq_top, hp, mem_span_singleton]
Principal Ideal Generated by a Nonzero Element is Prime if and only if the Element is Prime
Informal description
For a nonzero element $p$ in a commutative ring $\alpha$, the principal ideal generated by $\{p\}$ is prime if and only if $p$ is a prime element. That is, $\text{span}(\{p\})$ is a prime ideal if and only if $p$ is a prime element in $\alpha$.
Ideal.IsMaximal.isPrime theorem
{I : Ideal α} (H : I.IsMaximal) : I.IsPrime
Full source 
theorem IsMaximal.isPrime {I : Ideal α} (H : I.IsMaximal) : I.IsPrime :=
  ⟨H.1.1, @fun x y hxy =>
    or_iff_not_imp_left.2 fun hx => by
      let J : Ideal α := Submodule.span α (insert x ↑I)
      have IJ : I ≤ J := Set.Subset.trans (subset_insert _ _) subset_span
      have xJ : x ∈ J := Ideal.subset_span (Set.mem_insert x I)
      obtain ⟨_, oJ⟩ := isMaximal_iff.1 H
      specialize oJ J x IJ hx xJ
      rcases Submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩
      obtain F : y * 1 = y * (a • x + b) := congr_arg (fun g : α => y * g) oe
      rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc]
      refine Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y ?_)
      rwa [Submodule.span_eq] at h⟩
Maximal ideals are prime
Informal description
Let $I$ be a maximal ideal of a commutative ring $\alpha$. Then $I$ is a prime ideal.
Ideal.IsMaximal.isPrime' instance
(I : Ideal α) : ∀ [_H : I.IsMaximal], I.IsPrime
Full source 
instance (priority := 100) IsMaximal.isPrime' (I : Ideal α) : ∀ [_H : I.IsMaximal], I.IsPrime :=
  @IsMaximal.isPrime _ _ _
Maximal Ideals are Prime
Informal description
For any maximal ideal $I$ of a commutative ring $\alpha$, $I$ is a prime ideal.
Ideal.exists_disjoint_powers_of_span_eq_top theorem
(s : Set α) (hs : span s = ⊤) (I : Ideal α) (hI : I ≠ ⊤) : ∃ r ∈ s, Disjoint (I : Set α) (Submonoid.powers r)
Full source 
theorem exists_disjoint_powers_of_span_eq_top (s : Set α) (hs : span s = ⊤) (I : Ideal α)
    (hI : I ≠ ⊤) : ∃ r ∈ s, Disjoint (I : Set α) (Submonoid.powers r) := by
  have ⟨M, hM, le⟩ := exists_le_maximal I hI
  have := hM.1.1
  rw [Ne, eq_top_iff, ← hs, span_le, Set.not_subset] at this
  have ⟨a, has, haM⟩ := this
  exact ⟨a, has, Set.disjoint_left.mpr fun x hx ⟨n, hn⟩ ↦
    haM (hM.isPrime.mem_of_pow_mem _ (le <| hn ▸ hx))⟩
Existence of Disjoint Element from Proper Ideal in Generating Set
Informal description
Let $s$ be a subset of a commutative ring $\alpha$ such that the ideal generated by $s$ is the entire ring (i.e., $\text{span}(s) = \alpha$). For any proper ideal $I$ of $\alpha$ (i.e., $I \neq \alpha$), there exists an element $r \in s$ such that the set $I$ is disjoint from the submonoid generated by $r$ (i.e., $I \cap \{r^k \mid k \in \mathbb{N}\} = \emptyset$).
Ideal.span_singleton_lt_span_singleton theorem
[IsDomain α] {x y : α} : span ({ x } : Set α) < span ({ y } : Set α) ↔ DvdNotUnit y x
Full source 
theorem span_singleton_lt_span_singleton [IsDomain α] {x y : α} :
    spanspan ({x} : Set α) < span ({y} : Set α) ↔ DvdNotUnit y x := by
  rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
    dvd_and_not_dvd_iff]
Strict Inclusion of Principal Ideals in an Integral Domain is Equivalent to Non-Unit Divisibility
Informal description
Let $\alpha$ be an integral domain. For any two elements $x, y \in \alpha$, the principal ideal generated by $x$ is strictly contained in the principal ideal generated by $y$ if and only if $y$ divides $x$ but is not a unit (i.e., $y$ is a non-unit divisor of $x$).
Ideal.isPrime_of_maximally_disjoint theorem
(I : Ideal α) (S : Submonoid α) (disjoint : Disjoint (I : Set α) S) (maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (J : Set α) S) : I.IsPrime
Full source 
lemma isPrime_of_maximally_disjoint (I : Ideal α)
    (S : Submonoid α)
    (disjoint : Disjoint (I : Set α) S)
    (maximally_disjoint : ∀ (J : Ideal α), I < J → ¬ Disjoint (J : Set α) S) :
    I.IsPrime where
  ne_top' := by
    rintro rfl
    have : 1 ∈ (S : Set α) := S.one_mem
    aesop
  mem_or_mem' {x y} hxy := by
    by_contra! rid
    have hx := maximally_disjoint (I ⊔ span {x}) (Submodule.lt_sup_iff_not_mem.mpr rid.1)
    have hy := maximally_disjoint (I ⊔ span {y}) (Submodule.lt_sup_iff_not_mem.mpr rid.2)
    simp only [Set.not_disjoint_iff, mem_inter_iff, SetLike.mem_coe, Submodule.mem_sup,
      mem_span_singleton] at hx hy
    obtain ⟨s₁, ⟨i₁, hi₁, ⟨_, ⟨r₁, rfl⟩, hr₁⟩⟩, hs₁⟩ := hx
    obtain ⟨s₂, ⟨i₂, hi₂, ⟨_, ⟨r₂, rfl⟩, hr₂⟩⟩, hs₂⟩ := hy
    refine disjoint.ne_of_mem
      (I.add_mem (I.mul_mem_left (i₁ + x * r₁) hi₂) <| I.add_mem (I.mul_mem_right (y * r₂) hi₁) <|
        I.mul_mem_right (r₁ * r₂) hxy)
      (S.mul_mem hs₁ hs₂) ?_
    rw [← hr₁, ← hr₂]
    ring
Maximal Disjointness Implies Primality of Ideals
Informal description
Let $I$ be an ideal in a ring $\alpha$ and $S$ a submonoid of $\alpha$ such that $I$ and $S$ are disjoint (i.e., $I \cap S = \emptyset$). If $I$ is maximal with respect to this property (i.e., for any ideal $J$ strictly containing $I$, $J$ is not disjoint from $S$), then $I$ is a prime ideal.
Ideal.exists_le_prime_disjoint theorem
(S : Submonoid α) (disjoint : Disjoint (I : Set α) S) : ∃ p : Ideal α, p.IsPrime ∧ I ≤ p ∧ Disjoint (p : Set α) S
Full source 
theorem exists_le_prime_disjoint (S : Submonoid α) (disjoint : Disjoint (I : Set α) S) :
    ∃ p : Ideal α, p.IsPrime ∧ I ≤ p ∧ Disjoint (p : Set α) S := by
  have ⟨p, hIp, hp⟩ := zorn_le_nonempty₀ {p : Ideal α | Disjoint (p : Set α) S}
    (fun c hc hc' x hx ↦ ?_) I disjoint
  · exact ⟨p, isPrime_of_maximally_disjoint _ _ hp.1 (fun _ ↦ hp.not_prop_of_gt), hIp, hp.1⟩
  cases isEmpty_or_nonempty c
  · exact ⟨I, disjoint, fun J hJ ↦ isEmptyElim (⟨J, hJ⟩ : c)⟩
  refine ⟨sSup c, Set.disjoint_left.mpr fun x hx ↦ ?_, fun _ ↦ le_sSup⟩
  have ⟨p, hp⟩ := (Submodule.mem_iSup_of_directed _ hc'.directed).mp (sSup_eq_iSup' c ▸ hx)
  exact Set.disjoint_left.mp (hc p.2) hp
Existence of Prime Ideal Extending Disjoint Ideal and Submonoid
Informal description
Let $I$ be an ideal in a ring $\alpha$ and $S$ a submonoid of $\alpha$ such that $I$ and $S$ are disjoint (i.e., $I \cap S = \emptyset$). Then there exists a prime ideal $p$ of $\alpha$ such that $I \subseteq p$ and $p$ is disjoint from $S$ (i.e., $p \cap S = \emptyset$).
Ideal.exists_le_prime_nmem_of_isIdempotentElem theorem
(a : α) (ha : IsIdempotentElem a) (haI : a ∉ I) : ∃ p : Ideal α, p.IsPrime ∧ I ≤ p ∧ a ∉ p
Full source 
theorem exists_le_prime_nmem_of_isIdempotentElem (a : α) (ha : IsIdempotentElem a) (haI : a ∉ I) :
    ∃ p : Ideal α, p.IsPrime ∧ I ≤ p ∧ a ∉ p :=
  have : Disjoint (I : Set α) (Submonoid.powers a) := Set.disjoint_right.mpr <| by
    rw [ha.coe_powers]
    rintro _ (rfl|rfl)
    exacts [I.ne_top_iff_one.mp (ne_of_mem_of_not_mem' Submodule.mem_top haI).symm, haI]
  have ⟨p, h1, h2, h3⟩ := exists_le_prime_disjoint _ _ this
  ⟨p, h1, h2, Set.disjoint_right.mp h3 (Submonoid.mem_powers a)⟩
Existence of Prime Ideal Extending $I$ and Excluding an Idempotent Element
Informal description
Let $I$ be an ideal in a ring $\alpha$ and $a \in \alpha$ an idempotent element (i.e., $a^2 = a$) such that $a \notin I$. Then there exists a prime ideal $p$ of $\alpha$ such that $I \subseteq p$ and $a \notin p$.