mathlib documentation

order.ideal

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

Main definitions

We work with a preorder P throughout.

References

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 → order.ideal P

The smallest ideal containing a given element.

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

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

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

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

def order.ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] :
(ι → order.cofinal P)order.ideal 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
theorem order.mem_ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → order.cofinal 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.