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.

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.
ideal_Inter_nonempty P: a predicate for when the intersection of all ideals of P is nonempty.
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.

TODO #

order.ideal.ideal_Inter_nonempty is a complicated way to say that P has a bottom element. It should be replaced by this clearer condition, which could be called strong directedness and which is a Prop version of order_bot.

Tags #

ideal, cofinal, dense, countable, generic

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

Type u_2

carrier : set P
nonempty : self.carrier.nonempty
directed : directed_on has_le.le self.carrier
mem_of_le : ∀ {x y : P}, x ≤ y → y ∈ self.carrier → x ∈ self.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).

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

Prop

nonempty : I.nonempty
directed : directed_on has_le.le I
mem_of_le : ∀ {x y : P}, x ≤ y → y ∈ I → x ∈ 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).

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

order.is_ideal I ↔ I.nonempty ∧ directed_on has_le.le I ∧ ∀ {x y : P}, x ≤ y → y ∈ I → x ∈ I

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

h.to_ideal = {carrier := I, nonempty := _, directed := _, mem_of_le := _}

@[protected, instance]

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

has_coe (order.ideal P) (set P)

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

Equations

order.ideal.set.has_coe = {coe := order.ideal.carrier _inst_1}

@[protected, instance]

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

has_mem P (order.ideal P)

For the notation x ∈ I.

Equations

order.ideal.has_mem = {mem := λ (x : P) (I : order.ideal P), x ∈ ↑I}

@[simp]

theorem order.ideal.mem_coe {P : Type u_1} [has_le P] {I : order.ideal P} {x : P} :

x ∈ ↑I ↔ x ∈ I

@[ext]

theorem order.ideal.ext {P : Type u_1} [has_le P] {I J : order.ideal P} :

↑I = ↑J → I = J

Two ideals are equal when their underlying sets are equal.

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

function.injective coe

@[simp, norm_cast]

theorem order.ideal.coe_inj {P : Type u_1} [has_le P] {I J : order.ideal P} :

↑I = ↑J ↔ I = J

theorem order.ideal.ext_iff {P : Type u_1} [has_le P] {I J : order.ideal P} :

I = J ↔ ↑I = ↑J

@[protected]

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

order.is_ideal ↑I

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

theorem order.ideal.mem_of_mem_of_le {P : Type u_1} [has_le P] {I J : order.ideal P} {x : 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 : ↑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

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

I.is_proper ↔ ↑I ≠ set.univ

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

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

order.ideal.is_prime.is_maximal

@[class]

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

Prop

Inter_nonempty : (⋂ (I : order.ideal P), ↑I).nonempty

An order P has the ideal_Inter_nonempty property if the intersection of all ideals is nonempty. Most importantly, the ideals of a semilattice_sup with this property form a complete lattice.

TODO: This is equivalent to the existence of a bottom element and shouldn't be specialized to ideals.

Instances

order.ideal.order_bot.ideal_Inter_nonempty

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

(⋂ (I : order.ideal P), ↑I).nonempty

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

∃ (a : P), ∀ (I : order.ideal P), a ∈ I

theorem order.ideal.ideal_Inter_nonempty_of_exists_all_mem {P : Type u_1} [has_le P] (h : ∃ (a : P), ∀ (I : order.ideal P), a ∈ I) :

order.ideal.ideal_Inter_nonempty P

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

order.ideal.ideal_Inter_nonempty P ↔ ∃ (a : P), ∀ (I : order.ideal P), a ∈ I

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

(↑I ∩ ↑J).nonempty

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

The smallest ideal containing a given element.

Equations

order.ideal.principal p = {carrier := {x : P | x ≤ p}, nonempty := _, directed := _, mem_of_le := _}

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

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

@[simp]

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

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

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

x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ

@[simp]

theorem order.ideal.bot_mem {P : Type u_1} [has_le P] [order_bot P] {I : order.ideal P} :

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

@[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 := _}

@[protected, instance]

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

order.ideal.ideal_Inter_nonempty P

@[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 set.univ.

Equations

order.ideal.order_top = {top := {carrier := set.univ P, nonempty := _, directed := _, mem_of_le := _}, le_top := _}

@[simp]

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

↑⊤ = set.univ

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

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

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

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

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

theorem order.ideal.top_of_top_mem {P : Type u_1} [has_le P] [order_top P] {I : order.ideal P} (hI : ⊤ ∈ 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) :

theorem order.ideal.sup_mem {P : Type u_1} [semilattice_sup P] {I : order.ideal P} (x : P) (H : x ∈ I) (y : P) (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

@[protected, instance]

def order.ideal.has_inf {P : Type u_1} [semilattice_sup P] [is_directed P (function.swap has_le.le)] :

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), {carrier := ↑I ∩ ↑J, nonempty := _, directed := _, mem_of_le := _}}

@[protected, instance]

def order.ideal.has_sup {P : Type u_1} [semilattice_sup P] [is_directed P (function.swap has_le.le)] :

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), {carrier := {x : P | ∃ (i : P) (H : i ∈ I) (j : P) (H : j ∈ J), x ≤ i ⊔ j}, nonempty := _, directed := _, mem_of_le := _}}

@[protected, instance]

def order.ideal.lattice {P : Type u_1} [semilattice_sup P] [is_directed P (function.swap has_le.le)] :

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 := _}

@[simp]

theorem order.ideal.mem_inf {P : Type u_1} [semilattice_sup P] [is_directed P (function.swap has_le.le)] {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 (function.swap has_le.le)] {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 (function.swap has_le.le)] {x : P} {I : order.ideal P} (hx : x ∉ I) :

I < I ⊔ order.ideal.principal x

@[protected, instance]

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

is_directed P (function.swap has_le.le)

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

@[protected, instance]

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

has_Inf (order.ideal P)

Equations

order.ideal.has_Inf = {Inf := λ (s : set (order.ideal P)), {carrier := ⋂ (I : order.ideal P) (H : I ∈ s), ↑I, nonempty := _, directed := _, mem_of_le := _}}

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

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 ∈ s → I ≤ J) :

theorem order.ideal.is_glb_Inf {P : Type u_1} [semilattice_sup P] [order.ideal.ideal_Inter_nonempty P] {s : set (order.ideal P)} :

is_glb s (Inf s)

@[protected, instance]

def order.ideal.complete_lattice {P : Type u_1} [semilattice_sup P] [order.ideal.ideal_Inter_nonempty 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 := _}

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.

@[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 := _}}

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

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

D.above x = classical.some _

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

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 (some i) = («𝒟» i).above _f_2
order.sequence_of_cofinals._match_1 «𝒟» _f_1 _f_2 none = _f_1

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 «𝒟»)

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

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

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

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 «𝒟»

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.