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.

References #

https://en.wikipedia.org/wiki/Ideal_(order_theory)

Tags #

ideal, prime

source

@[nolint]

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

Type u_2

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

source

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)

source

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)

source

theorem order.ideal.prime_pair.I_is_proper {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :

IF.I.is_proper

source

theorem order.ideal.prime_pair.disjoint {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :

disjoint ↑(IF.I) ↑(IF.F)

source

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

source

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

source

theorem order.ideal.is_prime_iff {P : Type u_1} [preorder P] (I : order.ideal P) :

I.is_prime ↔ I.is_proper ∧ order.is_pfilter (↑I)ᶜ

source

@[class]

structure order.ideal.is_prime {P : Type u_1} [preorder P] (I : order.ideal P) :

Prop

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

order.ideal.is_maximal.is_prime

source

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

order.ideal.prime_pair P

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 := _}

source

theorem order.ideal.prime_pair.I_is_prime {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :

IF.I.is_prime

source

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

source

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

source

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

source

@[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

source

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

source

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

source

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

source

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

source

@[protected, instance]

def order.ideal.is_prime.is_maximal {P : Type u_1} [boolean_algebra P] {I : order.ideal P} [I.is_prime] :

I.is_maximal

source

@[class]

structure order.pfilter.is_prime {P : Type u_1} [preorder P] (F : order.pfilter P) :

Prop

compl_ideal : order.is_ideal (↑F)ᶜ

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

source

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

F.is_prime ↔ order.is_ideal (↑F)ᶜ

source

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

order.ideal.prime_pair P

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 := _}

source

theorem order.ideal.prime_pair.F_is_prime {P : Type u_1} [preorder P] (IF : order.ideal.prime_pair P) :

IF.F.is_prime