order.ideal

# 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 of P. Dual to the notion of a filter on a preorder.
• order.is_ideal P: a predicate for when a set P is an ideal.
• order.ideal.principal p: the principal ideal generated by p : 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 of P containing arbitrarily large elements. Dual to the notion of 'dense set' used in forcing.
• order.ideal_of_cofinals 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) [has_le P] :
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).
Instances for order.ideal
structure order.is_ideal {P : Type u_2} [has_le P] (I : set P) :
Prop
• is_lower_set :
• nonempty : I.nonempty
• 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).
theorem order.is_ideal_iff {P : Type u_2} [has_le P] (I : set P) :
def order.is_ideal.to_ideal {P : Type u_1} [has_le P] {I : set P} (h : order.is_ideal I) :

Create an element of type order.ideal from a set satisfying the predicate order.is_ideal.

Equations
@[protected, instance]
def order.ideal.set_like {P : Type u_1} [has_le P] :
P
Equations
@[ext]
theorem order.ideal.ext {P : Type u_1} [has_le P] {s t : order.ideal P} :
s = t s = t
@[simp]
theorem order.ideal.carrier_eq_coe {P : Type u_1} [has_le P] (s : order.ideal P) :
@[simp]
theorem order.ideal.coe_to_lower_set {P : Type u_1} [has_le P] (s : order.ideal P) :
@[protected]
theorem order.ideal.lower {P : Type u_1} [has_le P] (s : order.ideal P) :
@[protected]
theorem order.ideal.nonempty {P : Type u_1} [has_le P] (s : order.ideal P) :
@[protected]
theorem order.ideal.directed {P : Type u_1} [has_le P] (s : order.ideal P) :
@[protected]
theorem order.ideal.is_ideal {P : Type u_1} [has_le P] (s : order.ideal P) :
theorem order.ideal.mem_compl_of_ge {P : Type u_1} [has_le P] {I : order.ideal P} {x y : P} :
x y x (I) y (I)
@[protected, instance]
def order.ideal.partial_order {P : Type u_1} [has_le P] :

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

Equations
@[simp]
theorem order.ideal.coe_subset_coe {P : Type u_1} [has_le P] {s t : order.ideal P} :
s t s t
@[simp]
theorem order.ideal.coe_ssubset_coe {P : Type u_1} [has_le P] {s t : order.ideal P} :
s t s < t
@[trans]
theorem order.ideal.mem_of_mem_of_le {P : Type u_1} [has_le P] {x : P} {I J : order.ideal P} :
x I I J x J
@[class]
structure order.ideal.is_proper {P : Type u_1} [has_le P] (I : order.ideal P) :
Prop
• ne_univ :

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
theorem order.ideal.is_proper_iff {P : Type u_1} [has_le P] (I : order.ideal P) :
theorem order.ideal.is_proper_of_not_mem {P : Type u_1} [has_le P] {I : order.ideal P} {p : P} (nmem : p I) :
theorem order.ideal.is_maximal_iff {P : Type u_1} [has_le P] (I : order.ideal P) :
I.is_maximal I.is_proper ⦃J : ⦄, I < J
@[class]
structure order.ideal.is_maximal {P : Type u_1} [has_le P] (I : order.ideal P) :
Prop
• to_is_proper :
• maximal_proper : ⦃J : ⦄, I < J

An ideal is maximal if it is maximal in the collection of proper ideals.

Note that is_coatom is less general because ideals only have a top element when P is directed and nonempty.

Instances of this typeclass
theorem order.ideal.inter_nonempty {P : Type u_1} [has_le P] [ ge] (I J : order.ideal P) :
@[protected, instance]
def order.ideal.order_top {P : Type u_1} [has_le P] [nonempty P] :

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

Equations
@[simp]
theorem order.ideal.top_to_lower_set {P : Type u_1} [has_le P] [nonempty P] :
@[simp]
theorem order.ideal.coe_top {P : Type u_1} [has_le P] [nonempty P] :
theorem order.ideal.is_proper_of_ne_top {P : Type u_1} [has_le P] [nonempty P] {I : order.ideal P} (ne_top : I ) :
theorem order.ideal.is_proper.ne_top {P : Type u_1} [has_le P] [nonempty P] {I : order.ideal P} (hI : I.is_proper) :
theorem is_coatom.is_proper {P : Type u_1} [has_le P] [nonempty P] {I : order.ideal P} (hI : is_coatom I) :
theorem order.ideal.is_maximal.is_coatom {P : Type u_1} [has_le P] [nonempty P] {I : order.ideal P} (h : I.is_maximal) :
theorem is_coatom.is_maximal {P : Type u_1} [has_le P] [nonempty P] {I : order.ideal P} (hI : is_coatom I) :
@[simp]
theorem order.ideal.bot_mem {P : Type u_1} [has_le P] [order_bot P] (s : order.ideal P) :
theorem order.ideal.top_of_top_mem {P : Type u_1} [has_le P] [order_top P] {I : order.ideal P} (h : I) :
I =
theorem order.ideal.is_proper.top_not_mem {P : Type u_1} [has_le P] [order_top P] {I : order.ideal P} (hI : I.is_proper) :
def order.ideal.principal {P : Type u_1} [preorder P] (p : P) :

The smallest ideal containing a given element.

Equations
@[simp]
theorem order.ideal.principal_to_lower_set {P : Type u_1} [preorder P] (p : P) :
@[protected, instance]
def order.ideal.inhabited {P : Type u_1} [preorder P] [inhabited P] :
Equations
@[simp]
theorem order.ideal.principal_le_iff {P : Type u_1} [preorder P] {I : order.ideal P} {x : P} :
x I
@[simp]
theorem order.ideal.mem_principal {P : Type u_1} [preorder P] {x y : P} :
x y
@[protected, instance]
def order.ideal.order_bot {P : Type u_1} [preorder P] [order_bot P] :

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

Equations
@[simp]
theorem order.ideal.principal_bot {P : Type u_1} [preorder P] [order_bot P] :
@[simp]
theorem order.ideal.principal_top {P : Type u_1} [preorder P] [order_top P] :
theorem order.ideal.sup_mem {P : Type u_1} {x y : P} {s : order.ideal P} (hx : x s) (hy : y s) :
x y s

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

@[simp]
theorem order.ideal.sup_mem_iff {P : Type u_1} {x y : P} {I : order.ideal P} :
x y I x I y I
@[protected, instance]
def order.ideal.has_inf {P : Type u_1} [ ge] :

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

Equations
@[protected, instance]
def order.ideal.has_sup {P : Type u_1} [ ge] :

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
@[protected, instance]
def order.ideal.lattice {P : Type u_1} [ ge] :
Equations
@[simp]
theorem order.ideal.coe_sup {P : Type u_1} [ ge] {s t : order.ideal P} :
(s t) = {x : P | (a : P) (H : a s) (b : P) (H : b t), x a b}
@[simp]
theorem order.ideal.coe_inf {P : Type u_1} [ ge] {s t : order.ideal P} :
(s t) = s t
@[simp]
theorem order.ideal.mem_inf {P : Type u_1} [ ge] {x : P} {I J : order.ideal P} :
x I J x I x J
@[simp]
theorem order.ideal.mem_sup {P : Type u_1} [ ge] {x : P} {I J : order.ideal P} :
x I J (i : P) (H : i I) (j : P) (H : j J), x i j
theorem order.ideal.lt_sup_principal_of_not_mem {P : Type u_1} [ ge] {x : P} {I : order.ideal P} (hx : x I) :
I <
@[protected, instance]
def order.ideal.has_Inf {P : Type u_1} [order_bot P] :
Equations
@[simp]
theorem order.ideal.coe_Inf {P : Type u_1} [order_bot P] {S : set (order.ideal P)} :
(has_Inf.Inf S) = (s : (H : s S), s
@[simp]
theorem order.ideal.mem_Inf {P : Type u_1} [order_bot P] {x : P} {S : set (order.ideal P)} :
x (s : , s S x s
@[protected, instance]
Equations
theorem order.ideal.eq_sup_of_le_sup {P : Type u_1} {I J : order.ideal P} {x i j : P} (hi : i I) (hj : j J) (hx : x i j) :
(i' : P) (H : i' I) (j' : P) (H : j' J), x = i' j'
theorem order.ideal.coe_sup_eq {P : Type u_1} {I J : order.ideal P} :
(I J) = {x : P | (i : P) (H : i I) (j : P) (H : j J), x = i j}
theorem order.ideal.is_proper.not_mem_of_compl_mem {P : Type u_1} {x : P} {I : order.ideal P} (hI : I.is_proper) (hxc : x I) :
x I
theorem order.ideal.is_proper.not_mem_or_compl_not_mem {P : Type u_1} {x : P} {I : order.ideal P} (hI : I.is_proper) :
x I x I
structure order.cofinal (P : Type u_2) [preorder P] :
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.

Instances for order.cofinal
@[protected, instance]
def order.cofinal.inhabited {P : Type u_1} [preorder P] :
Equations
@[protected, instance]
def order.cofinal.has_mem {P : Type u_1} [preorder P] :
Equations
noncomputable def order.cofinal.above {P : Type u_1} [preorder P] (D : order.cofinal P) (x : P) :
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
noncomputable def order.sequence_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι ) :

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

Equations
• (n + 1) = order.sequence_of_cofinals._match_1 𝒟 n) n) n)
• = 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
theorem order.sequence_of_cofinals.monotone {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι ) :
theorem order.sequence_of_cofinals.encode_mem {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι ) (i : ι) :
+ 1) 𝒟 i
def order.ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι ) :

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 ι] (𝒟 : ι ) :
theorem order.cofinal_meets_ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι ) (i : ι) :
(x : P), x 𝒟 i

ideal_of_cofinals p 𝒟 is 𝒟-generic.