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 anideal
and apfilter
which form a partition ofP
. 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.
References #
Tags #
ideal, prime
@[nolint]
- I : order.ideal P
- F : order.pfilter P
- is_compl_I_F : is_compl ↑(self.I) ↑(self.F)
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) :
theorem
order.ideal.prime_pair.compl_F_eq_I
{P : Type u_1}
[preorder P]
(IF : order.ideal.prime_pair P) :
theorem
order.ideal.prime_pair.I_is_proper
{P : Type u_1}
[preorder P]
(IF : order.ideal.prime_pair P) :
theorem
order.ideal.prime_pair.disjoint
{P : Type u_1}
[preorder P]
(IF : order.ideal.prime_pair P) :
@[class]
- to_is_proper : I.is_proper
- compl_filter : order.is_pfilter (↑I)ᶜ
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
- h.to_prime_pair = {I := I, F := order.ideal.is_prime.compl_filter.to_pfilter, is_compl_I_F := _}
theorem
order.ideal.prime_pair.I_is_prime
{P : Type u_1}
[preorder P]
(IF : order.ideal.prime_pair P) :
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} :
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) :
I.is_prime
theorem
order.ideal.is_prime_iff_mem_or_mem
{P : Type u_1}
[semilattice_inf P]
{I : order.ideal P}
[I.is_proper] :
@[protected, instance]
def
order.ideal.is_maximal.is_prime
{P : Type u_1}
[distrib_lattice P]
{I : order.ideal P}
[I.is_maximal] :
I.is_prime
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) :
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) :
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) :
I.is_prime
theorem
order.ideal.is_prime_iff_mem_or_compl_mem
{P : Type u_1}
[boolean_algebra P]
{I : order.ideal P}
[I.is_proper] :
@[protected, instance]
def
order.ideal.is_prime.is_maximal
{P : Type u_1}
[boolean_algebra P]
{I : order.ideal P}
[I.is_prime] :
theorem
order.pfilter.is_prime_iff
{P : Type u_1}
[preorder P]
(F : order.pfilter P) :
F.is_prime ↔ order.is_ideal (↑F)ᶜ
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
- h.to_prime_pair = {I := order.pfilter.is_prime.compl_ideal.to_ideal, F := F, is_compl_I_F := _}
theorem
order.ideal.prime_pair.F_is_prime
{P : Type u_1}
[preorder P]
(IF : order.ideal.prime_pair P) :