# mathlibdocumentation

order.prime_ideal

# 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.prime_pair: A pair of an ideal and a 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.is_prime: a predicate for prime ideals. Dual to the notion of a prime filter.
• order.pfilter.is_prime: a predicate for prime filters. Dual to the notion of a prime ideal.

## Tags #

ideal, prime

@[nolint]
structure order.ideal.prime_pair (P : Type u_2) [preorder P] :
Type u_2

A pair of an ideal and a pfilter which form a partition of P.

Instances for order.ideal.prime_pair
• order.ideal.prime_pair.has_sizeof_inst
theorem order.ideal.prime_pair.compl_I_eq_F {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :
((IF.I)) = (IF.F)
theorem order.ideal.prime_pair.compl_F_eq_I {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :
((IF.F)) = (IF.I)
theorem order.ideal.prime_pair.disjoint {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :
disjoint (IF.I) (IF.F)
theorem order.ideal.prime_pair.I_union_F {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :
(IF.I) (IF.F) = set.univ
theorem order.ideal.prime_pair.F_union_I {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :
(IF.F) (IF.I) = set.univ
theorem order.ideal.is_prime_iff {P : Type u_1} [preorder P] (I : order.ideal P) :
@[class]
structure order.ideal.is_prime {P : Type u_1} [preorder P] (I : order.ideal P) :
Prop
• to_is_proper :
• compl_filter :

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

Instances of this typeclass
def order.ideal.is_prime.to_prime_pair {P : Type u_1} [preorder P] {I : order.ideal P} (h : I.is_prime) :

Create an element of type order.ideal.prime_pair from an ideal satisfying the predicate order.ideal.is_prime.

Equations
theorem order.ideal.is_prime.mem_or_mem {P : Type u_1} {I : order.ideal P} (hI : I.is_prime) {x y : P} :
x y Ix I y I
theorem order.ideal.is_prime.of_mem_or_mem {P : Type u_1} {I : order.ideal P} [I.is_proper] (hI : ∀ {x y : P}, x y Ix I y I) :
theorem order.ideal.is_prime_iff_mem_or_mem {P : Type u_1} {I : order.ideal P} [I.is_proper] :
I.is_prime ∀ {x y : P}, x y Ix I y I
@[protected, instance]
def order.ideal.is_maximal.is_prime {P : Type u_1} {I : order.ideal P} [I.is_maximal] :
theorem order.ideal.is_prime.mem_or_compl_mem {P : Type u_1} {x : P} {I : order.ideal P} (hI : I.is_prime) :
x I x I
theorem order.ideal.is_prime.mem_compl_of_not_mem {P : Type u_1} {x : P} {I : order.ideal P} (hI : I.is_prime) (hxnI : x I) :
x I
theorem order.ideal.is_prime_of_mem_or_compl_mem {P : Type u_1} {I : order.ideal P} [I.is_proper] (h : ∀ {x : P}, x I x I) :
theorem order.ideal.is_prime_iff_mem_or_compl_mem {P : Type u_1} {I : order.ideal P} [I.is_proper] :
I.is_prime ∀ {x : P}, x I x I
@[protected, instance]
def order.ideal.is_prime.is_maximal {P : Type u_1} {I : order.ideal P} [I.is_prime] :
@[class]
structure order.pfilter.is_prime {P : Type u_1} [preorder P] (F : order.pfilter P) :
Prop
• compl_ideal :

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

theorem order.pfilter.is_prime_iff {P : Type u_1} [preorder P] (F : order.pfilter P) :
def order.pfilter.is_prime.to_prime_pair {P : Type u_1} [preorder P] {F : order.pfilter P} (h : F.is_prime) :

Create an element of type order.ideal.prime_pair from a filter satisfying the predicate order.pfilter.is_prime.

Equations