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

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.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) : Order.Ideal.IsProper IF.I

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) : Order.Ideal.IsPrime I ↔ Order.Ideal.IsProper I ∧ 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)ᶜ

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

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

Equations

• Order.Ideal.IsPrime.toPrimePair h = { I := I, F := Order.IsPFilter.toPFilter ⋯, isCompl_I_F := ⋯ }

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

theorem Order.Ideal.IsPrime.mem_or_mem {P : Type u_1} [SemilatticeInf P] {I : Order.Ideal P} (hI : Order.Ideal.IsPrime I) {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} [Order.Ideal.IsProper I] (hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I) : Order.Ideal.IsPrime I

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

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

Equations

• ⋯ = ⋯

theorem Order.Ideal.IsPrime.mem_or_compl_mem {P : Type u_1} [BooleanAlgebra P] {x : P} {I : Order.Ideal P} (hI : Order.Ideal.IsPrime I) : 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 : Order.Ideal.IsPrime I) (hxnI : x ∉ I) : xᶜ ∈ I

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

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

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

Equations

• ⋯ = ⋯

theorem Order.PFilter.isPrime_iff {P : Type u_1} [Preorder P] (F : Order.PFilter P) : Order.PFilter.IsPrime F ↔ 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)ᶜ

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

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

Equations

• Order.PFilter.IsPrime.toPrimePair h = { I := Order.IsIdeal.toIdeal ⋯, F := F, isCompl_I_F := ⋯ }

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