mathlib documentation

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

carrier : set P
nonempty : c.carrier.nonempty
directed : directed_on has_le.le c.carrier
mem_of_le : ∀ {x y : P}, x ≤ y → y ∈ c.carrier → x ∈ c.carrier

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 : P) :

The smallest ideal containing a given element.

Equations

order.ideal.principal p = {carrier := {x : P | x ≤ p}, nonempty := _, directed := _, mem_of_le := _}

@[instance]

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

inhabited (order.ideal P)

Equations

order.ideal.inhabited = {default := order.ideal.principal (default P)}

@[instance]

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

has_mem P (order.ideal P)

Equations

order.ideal.has_mem = {mem := λ (x : P) (I : order.ideal P), x ∈ I.carrier}

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] :

inhabited (order.cofinal P)

Equations

order.inhabited = {default := {carrier := set.univ P, mem_gt := _}}

@[instance]

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

has_mem P (order.cofinal P)

Equations

order.has_mem = {mem := λ (x : P) (D : order.cofinal P), x ∈ D.carrier}

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

P

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

Equations

D.above x = classical.some _

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 ι] (𝒟 : ι → order.cofinal P) (a : ℕ) :

P

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

Equations

order.sequence_of_cofinals p 𝒟 (n + 1) = order.sequence_of_cofinals._match_1 𝒟 (order.sequence_of_cofinals p 𝒟 n) (order.sequence_of_cofinals p 𝒟 n) (encodable.decode ι n)
order.sequence_of_cofinals p 𝒟 0 = 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 ι] (𝒟 : ι → order.cofinal P) :

monotone (order.sequence_of_cofinals p 𝒟)

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

order.sequence_of_cofinals p 𝒟 (encodable.encode i + 1) ∈ 𝒟 i

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

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

order.ideal_of_cofinals p 𝒟 = {carrier := {x : P | ∃ (n : ℕ), x ≤ order.sequence_of_cofinals p 𝒟 n}, nonempty := _, directed := _, mem_of_le := _}

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

p ∈ order.ideal_of_cofinals p 𝒟

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

∃ (x : P), x ∈ 𝒟 i ∧ x ∈ order.ideal_of_cofinals p 𝒟

ideal_of_cofinals p 𝒟 is 𝒟-generic.