mathlib documentation

order.ideal

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.

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

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).
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] :
Equations
@[ext]
theorem order.ideal.ext {P : Type u_1} [has_le P] {s t : order.ideal P} :
s = ts = 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 yx (I)y (I)
@[protected, instance]

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 II Jx J
@[class]
structure order.ideal.is_proper {P : Type u_1} [has_le P] (I : order.ideal P) :
Prop

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 : order.ideal P⦄, I < JJ = set.univ
@[class]
structure order.ideal.is_maximal {P : Type u_1} [has_le P] (I : order.ideal P) :
Prop

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] [is_directed P ge] (I J : order.ideal P) :
@[protected, instance]

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

Equations
@[simp]
theorem order.ideal.coe_top {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] :
theorem order.ideal.is_proper_of_ne_top {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] {I : order.ideal P} (ne_top : I ) :
theorem order.ideal.is_proper.ne_top {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] {I : order.ideal P} (hI : I.is_proper) :
theorem is_coatom.is_proper {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] {I : order.ideal P} (hI : is_coatom I) :
theorem is_coatom.is_maximal {P : Type u_1} [has_le P] [is_directed P has_le.le] [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_le_iff {P : Type u_1} [preorder P] {I : order.ideal P} {x : P} :
@[simp]
theorem order.ideal.mem_principal {P : Type u_1} [preorder P] {x y : P} :
@[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]
@[simp]
theorem order.ideal.sup_mem {P : Type u_1} [semilattice_sup P] {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} [semilattice_sup P] {x y : P} {I : order.ideal P} :
x y I x I y I
@[protected, instance]

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

Equations
@[protected, instance]

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
@[simp]
theorem order.ideal.coe_sup {P : Type u_1} [semilattice_sup P] [is_directed P 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} [semilattice_sup P] [is_directed P ge] {s t : order.ideal P} :
(s t) = s t
@[simp]
theorem order.ideal.mem_inf {P : Type u_1} [semilattice_sup P] [is_directed P 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} [semilattice_sup P] [is_directed P 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} [semilattice_sup P] [is_directed P ge] {x : P} {I : order.ideal P} (hx : x I) :
@[protected, instance]
Equations
@[simp]
theorem order.ideal.coe_Inf {P : Type u_1} [semilattice_sup P] [order_bot P] {S : set (order.ideal P)} :
(has_Inf.Inf S) = ⋂ (s : order.ideal P) (H : s S), s
@[simp]
theorem order.ideal.mem_Inf {P : Type u_1} [semilattice_sup P] [order_bot P] {x : P} {S : set (order.ideal P)} :
x has_Inf.Inf S ∀ (s : order.ideal P), s Sx s
@[protected, instance]
Equations
theorem order.ideal.eq_sup_of_le_sup {P : Type u_1} [distrib_lattice P] {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} [distrib_lattice P] {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} [boolean_algebra P] {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} [boolean_algebra P] {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
  • carrier : set P
  • mem_gt : ∀ (x : P), ∃ (y : P) (H : y self.carrier), x y

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]
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 ι] (𝒟 : ι → order.cofinal P) :
→ P

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

Equations
theorem order.sequence_of_cofinals.monotone {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → order.cofinal P) :
theorem order.sequence_of_cofinals.encode_mem {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → order.cofinal P) (i : ι) :
def order.ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → order.cofinal P) :

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

ideal_of_cofinals p 𝒟 is 𝒟-generic.