Order ideals, cofinal sets, and the Rasiowa–Sikorski lemma #
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 P
: the type of nonempty, upward directed, and downward closed subsets ofP
. Dual to the notion of a filter on a preorder.order.is_ideal P
: a predicate for when aset P
is an ideal.order.ideal.principal p
: the principal ideal generated byp : P
.order.ideal.is_proper P
: a predicate for proper ideals. Dual to the notion of a proper filter.order.ideal.is_maximal
: a predicate for maximal ideals. Dual to the notion of an ultrafilter.order.cofinal P
: the type of subsets ofP
containing arbitrarily large elements. Dual to the notion of 'dense set' used in forcing.order.ideal_of_cofinals p 𝒟
, wherep : P
, and𝒟
is a countable family of cofinal subsets of P: an ideal inP
which containsp
and intersects every set in𝒟
. (This a form of the Rasiowa–Sikorski lemma.)
References #
- https://en.wikipedia.org/wiki/Ideal_(order_theory)
- https://en.wikipedia.org/wiki/Cofinal_(mathematics)
- https://en.wikipedia.org/wiki/Rasiowa%E2%80%93Sikorski_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
- to_lower_set : lower_set P
- nonempty' : self.to_lower_set.carrier.nonempty
- directed' : directed_on has_le.le self.to_lower_set.carrier
An ideal on an order P
is a subset of P
that is
- nonempty
- upward directed (any pair of elements in the ideal has an upper bound in the ideal)
- downward closed (any element less than an element of the ideal is in the ideal).
Instances for order.ideal
- is_lower_set : is_lower_set I
- nonempty : I.nonempty
- directed : directed_on has_le.le I
A subset of a preorder P
is an ideal if it is
- nonempty
- upward directed (any pair of elements in the ideal has an upper bound in the ideal)
- downward closed (any element less than an element of the ideal is in the ideal).
Create an element of type order.ideal
from a set satisfying the predicate
order.is_ideal
.
Equations
- order.ideal.set_like = {coe := λ (s : order.ideal P), s.to_lower_set.carrier, coe_injective' := _}
The partial ordering by subset inclusion, inherited from set P
.
Equations
- order.ideal.partial_order = partial_order.lift coe order.ideal.partial_order._proof_1
A proper ideal is one that is not the whole set. Note that the whole set might not be an ideal.
Instances of this typeclass
In a directed and nonempty order, the top ideal of a is univ
.
Equations
- order.ideal.order_top = {top := {to_lower_set := ⊤, nonempty' := _, directed' := _}, le_top := _}
The smallest ideal containing a given element.
Equations
- order.ideal.principal p = {to_lower_set := lower_set.Iic p, nonempty' := _, directed' := _}
Equations
There is a bottom ideal when P
has a bottom element.
Equations
- order.ideal.order_bot = {bot := order.ideal.principal ⊥, bot_le := _}
A specific witness of I.directed
when P
has joins.
The infimum of two ideals of a co-directed order is their intersection.
Equations
- order.ideal.has_inf = {inf := λ (I J : order.ideal P), {to_lower_set := I.to_lower_set ⊓ J.to_lower_set, nonempty' := _, directed' := _}}
The supremum of two ideals of a co-directed order is the union of the down sets of the pointwise
supremum of I
and J
.
Equations
- order.ideal.lattice = {sup := has_sup.sup order.ideal.has_sup, le := partial_order.le order.ideal.partial_order, lt := partial_order.lt order.ideal.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf order.ideal.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
- order.ideal.has_Inf = {Inf := λ (S : set (order.ideal P)), {to_lower_set := ⨅ (s : order.ideal P) (H : s ∈ S), s.to_lower_set, nonempty' := _, directed' := _}}
Equations
- order.ideal.complete_lattice = {sup := lattice.sup order.ideal.lattice, le := lattice.le order.ideal.lattice, lt := lattice.lt order.ideal.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf order.ideal.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (order.ideal P) order.ideal.complete_lattice._proof_12), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (order.ideal P) order.ideal.complete_lattice._proof_12), Inf_le := _, le_Inf := _, top := complete_lattice.top (complete_lattice_of_Inf (order.ideal P) order.ideal.complete_lattice._proof_12), bot := complete_lattice.bot (complete_lattice_of_Inf (order.ideal P) order.ideal.complete_lattice._proof_12), le_top := _, bot_le := _}
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.
Instances for order.cofinal
- order.cofinal.has_sizeof_inst
- order.cofinal.inhabited
- order.cofinal.has_mem
Equations
- order.cofinal.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 𝒟 = {to_lower_set := {carrier := {x : P | ∃ (n : ℕ), x ≤ order.sequence_of_cofinals p 𝒟 n}, lower' := _}, nonempty' := _, directed' := _}
ideal_of_cofinals p 𝒟
is 𝒟
-generic.