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

source

structure order.ideal (P : Type u_2) [has_le P] :

Type u_2

to_lower_set : lower_set P
nonempty' : self.to_lower_set.carrier.nonempty
directed' : directed_on has_le.le self.to_lower_set.carrier

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

source

structure order.is_ideal {P : Type u_2} [has_le P] (I : set P) :

Prop

is_lower_set : is_lower_set I
nonempty : I.nonempty
directed : directed_on has_le.le I

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).

source

theorem order.is_ideal_iff {P : Type u_2} [has_le P] (I : set P) :

order.is_ideal I ↔ is_lower_set I ∧ I.nonempty ∧ directed_on has_le.le I

source

def order.is_ideal.to_ideal {P : Type u_1} [has_le P] {I : set P} (h : order.is_ideal I) :

order.ideal P

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

Equations

h.to_ideal = {to_lower_set := {carrier := I, lower' := _}, nonempty' := _, directed' := _}

source

theorem order.ideal.to_lower_set_injective {P : Type u_1} [has_le P] :

function.injective order.ideal.to_lower_set

source

@[protected, instance]

def order.ideal.set_like {P : Type u_1} [has_le P] :

set_like (order.ideal P) P

Equations

order.ideal.set_like = {coe := λ (s : order.ideal P), s.to_lower_set.carrier, coe_injective' := _}

source

@[ext]

theorem order.ideal.ext {P : Type u_1} [has_le P] {s t : order.ideal P} :

↑s = ↑t → s = t

source

@[simp]

theorem order.ideal.carrier_eq_coe {P : Type u_1} [has_le P] (s : order.ideal P) :

s.to_lower_set.carrier = ↑s

source

@[simp]

theorem order.ideal.coe_to_lower_set {P : Type u_1} [has_le P] (s : order.ideal P) :

↑(s.to_lower_set) = ↑s

source

@[protected]

theorem order.ideal.lower {P : Type u_1} [has_le P] (s : order.ideal P) :

is_lower_set ↑s

source

@[protected]

theorem order.ideal.nonempty {P : Type u_1} [has_le P] (s : order.ideal P) :

↑s.nonempty

source

@[protected]

theorem order.ideal.directed {P : Type u_1} [has_le P] (s : order.ideal P) :

directed_on has_le.le ↑s

source

@[protected]

theorem order.ideal.is_ideal {P : Type u_1} [has_le P] (s : order.ideal P) :

order.is_ideal ↑s

source

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)ᶜ

source

@[protected, instance]

def order.ideal.partial_order {P : Type u_1} [has_le P] :

partial_order (order.ideal P)

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

Equations

order.ideal.partial_order = partial_order.lift coe order.ideal.partial_order._proof_1

source

@[simp]

theorem order.ideal.coe_subset_coe {P : Type u_1} [has_le P] {s t : order.ideal P} :

↑s ⊆ ↑t ↔ s ≤ t

source

@[simp]

theorem order.ideal.coe_ssubset_coe {P : Type u_1} [has_le P] {s t : order.ideal P} :

↑s ⊂ ↑t ↔ s < t

source

@[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

source

@[class]

structure order.ideal.is_proper {P : Type u_1} [has_le P] (I : order.ideal P) :

Prop

ne_univ : ↑I ≠ set.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

source

theorem order.ideal.is_proper_iff {P : Type u_1} [has_le P] (I : order.ideal P) :

I.is_proper ↔ ↑I ≠ set.univ

source

theorem order.ideal.is_proper_of_not_mem {P : Type u_1} [has_le P] {I : order.ideal P} {p : P} (nmem : p ∉ I) :

I.is_proper

source

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 < J → ↑J = set.univ

source

@[class]

structure order.ideal.is_maximal {P : Type u_1} [has_le P] (I : order.ideal P) :

Prop

to_is_proper : I.is_proper
maximal_proper : ∀ ⦃J : order.ideal P⦄, I < J → ↑J = set.univ

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

order.ideal.is_prime.is_maximal

source

theorem order.ideal.inter_nonempty {P : Type u_1} [has_le P] [is_directed P ge] (I J : order.ideal P) :

(↑I ∩ ↑J).nonempty

source

@[protected, instance]

def order.ideal.order_top {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] :

order_top (order.ideal P)

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

Equations

order.ideal.order_top = {top := {to_lower_set := ⊤, nonempty' := _, directed' := _}, le_top := _}

source

@[simp]

theorem order.ideal.top_to_lower_set {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] :

⊤.to_lower_set = ⊤

source

@[simp]

theorem order.ideal.coe_top {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] :

↑⊤ = set.univ

source

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 ≠ ⊤) :

I.is_proper

source

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) :

I ≠ ⊤

source

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) :

I.is_proper

source

theorem order.ideal.is_proper_iff_ne_top {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] {I : order.ideal P} :

I.is_proper ↔ I ≠ ⊤

source

theorem order.ideal.is_maximal.is_coatom {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] {I : order.ideal P} (h : I.is_maximal) :

is_coatom I

source

theorem order.ideal.is_maximal.is_coatom' {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] {I : order.ideal P} [I.is_maximal] :

is_coatom I

source

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) :

I.is_maximal

source

theorem order.ideal.is_maximal_iff_is_coatom {P : Type u_1} [has_le P] [is_directed P has_le.le] [nonempty P] {I : order.ideal P} :

I.is_maximal ↔ is_coatom I

source

@[simp]

theorem order.ideal.bot_mem {P : Type u_1} [has_le P] [order_bot P] (s : order.ideal P) :

⊥ ∈ s

source

theorem order.ideal.top_of_top_mem {P : Type u_1} [has_le P] [order_top P] {I : order.ideal P} (h : ⊤ ∈ I) :

I = ⊤

source

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) :

⊤ ∉ I

source

def order.ideal.principal {P : Type u_1} [preorder P] (p : P) :

order.ideal P

The smallest ideal containing a given element.

Equations

order.ideal.principal p = {to_lower_set := lower_set.Iic p, nonempty' := _, directed' := _}

source

@[simp]

theorem order.ideal.principal_to_lower_set {P : Type u_1} [preorder P] (p : P) :

(order.ideal.principal p).to_lower_set = lower_set.Iic p

source

@[protected, instance]

def order.ideal.inhabited {P : Type u_1} [preorder P] [inhabited P] :

inhabited (order.ideal P)

Equations

order.ideal.inhabited = {default := order.ideal.principal inhabited.default}

source

@[simp]

theorem order.ideal.principal_le_iff {P : Type u_1} [preorder P] {I : order.ideal P} {x : P} :

order.ideal.principal x ≤ I ↔ x ∈ I

source

@[simp]

theorem order.ideal.mem_principal {P : Type u_1} [preorder P] {x y : P} :

x ∈ order.ideal.principal y ↔ x ≤ y

source

@[protected, instance]

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

order_bot (order.ideal P)

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

Equations

order.ideal.order_bot = {bot := order.ideal.principal ⊥, bot_le := _}

source

@[simp]

theorem order.ideal.principal_bot {P : Type u_1} [preorder P] [order_bot P] :

order.ideal.principal ⊥ = ⊥

source

@[simp]

theorem order.ideal.principal_top {P : Type u_1} [preorder P] [order_top P] :

order.ideal.principal ⊤ = ⊤

source

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.

source

@[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

source

@[protected, instance]

def order.ideal.has_inf {P : Type u_1} [semilattice_sup P] [is_directed P ge] :

has_inf (order.ideal P)

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

Equations

order.ideal.has_inf = {inf := λ (I J : order.ideal P), {to_lower_set := I.to_lower_set ⊓ J.to_lower_set, nonempty' := _, directed' := _}}

source

@[protected, instance]

def order.ideal.has_sup {P : Type u_1} [semilattice_sup P] [is_directed P ge] :

has_sup (order.ideal P)

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.has_sup = {sup := λ (I J : order.ideal P), {to_lower_set := {carrier := {x : P | ∃ (i : P) (H : i ∈ I) (j : P) (H : j ∈ J), x ≤ i ⊔ j}, lower' := _}, nonempty' := _, directed' := _}}

source

@[protected, instance]

def order.ideal.lattice {P : Type u_1} [semilattice_sup P] [is_directed P ge] :

lattice (order.ideal P)

Equations

order.ideal.lattice = {sup := has_sup.sup order.ideal.has_sup, le := partial_order.le order.ideal.partial_order, lt := partial_order.lt order.ideal.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf order.ideal.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[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}

source

@[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

source

@[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

source

@[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

source

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) :

I < I ⊔ order.ideal.principal x

source

@[protected, instance]

def order.ideal.has_Inf {P : Type u_1} [semilattice_sup P] [order_bot P] :

has_Inf (order.ideal P)

Equations

order.ideal.has_Inf = {Inf := λ (S : set (order.ideal P)), {to_lower_set := ⨅ (s : order.ideal P) (H : s ∈ S), s.to_lower_set, nonempty' := _, directed' := _}}

source

@[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

source

@[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 ∈ S → x ∈ s

source

@[protected, instance]

def order.ideal.complete_lattice {P : Type u_1} [semilattice_sup P] [order_bot P] :

complete_lattice (order.ideal P)

Equations

order.ideal.complete_lattice = {sup := lattice.sup order.ideal.lattice, le := lattice.le order.ideal.lattice, lt := lattice.lt order.ideal.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf order.ideal.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (order.ideal P) order.ideal.complete_lattice._proof_12), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (order.ideal P) order.ideal.complete_lattice._proof_12), Inf_le := _, le_Inf := _, top := complete_lattice.top (complete_lattice_of_Inf (order.ideal P) order.ideal.complete_lattice._proof_12), bot := complete_lattice.bot (complete_lattice_of_Inf (order.ideal P) order.ideal.complete_lattice._proof_12), le_top := _, bot_le := _}

source

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'

source

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}

source

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

source

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

source

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

order.cofinal.has_sizeof_inst
order.cofinal.inhabited
order.cofinal.has_mem

source

@[protected, instance]

def order.cofinal.inhabited {P : Type u_1} [preorder P] :

inhabited (order.cofinal P)

Equations

order.cofinal.inhabited = {default := {carrier := set.univ P, mem_gt := _}}

source

@[protected, instance]

def order.cofinal.has_mem {P : Type u_1} [preorder P] :

has_mem P (order.cofinal P)

Equations

order.cofinal.has_mem = {mem := λ (x : P) (D : order.cofinal P), x ∈ D.carrier}

source

noncomputable def order.cofinal.above {P : Type u_1} [preorder P] (D : order.cofinal P) (x : P) :

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

Equations

D.above x = classical.some _

source

theorem order.cofinal.above_mem {P : Type u_1} [preorder P] (D : order.cofinal P) (x : P) :

D.above x ∈ D

source

theorem order.cofinal.le_above {P : Type u_1} [preorder P] (D : order.cofinal P) (x : P) :

x ≤ D.above x

source

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

order.sequence_of_cofinals p 𝒟 (n + 1) = order.sequence_of_cofinals._match_1 𝒟 (order.sequence_of_cofinals p 𝒟 n) (order.sequence_of_cofinals p 𝒟 n) (encodable.decode ι n)
order.sequence_of_cofinals p 𝒟 0 = 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

source

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

monotone (order.sequence_of_cofinals p 𝒟)

source

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

order.sequence_of_cofinals p 𝒟 (encodable.encode i + 1) ∈ 𝒟 i

source

def order.ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → order.cofinal P) :

order.ideal 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

order.ideal_of_cofinals p 𝒟 = {to_lower_set := {carrier := {x : P | ∃ (n : ℕ), x ≤ order.sequence_of_cofinals p 𝒟 n}, lower' := _}, nonempty' := _, directed' := _}

source

theorem order.mem_ideal_of_cofinals {P : Type u_1} [preorder P] (p : P) {ι : Type u_2} [encodable ι] (𝒟 : ι → order.cofinal P) :

p ∈ order.ideal_of_cofinals p 𝒟

source

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.