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.

Tags #

ideal, prime

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

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

• I :
• F :
• isCompl_I_F : IsCompl self.I self.F
Instances For
theorem Order.Ideal.PrimePair.isCompl_I_F {P : Type u_2} [] (self : ) :
IsCompl self.I self.F
theorem Order.Ideal.PrimePair.compl_I_eq_F {P : Type u_1} [] (IF : ) :
(↑IF.I) = IF.F
theorem Order.Ideal.PrimePair.compl_F_eq_I {P : Type u_1} [] (IF : ) :
(↑IF.F) = IF.I
theorem Order.Ideal.PrimePair.I_isProper {P : Type u_1} [] (IF : ) :
IF.I.IsProper
theorem Order.Ideal.PrimePair.disjoint {P : Type u_1} [] (IF : ) :
Disjoint IF.I IF.F
theorem Order.Ideal.PrimePair.I_union_F {P : Type u_1} [] (IF : ) :
IF.I IF.F = Set.univ
theorem Order.Ideal.PrimePair.F_union_I {P : Type u_1} [] (IF : ) :
IF.F IF.I = Set.univ
theorem Order.Ideal.isPrime_iff {P : Type u_1} [] (I : ) :
I.IsPrime I.IsProper Order.IsPFilter (↑I)
class Order.Ideal.IsPrime {P : Type u_1} [] (I : ) extends :

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

Instances
theorem Order.Ideal.IsPrime.compl_filter {P : Type u_1} [] {I : } [self : I.IsPrime] :
def Order.Ideal.IsPrime.toPrimePair {P : Type u_1} [] {I : } (h : I.IsPrime) :

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 := }
Instances For
theorem Order.Ideal.PrimePair.I_isPrime {P : Type u_1} [] (IF : ) :
IF.I.IsPrime
theorem Order.Ideal.IsPrime.mem_or_mem {P : Type u_1} [] {I : } (hI : I.IsPrime) {x : P} {y : P} :
x y Ix I y I
theorem Order.Ideal.IsPrime.of_mem_or_mem {P : Type u_1} [] {I : } [I.IsProper] (hI : ∀ {x y : P}, x y Ix I y I) :
I.IsPrime
theorem Order.Ideal.isPrime_iff_mem_or_mem {P : Type u_1} [] {I : } [I.IsProper] :
I.IsPrime ∀ {x y : P}, x y Ix I y I
@[instance 100]
instance Order.Ideal.IsMaximal.isPrime {P : Type u_1} [] {I : } [I.IsMaximal] :
I.IsPrime
Equations
• =
theorem Order.Ideal.IsPrime.mem_or_compl_mem {P : Type u_1} [] {x : P} {I : } (hI : I.IsPrime) :
x I x I
theorem Order.Ideal.IsPrime.mem_compl_of_not_mem {P : Type u_1} [] {x : P} {I : } (hI : I.IsPrime) (hxnI : xI) :
x I
theorem Order.Ideal.isPrime_of_mem_or_compl_mem {P : Type u_1} [] {I : } [I.IsProper] (h : ∀ {x : P}, x I x I) :
I.IsPrime
theorem Order.Ideal.isPrime_iff_mem_or_compl_mem {P : Type u_1} [] {I : } [I.IsProper] :
I.IsPrime ∀ {x : P}, x I x I
@[instance 100]
instance Order.Ideal.IsPrime.isMaximal {P : Type u_1} [] {I : } [I.IsPrime] :
I.IsMaximal
Equations
• =
theorem Order.PFilter.isPrime_iff {P : Type u_1} [] (F : ) :
F.IsPrime Order.IsIdeal (↑F)
class Order.PFilter.IsPrime {P : Type u_1} [] (F : ) :

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

Instances
theorem Order.PFilter.IsPrime.compl_ideal {P : Type u_1} [] {F : } [self : F.IsPrime] :
def Order.PFilter.IsPrime.toPrimePair {P : Type u_1} [] {F : } (h : F.IsPrime) :

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 := }
Instances For
theorem Order.Ideal.PrimePair.F_isPrime {P : Type u_1} [] (IF : ) :
IF.F.IsPrime