Order ideals, cofinal sets, and the RasiowaβSikorski lemma #
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.IsIdeal I
: a predicate for when aSet P
is an ideal.Order.Ideal.principal p
: the principal ideal generated byp : P
.Order.Ideal.IsProper I
: a predicate for proper ideals. Dual to the notion of a proper filter.Order.Ideal.IsMaximal I
: 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.idealOfCofinals p π
, wherep : P
, andπ
is a countable family of cofinal subsets ofP
: 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
- carrier : Set P
- lower' : IsLowerSet s.carrier
- nonempty' : Set.Nonempty s.carrier
The ideal is nonempty.
- directed' : DirectedOn (fun x x_1 => x β€ x_1) s.carrier
The ideal is upward directed.
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
- IsLowerSet : IsLowerSet I
The ideal is downward closed.
- Nonempty : Set.Nonempty I
The ideal is nonempty.
- Directed : DirectedOn (fun x x_1 => x β€ x_1) I
The ideal is upward directed.
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).
Instances For
Create an element of type Order.Ideal
from a set satisfying the predicate
Order.IsIdeal
.
Instances For
The partial ordering by subset inclusion, inherited from Set P
.
- ne_univ : βI β Set.univ
This ideal is not the whole set.
A proper ideal is one that is not the whole set. Note that the whole set might not be an ideal.
Instances
- ne_univ : βI β Set.univ
- maximal_proper : β β¦J : Order.Ideal Pβ¦, I < J β βJ = Set.univ
This ideal is maximal in the collection of proper ideals.
An ideal is maximal if it is maximal in the collection of proper ideals.
Note that IsCoatom
is less general because ideals only have a top element when P
is directed
and nonempty.
Instances
In a directed and nonempty order, the top ideal of a is univ
.
The smallest ideal containing a given element.
Instances For
There is a bottom ideal when P
has a bottom element.
A specific witness of I.directed
when P
has joins.
The infimum of two ideals of a co-directed order is their intersection.
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
.
A (noncomputable) element of a cofinal set lying above a given element.
Instances For
Given a starting point, and a countable family of cofinal sets, this is an increasing sequence that intersects each cofinal set.
Equations
- Order.sequenceOfCofinals p π 0 = p
- Order.sequenceOfCofinals p π (Nat.succ n) = match Encodable.decode n with | none => Order.sequenceOfCofinals p π n | some i => Order.Cofinal.above (π i) (Order.sequenceOfCofinals p π n)
Instances For
Given an element p : P
and a family π
of cofinal subsets of a preorder P
,
indexed by a countable type, idealOfCofinals p π
is an ideal in P
which
- contains
p
, according tomem_idealOfCofinals p π
, and - intersects every set in
π
, according tocofinal_meets_idealOfCofinals p π
.
This proves the RasiowaβSikorski lemma.
Instances For
idealOfCofinals p π
is π
-generic.