mathlib documentation

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.

References #

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
@[class]
structure order.ideal.is_prime {P : Type u_1} [preorder P] (I : order.ideal P) :
Prop

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} [semilattice_inf P] {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} [semilattice_inf P] {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} [semilattice_inf P] {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} [boolean_algebra P] {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} [boolean_algebra P] {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} [boolean_algebra P] {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

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

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

Equations