Prime ideals

Main definitions

Throughout this file, P is at least a preorder, but some sections require more structure, such as a bottom element, a top element, or a join-semilattice structure.

• Order.Ideal.PrimePair: A pair of an Order.Ideal and an Order.PFilter which form a partition of P. This is useful as giving the data of a prime ideal is the same as giving the data of a prime filter.
• Order.Ideal.IsPrime: a predicate for prime ideals. Dual to the notion of a prime filter.
• Order.PFilter.IsPrime: a predicate for prime filters. Dual to the notion of a prime ideal.

References

• https://en.wikipedia.org/wiki/Ideal_(order_theory)

Tags

ideal, prime

structure Order.Ideal.PrimePair (P : Type u_2) [Preorder P] : Type u_2

A pair of an Order.Ideal and an Order.PFilter which form a partition of P.

• I : Ideal P
• F : PFilter P
• isCompl_I_F : IsCompl ↑self.I ↑self.F

theorem Order.Ideal.PrimePair.compl_I_eq_F {P : Type u_1} [Preorder P] (IF : PrimePair P) : (↑IF.I)ᶜ = ↑IF.F

theorem Order.Ideal.PrimePair.compl_F_eq_I {P : Type u_1} [Preorder P] (IF : PrimePair P) : (↑IF.F)ᶜ = ↑IF.I

theorem Order.Ideal.PrimePair.I_isProper {P : Type u_1} [Preorder P] (IF : PrimePair P) : IF.I.IsProper

theorem Order.Ideal.PrimePair.disjoint {P : Type u_1} [Preorder P] (IF : PrimePair P) : Disjoint ↑IF.I ↑IF.F

theorem Order.Ideal.PrimePair.I_union_F {P : Type u_1} [Preorder P] (IF : PrimePair P) : ↑IF.I ∪ ↑IF.F = Set.univ

theorem Order.Ideal.PrimePair.F_union_I {P : Type u_1} [Preorder P] (IF : PrimePair P) : ↑IF.F ∪ ↑IF.I = Set.univ

class Order.Ideal.IsPrime {P : Type u_1} [Preorder P] (I : Ideal P) extends I.IsProper : Prop

An ideal I is prime if its complement is a filter.

• ne_univ : ↑I ≠ Set.univ
• compl_filter : IsPFilter (↑I)ᶜ

theorem Order.Ideal.isPrime_iff {P : Type u_1} [Preorder P] (I : Ideal P) : I.IsPrime ↔ I.IsProper ∧ IsPFilter (↑I)ᶜ

def Order.Ideal.IsPrime.toPrimePair {P : Type u_1} [Preorder P] {I : Ideal P} (h : I.IsPrime) : PrimePair P

Create an element of type Order.Ideal.PrimePair from an ideal satisfying the predicate Order.Ideal.IsPrime.

Equations

• h.toPrimePair = { I := I, F := ⋯.toPFilter, isCompl_I_F := ⋯ }

theorem Order.Ideal.PrimePair.I_isPrime {P : Type u_1} [Preorder P] (IF : PrimePair P) : IF.I.IsPrime

theorem Order.Ideal.IsPrime.mem_or_mem {P : Type u_1} [SemilatticeInf P] {I : Ideal P} (hI : I.IsPrime) {x y : P} : x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

theorem Order.Ideal.IsPrime.of_mem_or_mem {P : Type u_1} [SemilatticeInf P] {I : Ideal P} [I.IsProper] (hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I) : I.IsPrime

theorem Order.Ideal.isPrime_iff_mem_or_mem {P : Type u_1} [SemilatticeInf P] {I : Ideal P} [I.IsProper] : I.IsPrime ↔ ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

@[instance 100]

instance Order.Ideal.IsMaximal.isPrime {P : Type u_1} [DistribLattice P] {I : Ideal P} [I.IsMaximal] : I.IsPrime

theorem Order.Ideal.IsPrime.mem_or_compl_mem {P : Type u_1} [BooleanAlgebra P] {x : P} {I : Ideal P} (hI : I.IsPrime) : x ∈ I ∨ xᶜ ∈ I

theorem Order.Ideal.IsPrime.compl_mem_of_notMem {P : Type u_1} [BooleanAlgebra P] {x : P} {I : Ideal P} (hI : I.IsPrime) (hxnI : x ∉ I) : xᶜ ∈ I

theorem Order.Ideal.isPrime_of_mem_or_compl_mem {P : Type u_1} [BooleanAlgebra P] {I : Ideal P} [I.IsProper] (h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I) : I.IsPrime

theorem Order.Ideal.isPrime_iff_mem_or_compl_mem {P : Type u_1} [BooleanAlgebra P] {I : Ideal P} [I.IsProper] : I.IsPrime ↔ ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I

@[instance 100]

instance Order.Ideal.IsPrime.isMaximal {P : Type u_1} [BooleanAlgebra P] {I : Ideal P} [I.IsPrime] : I.IsMaximal

class Order.PFilter.IsPrime {P : Type u_1} [Preorder P] (F : PFilter P) : Prop

A filter F is prime if its complement is an ideal.

• compl_ideal : IsIdeal (↑F)ᶜ

theorem Order.PFilter.isPrime_iff {P : Type u_1} [Preorder P] (F : PFilter P) : F.IsPrime ↔ IsIdeal (↑F)ᶜ

def Order.PFilter.IsPrime.toPrimePair {P : Type u_1} [Preorder P] {F : PFilter P} (h : F.IsPrime) : Ideal.PrimePair P

Create an element of type Order.Ideal.PrimePair from a filter satisfying the predicate Order.PFilter.IsPrime.

Equations

• h.toPrimePair = { I := ⋯.toIdeal, F := F, isCompl_I_F := ⋯ }

theorem Order.Ideal.PrimePair.F_isPrime {P : Type u_1} [Preorder P] (IF : PrimePair P) : IF.F.IsPrime