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) [preorder P] :
Type u_2

An ideal on a preorder 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).
structure order.is_ideal {P : Type u_2} [preorder 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).
theorem order.is_ideal_iff {P : Type u_2} [preorder P] (I : set P) :
order.is_ideal I I.nonempty directed_on has_le.le I ∀ {x y : P}, x yy Ix I
def order.is_ideal.to_ideal {P : Type u_1} [preorder 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
def order.ideal.principal {P : Type u_1} [preorder P] (p : P) :

The smallest ideal containing a given element.

Equations
@[instance]
def order.ideal.set.has_coe {P : Type u_1} [preorder P] :

An ideal of P can be viewed as a subset of P.

Equations
@[instance]
def order.ideal.has_mem {P : Type u_1} [preorder P] :

For the notation x ∈ I.

Equations
@[simp]
theorem order.ideal.mem_coe {P : Type u_1} [preorder P] {x : P} {I : order.ideal P} :
x I x I
@[simp]
theorem order.ideal.mem_principal {P : Type u_1} [preorder P] {x y : P} :
@[ext]
theorem order.ideal.ext {P : Type u_1} [preorder P] (I J : order.ideal P) :
I = JI = J

Two ideals are equal when their underlying sets are equal.

@[simp]
theorem order.ideal.ext_set_eq {P : Type u_1} [preorder P] {I J : order.ideal P} :
I = J I = J
theorem order.ideal.ext'_iff {P : Type u_1} [preorder P] {I J : order.ideal P} :
I = J I = J
theorem order.ideal.is_ideal {P : Type u_1} [preorder P] (I : order.ideal P) :
@[instance]

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

Equations
theorem order.ideal.mem_of_mem_of_le {P : Type u_1} [preorder P] {x : P} {I J : order.ideal P} :
x II Jx J
@[simp]
theorem order.ideal.principal_le_iff {P : Type u_1} [preorder P] {x : P} {I : order.ideal P} :
theorem order.ideal.mem_compl_of_ge {P : Type u_1} [preorder P] {I : order.ideal P} {x y : P} :
x yx (I)y (I)
@[class]
structure order.ideal.is_proper {P : Type u_1} [preorder 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
theorem order.ideal.is_proper_iff {P : Type u_1} [preorder P] (I : order.ideal P) :
theorem order.ideal.is_proper_of_not_mem {P : Type u_1} [preorder P] {I : order.ideal P} {p : P} (nmem : p I) :
theorem order.ideal.is_maximal_iff {P : Type u_1} [preorder 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} [preorder P] (I : order.ideal P) :
Prop

An ideal is maximal if it is maximal in the collection of proper ideals. Note that we cannot use the is_coatom class because P might not have a top element.

Instances
@[class]
structure order.ideal.ideal_inter_nonempty (P : Type u_1) [preorder P] :
Prop

A preorder P has the ideal_inter_nonempty property if the intersection of any two ideals is nonempty. Most importantly, a semilattice_sup preorder with this property satisfies that its ideal poset is a lattice.

Instances
@[class]
structure order.ideal.ideal_Inter_nonempty (P : Type u_1) [preorder P] :
Prop

A preorder P has the ideal_Inter_nonempty property if the intersection of all ideals is nonempty. Most importantly, a semilattice_sup preorder with this property satisfies that its ideal poset is a complete lattice.

Instances
theorem order.ideal.ideal_Inter_nonempty_of_exists_all_mem {P : Type u_1} [preorder P] (h : ∃ (a : P), ∀ (I : order.ideal P), a I) :
theorem order.ideal.ideal_Inter_nonempty_iff {P : Type u_1} [preorder P] :
order.ideal.ideal_Inter_nonempty P ∃ (a : P), ∀ (I : order.ideal P), a I
@[simp]
theorem order.ideal.bot_mem {P : Type u_1} [order_bot P] {I : order.ideal P} :

A specific witness of I.nonempty when P has a bottom element.

@[instance]
def order.ideal.order_bot {P : Type u_1} [order_bot P] :

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

Equations
@[instance]
def order.ideal.order_top {P : Type u_1} [order_top P] :

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

Equations
@[simp]
theorem order.ideal.coe_top {P : Type u_1} [order_top P] :
theorem order.ideal.top_of_mem_top {P : Type u_1} [order_top P] {I : order.ideal P} (mem_top : I) :
I =
theorem order.ideal.is_proper_of_ne_top {P : Type u_1} [order_top P] {I : order.ideal P} (ne_top : I ) :
theorem order.ideal.is_proper.ne_top {P : Type u_1} [order_top P] {I : order.ideal P} (hI : I.is_proper) :
theorem order.ideal.is_proper.top_not_mem {P : Type u_1} [order_top P] {I : order.ideal P} (hI : I.is_proper) :
theorem is_coatom.is_proper {P : Type u_1} [order_top P] {I : order.ideal P} (hI : is_coatom I) :
theorem order.ideal.is_proper_iff_ne_top {P : Type u_1} [order_top P] {I : order.ideal P} :
theorem order.ideal.is_maximal.is_coatom {P : Type u_1} [order_top P] {I : order.ideal P} (h : I.is_maximal) :
theorem is_coatom.is_maximal {P : Type u_1} [order_top P] {I : order.ideal P} (hI : is_coatom I) :
theorem order.ideal.sup_mem {P : Type u_1} [semilattice_sup P] {I : order.ideal P} (x y : P) (H : x I) (H_1 : y I) :
x y I

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

The intersection of two ideals is an ideal, when it is nonempty and P has joins.

Equations

There is a smallest ideal containing two ideals, when their intersection is nonempty and P has joins.

Equations
theorem order.ideal.sup_le {P : Type u_1} [semilattice_sup P] [order.ideal.ideal_inter_nonempty P] {I J K : order.ideal P} :
I KJ KI.sup J K
@[simp]
theorem order.ideal.mem_inf {P : Type u_1} [semilattice_sup P] [order.ideal.ideal_inter_nonempty P] {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] [order.ideal.ideal_inter_nonempty P] {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.ideal_Inter_nonempty.all_Inter_nonempty {P : Type u_1} [preorder P] [order.ideal.ideal_Inter_nonempty P] {ι : Sort u_5} {f : ι → order.ideal P} :
(⋂ (x : ι), (f x)).nonempty
theorem order.ideal.ideal_Inter_nonempty.all_bInter_nonempty {P : Type u_1} [preorder P] [order.ideal.ideal_Inter_nonempty P] {α : Type u_2} {f : α → order.ideal P} {s : set α} :
(⋂ (x : α) (H : x s), (f x)).nonempty
@[instance]
Equations
@[simp]
theorem order.ideal.mem_Inf {P : Type u_1} [semilattice_sup P] [order.ideal.ideal_Inter_nonempty P] {x : P} {s : set (order.ideal P)} :
x Inf s ∀ (I : order.ideal P), I sx I
@[simp]
theorem order.ideal.coe_Inf {P : Type u_1} [semilattice_sup P] [order.ideal.ideal_Inter_nonempty P] {s : set (order.ideal P)} :
(Inf s) = ⋂ (I : order.ideal P) (H : I s), I
theorem order.ideal.Inf_le {P : Type u_1} [semilattice_sup P] [order.ideal.ideal_Inter_nonempty P] {I : order.ideal P} {s : set (order.ideal P)} (hI : I s) :
Inf s I
theorem order.ideal.le_Inf {P : Type u_1} [semilattice_sup P] [order.ideal.ideal_Inter_nonempty P] {I : order.ideal P} {s : set (order.ideal P)} (h : ∀ (J : order.ideal P), J sI J) :
I Inf s
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.

@[instance]
Equations
@[instance]
def order.cofinal.has_mem {P : Type u_1} [preorder P] :
Equations
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
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.