order.ideal

# Order ideals, cofinal sets, and the Rasiowa–Sikorski lemma

## Main definitions

We work with a preorder P throughout.

• ideal P: the type of upward directed, downward closed subsets of P. Dual to the notion of a filter on a preorder.
• cofinal P: the type of subsets of P containing arbitrarily large elements. Dual to the notion of 'dense set' used in forcing.
• ideal_of_cofinals p 𝒟, where p : P, and 𝒟 is a countable family of cofinal subsets of P: an ideal in P which contains p and intersects every set in 𝒟.

## References

• https://en.wikipedia.org/wiki/Ideal_(order_theory)
• https://en.wikipedia.org/wiki/Cofinal_(mathematics)
• https://en.wikipedia.org/wiki/Rasiowa–Sikorski_lemma

Note that for the Rasiowa–Sikorski lemma, Wikipedia uses the opposite ordering on P, in line with most presentations of forcing.

## Tags

ideal, cofinal, dense, countable, generic

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

An ideal on a preorder P is a subset of P that is

• nonempty
• upward directed
• downward closed.
def order.ideal.principal {P : Type u_1} [preorder P] :
P →

The smallest ideal containing a given element.

Equations
@[instance]
def order.ideal.inhabited {P : Type u_1} [preorder P] [inhabited P] :

Equations
@[instance]
def order.ideal.has_mem {P : Type u_1} [preorder P] :

Equations
structure order.cofinal (P : Type u_2) [preorder P] :
Type u_2
• carrier : set P
• mem_gt : ∀ (x : P), ∃ (y : P) (H : y c.carrier), x y

For a preorder P, cofinal P is the type of subsets of P containing arbitrarily large elements. They are the dense sets in the topology whose open sets are terminal segments.

@[instance]
def order.inhabited {P : Type u_1} [preorder P] :

Equations
@[instance]
def order.has_mem {P : Type u_1} [preorder P] :

Equations
def order.cofinal.above {P : Type u_1} [preorder P] :
P → P

A (noncomputable) element of a cofinal set lying above a given element.

Equations
theorem order.cofinal.above_mem {P : Type u_1} [preorder P] (D : order.cofinal P) (x : P) :
D.above x D

theorem order.cofinal.le_above {P : Type u_1} [preorder P] (D : order.cofinal P) (x : P) :
x D.above x

def order.sequence_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] :
(ι → → P

Given a starting point, and a countable family of cofinal sets, this is an increasing sequence that intersects each cofinal set.

Equations
• (n + 1) = order.sequence_of_cofinals._match_1 𝒟 n) n) n)
• = p
• order.sequence_of_cofinals._match_1 𝒟 _f_1 _f_2 (some i) = (𝒟 i).above _f_2
• order.sequence_of_cofinals._match_1 𝒟 _f_1 _f_2 none = _f_1
theorem order.sequence_of_cofinals.monotone {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → ) :

theorem order.sequence_of_cofinals.encode_mem {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → ) (i : ι) :
+ 1) 𝒟 i

def order.ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] :
(ι →

Given an element p : P and a family 𝒟 of cofinal subsets of a preorder P, indexed by a countable type, ideal_of_cofinals p 𝒟 is an ideal in P which

• contains p, according to mem_ideal_of_cofinals p 𝒟, and
• intersects every set in 𝒟, according to cofinal_meets_ideal_of_cofinals p 𝒟.

This proves the Rasiowa–Sikorski lemma.

Equations
theorem order.mem_ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → ) :

theorem order.cofinal_meets_ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → ) (i : ι) :
∃ (x : P), x 𝒟 i

ideal_of_cofinals p 𝒟 is 𝒟-generic.