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 ofP. Dual to the notion of a filter on a preorder.cofinal P: the type of subsets ofPcontaining arbitrarily large elements. Dual to the notion of 'dense set' used in forcing.ideal_of_cofinals p ๐, wherep : P, and๐is a countable family of cofinal subsets of P: an ideal inPwhich containspand 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
The smallest ideal containing a given element.
Equations
Equations
- order.ideal.has_mem = {mem := ฮป (x : P) (I : order.ideal P), x โ I.carrier}
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.
Equations
- order.has_mem = {mem := ฮป (x : P) (D : order.cofinal P), x โ D.carrier}
A (noncomputable) element of a cofinal set lying above a given element.
Equations
- D.above x = classical.some _
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 (option.some i) = (๐ i).above _f_2
- order.sequence_of_cofinals._match_1 ๐ _f_1 _f_2 option.none = _f_1
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 tomem_ideal_of_cofinals p ๐, and - intersects every set in
๐, according tocofinal_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 := _}
ideal_of_cofinals p ๐ is ๐-generic.