# mathlib3documentation

order.prime_ideal

# Prime ideals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## 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.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

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 I x 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 I x 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 I x I y I
@[protected, instance]
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) :
@[protected, instance]
@[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) :

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

Equations