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
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
@[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 Ix 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 Ix 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 Ix 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) :
theorem order.ideal.is_prime_iff_mem_or_compl_mem {P : Type u_1} [boolean_algebra P] {I : order.ideal P} [I.is_proper] :
I.is_prime ∀ {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