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 : Order.Ideal P
• F : Order.PFilter P
• isCompl_I_F : IsCompl ↑self.I ↑self.F

theorem Order.Ideal.PrimePair.isCompl_I_F {P : Type u_2} [Preorder P] (self : Order.Ideal.PrimePair P) : IsCompl ↑self.I ↑self.F

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

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

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

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

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

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

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

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

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

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

theorem Order.Ideal.IsPrime.compl_filter {P : Type u_1} [Preorder P] {I : Order.Ideal P} [self : I.IsPrime] : Order.IsPFilter (↑I)ᶜ

def Order.Ideal.IsPrime.toPrimePair {P : Type u_1} [Preorder P] {I : Order.Ideal P} (h : I.IsPrime) : Order.Ideal.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 : Order.Ideal.PrimePair P) : IF.I.IsPrime

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

theorem Order.Ideal.IsPrime.of_mem_or_mem {P : Type u_1} [SemilatticeInf P] {I : Order.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 : Order.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 : Order.Ideal P} [I.IsMaximal] : I.IsPrime

Equations

• ⋯ = ⋯

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

theorem Order.Ideal.IsPrime.mem_compl_of_not_mem {P : Type u_1} [BooleanAlgebra P] {x : P} {I : Order.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 : Order.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 : Order.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 : Order.Ideal P} [I.IsPrime] : I.IsMaximal

Equations

• ⋯ = ⋯

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

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

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

• compl_ideal : Order.IsIdeal (↑F)ᶜ

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

def Order.PFilter.IsPrime.toPrimePair {P : Type u_1} [Preorder P] {F : Order.PFilter P} (h : F.IsPrime) : Order.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 : Order.Ideal.PrimePair P) : IF.F.IsPrime