# 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 of P. Dual to the notion of a filter on a preorder.
• Order.IsIdeal I: a predicate for when a Set P is an ideal.
• Order.Ideal.principal p: the principal ideal generated by p : 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 of P containing arbitrarily large elements. Dual to the notion of 'dense set' used in forcing.
• Order.idealOfCofinals 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 π. (This a form of the RasiowaβSikorski lemma.)

## 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) [LE P] extends :
Type u_2

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).
• carrier : Set P
• lower' : IsLowerSet self.carrier
• nonempty' : self.carrier.Nonempty

The ideal is nonempty.

• directed' : DirectedOn (fun (x x_1 : P) => x β€ x_1) self.carrier

The ideal is upward directed.

Instances For
theorem Order.Ideal.nonempty' {P : Type u_2} [LE P] (self : ) :
self.carrier.Nonempty

The ideal is nonempty.

theorem Order.Ideal.directed' {P : Type u_2} [LE P] (self : ) :
DirectedOn (fun (x x_1 : P) => x β€ x_1) self.carrier

The ideal is upward directed.

theorem Order.isIdeal_iff {P : Type u_2} [LE P] (I : Set P) :
β β§ I.Nonempty β§ DirectedOn (fun (x x_1 : P) => x β€ x_1) I
structure Order.IsIdeal {P : Type u_2} [LE P] (I : Set P) :

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).
• IsLowerSet :

The ideal is downward closed.

• Nonempty : I.Nonempty

The ideal is nonempty.

• Directed : DirectedOn (fun (x x_1 : P) => x β€ x_1) I

The ideal is upward directed.

Instances For
theorem Order.IsIdeal.IsLowerSet {P : Type u_2} [LE P] {I : Set P} (self : ) :

The ideal is downward closed.

theorem Order.IsIdeal.Nonempty {P : Type u_2} [LE P] {I : Set P} (self : ) :
I.Nonempty

The ideal is nonempty.

theorem Order.IsIdeal.Directed {P : Type u_2} [LE P] {I : Set P} (self : ) :
DirectedOn (fun (x x_1 : P) => x β€ x_1) I

The ideal is upward directed.

def Order.IsIdeal.toIdeal {P : Type u_1} [LE P] {I : Set P} (h : ) :

Create an element of type Order.Ideal from a set satisfying the predicate Order.IsIdeal.

Equations
• h.toIdeal = { carrier := I, lower' := β―, nonempty' := β―, directed' := β― }
Instances For
theorem Order.Ideal.toLowerSet_injective {P : Type u_1} [LE P] :
Function.Injective Order.Ideal.toLowerSet
instance Order.Ideal.instSetLike {P : Type u_1} [LE P] :
SetLike () P
Equations
• Order.Ideal.instSetLike = { coe := fun (s : ) => s.carrier, coe_injective' := β― }
theorem Order.Ideal.ext {P : Type u_1} [LE P] {s : } {t : } :
βs = βt β s = t
@[simp]
theorem Order.Ideal.carrier_eq_coe {P : Type u_1} [LE P] (s : ) :
s.carrier = βs
@[simp]
theorem Order.Ideal.coe_toLowerSet {P : Type u_1} [LE P] (s : ) :
βs.toLowerSet = βs
theorem Order.Ideal.lower {P : Type u_1} [LE P] (s : ) :
IsLowerSet βs
theorem Order.Ideal.nonempty {P : Type u_1} [LE P] (s : ) :
(βs).Nonempty
theorem Order.Ideal.directed {P : Type u_1} [LE P] (s : ) :
DirectedOn (fun (x x_1 : P) => x β€ x_1) βs
theorem Order.Ideal.isIdeal {P : Type u_1} [LE P] (s : ) :
theorem Order.Ideal.mem_compl_of_ge {P : Type u_1} [LE P] {I : } {x : P} {y : P} :
x β€ y β x β (βI)αΆ β y β (βI)αΆ
instance Order.Ideal.instPartialOrderIdeal {P : Type u_1} [LE P] :

The partial ordering by subset inclusion, inherited from Set P.

Equations
theorem Order.Ideal.coe_subset_coe {P : Type u_1} [LE P] {s : } {t : } :
βs β βt β s β€ t
theorem Order.Ideal.coe_ssubset_coe {P : Type u_1} [LE P] {s : } {t : } :
βs β βt β s < t
theorem Order.Ideal.mem_of_mem_of_le {P : Type u_1} [LE P] {x : P} {I : } {J : } :
x β I β I β€ J β x β J
theorem Order.Ideal.isProper_iff {P : Type u_1} [LE P] (I : ) :
I.IsProper β βI β  Set.univ
class Order.Ideal.IsProper {P : Type u_1} [LE P] (I : ) :

A proper ideal is one that is not the whole set. Note that the whole set might not be an ideal.

• ne_univ : βI β  Set.univ

This ideal is not the whole set.

Instances
theorem Order.Ideal.IsProper.ne_univ {P : Type u_1} [LE P] {I : } [self : I.IsProper] :
βI β  Set.univ

This ideal is not the whole set.

theorem Order.Ideal.isProper_of_not_mem {P : Type u_1} [LE P] {I : } {p : P} (nmem : p β I) :
I.IsProper
theorem Order.Ideal.isMaximal_iff {P : Type u_1} [LE P] (I : ) :
I.IsMaximal β I.IsProper β§ β β¦J : β¦, I < J β βJ = Set.univ
class Order.Ideal.IsMaximal {P : Type u_1} [LE P] (I : ) extends :

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.

• ne_univ : βI β  Set.univ
• maximal_proper : β β¦J : β¦, I < J β βJ = Set.univ

This ideal is maximal in the collection of proper ideals.

Instances
theorem Order.Ideal.IsMaximal.maximal_proper {P : Type u_1} [LE P] {I : } [self : I.IsMaximal] β¦J : β¦ :
I < J β βJ = Set.univ

This ideal is maximal in the collection of proper ideals.

theorem Order.Ideal.inter_nonempty {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β₯ x_1] (I : ) (J : ) :
instance Order.Ideal.instOrderTop {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] :

In a directed and nonempty order, the top ideal of a is univ.

Equations
@[simp]
theorem Order.Ideal.top_toLowerSet {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] :
β€.toLowerSet = β€
@[simp]
theorem Order.Ideal.coe_top {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] :
ββ€ = Set.univ
theorem Order.Ideal.isProper_of_ne_top {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] {I : } (ne_top : ) :
I.IsProper
theorem Order.Ideal.IsProper.ne_top {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] {I : } :
I.IsProper β
theorem IsCoatom.isProper {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] {I : } (hI : ) :
I.IsProper
theorem Order.Ideal.isProper_iff_ne_top {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] {I : } :
I.IsProper β
theorem Order.Ideal.IsMaximal.isCoatom {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] {I : } :
I.IsMaximal β
theorem Order.Ideal.IsMaximal.isCoatom' {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] {I : } [I.IsMaximal] :
theorem IsCoatom.isMaximal {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] {I : } (hI : ) :
I.IsMaximal
theorem Order.Ideal.isMaximal_iff_isCoatom {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x β€ x_1] [] {I : } :
I.IsMaximal β
@[simp]
theorem Order.Ideal.bot_mem {P : Type u_1} [LE P] [] (s : ) :
theorem Order.Ideal.top_of_top_mem {P : Type u_1} [LE P] [] {I : } (h : ) :
theorem Order.Ideal.IsProper.top_not_mem {P : Type u_1} [LE P] [] {I : } (hI : I.IsProper) :
β€ β I
@[simp]
theorem Order.Ideal.principal_toLowerSet {P : Type u_1} [] (p : P) :
.toLowerSet =
def Order.Ideal.principal {P : Type u_1} [] (p : P) :

The smallest ideal containing a given element.

Equations
• = { toLowerSet := , nonempty' := β―, directed' := β― }
Instances For
instance Order.Ideal.instInhabited {P : Type u_1} [] [] :
Equations
@[simp]
theorem Order.Ideal.principal_le_iff {P : Type u_1} [] {I : } {x : P} :
@[simp]
theorem Order.Ideal.mem_principal {P : Type u_1} [] {x : P} {y : P} :
theorem Order.Ideal.mem_principal_self {P : Type u_1} [] {x : P} :
instance Order.Ideal.instOrderBot {P : Type u_1} [] [] :

There is a bottom ideal when P has a bottom element.

Equations
@[simp]
theorem Order.Ideal.principal_bot {P : Type u_1} [] [] :
@[simp]
theorem Order.Ideal.principal_top {P : Type u_1} [] [] :
theorem Order.Ideal.sup_mem {P : Type u_1} [] {x : P} {y : P} {s : } (hx : x β s) (hy : y β s) :

A specific witness of I.directed when P has joins.

@[simp]
theorem Order.Ideal.sup_mem_iff {P : Type u_1} [] {x : P} {y : P} {I : } :
instance Order.Ideal.instInf {P : Type u_1} [] [IsDirected P fun (x x_1 : P) => x β₯ x_1] :
Inf ()

The infimum of two ideals of a co-directed order is their intersection.

Equations
• Order.Ideal.instInf = { inf := fun (I J : ) => { toLowerSet := I.toLowerSet β J.toLowerSet, nonempty' := β―, directed' := β― } }
instance Order.Ideal.instSup {P : Type u_1} [] [IsDirected P fun (x x_1 : P) => x β₯ x_1] :
Sup ()

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.instSup = { sup := fun (I J : ) => { carrier := {x : P | β i β I, β j β J, x β€ i β j}, lower' := β―, nonempty' := β―, directed' := β― } }
instance Order.Ideal.instLattice {P : Type u_1} [] [IsDirected P fun (x x_1 : P) => x β₯ x_1] :
Equations
• Order.Ideal.instLattice = let __src := Order.Ideal.instPartialOrderIdeal; Lattice.mk β― β― β―
@[simp]
theorem Order.Ideal.coe_sup {P : Type u_1} [] [IsDirected P fun (x x_1 : P) => x β₯ x_1] {s : } {t : } :
β(s β t) = {x : P | β a β s, β b β t, x β€ a β b}
@[simp]
theorem Order.Ideal.coe_inf {P : Type u_1} [] [IsDirected P fun (x x_1 : P) => x β₯ x_1] {s : } {t : } :
β(s β t) = βs β© βt
@[simp]
theorem Order.Ideal.mem_inf {P : Type u_1} [] [IsDirected P fun (x x_1 : P) => x β₯ x_1] {x : P} {I : } {J : } :
@[simp]
theorem Order.Ideal.mem_sup {P : Type u_1} [] [IsDirected P fun (x x_1 : P) => x β₯ x_1] {x : P} {I : } {J : } :
x β I β J β β i β I, β j β J, x β€ i β j
theorem Order.Ideal.lt_sup_principal_of_not_mem {P : Type u_1} [] [IsDirected P fun (x x_1 : P) => x β₯ x_1] {x : P} {I : } (hx : x β I) :
instance Order.Ideal.instInfSet {P : Type u_1} [] [] :
Equations
• Order.Ideal.instInfSet = { sInf := fun (S : Set ()) => { toLowerSet := β¨ s β S, s.toLowerSet, nonempty' := β―, directed' := β― } }
@[simp]
theorem Order.Ideal.coe_sInf {P : Type u_1} [] [] {S : Set ()} :
β(sInf S) = β s β S, βs
@[simp]
theorem Order.Ideal.mem_sInf {P : Type u_1} [] [] {x : P} {S : Set ()} :
x β sInf S β β s β S, x β s
instance Order.Ideal.instCompleteLattice {P : Type u_1} [] [] :
Equations
• Order.Ideal.instCompleteLattice = let __src := inferInstance; let __src_1 := ; CompleteLattice.mk β― β― β― β― β― β―
theorem Order.Ideal.eq_sup_of_le_sup {P : Type u_1} [] {I : } {J : } {x : P} {i : P} {j : P} (hi : i β I) (hj : j β J) (hx : x β€ i β j) :
β i' β I, β j' β J, x = i' β j'
theorem Order.Ideal.coe_sup_eq {P : Type u_1} [] {I : } {J : } :
β(I β J) = {x : P | β i β I, β j β J, x = i β j}
theorem Order.Ideal.IsProper.not_mem_of_compl_mem {P : Type u_1} [] {x : P} {I : } (hI : I.IsProper) (hxc : xαΆ β I) :
x β I
theorem Order.Ideal.IsProper.not_mem_or_compl_not_mem {P : Type u_1} [] {x : P} {I : } (hI : I.IsProper) :
x β I β¨ xαΆ β I
structure Order.Cofinal (P : Type u_2) [] :
Type u_2

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.

• carrier : Set P

The carrier of a Cofinal is the underlying set.

• mem_gt : β (x : P), β y β self.carrier, x β€ y

The Cofinal contains arbitrarily large elements.

Instances For
theorem Order.Cofinal.mem_gt {P : Type u_2} [] (self : ) (x : P) :
β y β self.carrier, x β€ y

The Cofinal contains arbitrarily large elements.

instance Order.Cofinal.instInhabited {P : Type u_1} [] :
Equations
• Order.Cofinal.instInhabited = { default := { carrier := Set.univ, mem_gt := β― } }
instance Order.Cofinal.instMembership {P : Type u_1} [] :
Equations
• Order.Cofinal.instMembership = { mem := fun (x : P) (D : ) => x β D.carrier }
noncomputable def Order.Cofinal.above {P : Type u_1} [] (D : ) (x : P) :
P

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

Equations
• D.above x =
Instances For
theorem Order.Cofinal.above_mem {P : Type u_1} [] (D : ) (x : P) :
D.above x β D
theorem Order.Cofinal.le_above {P : Type u_1} [] (D : ) (x : P) :
x β€ D.above x
noncomputable def Order.sequenceOfCofinals {P : Type u_1} [] (p : P) {ΞΉ : Type u_2} [] (π : ΞΉ β ) :
β β P

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

Equations
Instances For
theorem Order.sequenceOfCofinals.monotone {P : Type u_1} [] (p : P) {ΞΉ : Type u_2} [] (π : ΞΉ β ) :
theorem Order.sequenceOfCofinals.encode_mem {P : Type u_1} [] (p : P) {ΞΉ : Type u_2} [] (π : ΞΉ β ) (i : ΞΉ) :
Order.sequenceOfCofinals p π () β π i
def Order.idealOfCofinals {P : Type u_1} [] (p : P) {ΞΉ : Type u_2} [] (π : ΞΉ β ) :

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 to mem_idealOfCofinals p π, and
• intersects every set in π, according to cofinal_meets_idealOfCofinals p π.

This proves the RasiowaβSikorski lemma.

Equations
Instances For
theorem Order.mem_idealOfCofinals {P : Type u_1} [] (p : P) {ΞΉ : Type u_2} [] (π : ΞΉ β ) :
theorem Order.cofinal_meets_idealOfCofinals {P : Type u_1} [] (p : P) {ΞΉ : Type u_2} [] (π : ΞΉ β ) (i : ΞΉ) :
β x β π i, x β

idealOfCofinals p π is π-generic.

theorem Order.isIdeal_sUnion_of_directedOn {P : Type u_1} [] {C : Set (Set P)} (hidl : β I β C, ) (hD : DirectedOn (fun (x x_1 : Set P) => x β x_1) C) (hNe : C.Nonempty) :

A non-empty directed union of ideals of sets in a preorder is an ideal.

theorem Order.isIdeal_sUnion_of_isChain {P : Type u_1} [] {C : Set (Set P)} (hidl : β I β C, ) (hC : IsChain (fun (x x_1 : Set P) => x β x_1) C) (hNe : C.Nonempty) :

A union of a nonempty chain of ideals of sets is an ideal.