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.IsIdeal I: a predicate for when a Set P is an ideal.
• Order.Ideal.principal p: the principal ideal generated by p : P.
• Order.Ideal.IsProper I: a predicate for proper ideals. Dual to the notion of a proper filter.
• Order.Ideal.IsMaximal I: 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.idealOfCofinals 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

• https://en.wikipedia.org/wiki/Ideal_(order_theory)
• https://en.wikipedia.org/wiki/Cofinal_(mathematics)
• https://en.wikipedia.org/wiki/Rasiowa%E2%80%93Sikorski_lemma

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) [LE P] extends LowerSet 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).

• carrier : Set P
• lower' : IsLowerSet self.carrier
• nonempty' : self.carrier.Nonempty

  The ideal is nonempty.

• directed' : DirectedOn (fun (x1 x2 : P) => x1 ≤ x2) self.carrier

  The ideal is upward directed.

structure Order.IsIdeal {P : Type u_2} [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).

• IsLowerSet : _root_.IsLowerSet I

  The ideal is downward closed.

• Nonempty : I.Nonempty

  The ideal is nonempty.

• Directed : DirectedOn (fun (x1 x2 : P) => x1 ≤ x2) I

  The ideal is upward directed.

theorem Order.isIdeal_iff {P : Type u_2} [LE P] (I : Set P) : IsIdeal I ↔ IsLowerSet I ∧ I.Nonempty ∧ DirectedOn (fun (x1 x2 : P) => x1 ≤ x2) I

def Order.IsIdeal.toIdeal {P : Type u_1} [LE P] {I : Set P} (h : IsIdeal I) : Ideal P

Create an element of type Order.Ideal from a set satisfying the predicate Order.IsIdeal.

Equations

• h.toIdeal = { carrier := I, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }

theorem Order.Ideal.toLowerSet_injective {P : Type u_1} [LE P] : Function.Injective toLowerSet

instance Order.Ideal.instSetLike {P : Type u_1} [LE P] : SetLike (Ideal P) P

Equations

• Order.Ideal.instSetLike = { coe := fun (s : Order.Ideal P) => s.carrier, coe_injective' := ⋯ }

theorem Order.Ideal.ext {P : Type u_1} [LE P] {s t : Ideal P} : ↑s = ↑t → s = t

theorem Order.Ideal.ext_iff {P : Type u_1} [LE P] {s t : Ideal P} : s = t ↔ ↑s = ↑t

@[simp]

theorem Order.Ideal.carrier_eq_coe {P : Type u_1} [LE P] (s : Ideal P) : s.carrier = ↑s

@[simp]

theorem Order.Ideal.coe_toLowerSet {P : Type u_1} [LE P] (s : Ideal P) : ↑s.toLowerSet = ↑s

theorem Order.Ideal.lower {P : Type u_1} [LE P] (s : Ideal P) : IsLowerSet ↑s

theorem Order.Ideal.nonempty {P : Type u_1} [LE P] (s : Ideal P) : (↑s).Nonempty

theorem Order.Ideal.directed {P : Type u_1} [LE P] (s : Ideal P) : DirectedOn (fun (x1 x2 : P) => x1 ≤ x2) ↑s

theorem Order.Ideal.isIdeal {P : Type u_1} [LE P] (s : Ideal P) : IsIdeal ↑s

theorem Order.Ideal.mem_compl_of_ge {P : Type u_1} [LE P] {I : Ideal P} {x y : P} : x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ

instance Order.Ideal.instPartialOrderIdeal {P : Type u_1} [LE P] : PartialOrder (Ideal P)

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

Equations

• Order.Ideal.instPartialOrderIdeal = PartialOrder.lift SetLike.coe ⋯

theorem Order.Ideal.coe_subset_coe {P : Type u_1} [LE P] {s t : Ideal P} : ↑s ⊆ ↑t ↔ s ≤ t

theorem Order.Ideal.coe_ssubset_coe {P : Type u_1} [LE P] {s t : Ideal P} : ↑s ⊂ ↑t ↔ s < t

theorem Order.Ideal.mem_of_mem_of_le {P : Type u_1} [LE P] {x : P} {I J : Ideal P} : x ∈ I → I ≤ J → x ∈ J

class Order.Ideal.IsProper {P : Type u_1} [LE P] (I : Ideal P) : Prop

A proper ideal is one that is not the whole set. Note that the whole set might not be an ideal.

• ne_univ : ↑I ≠ Set.univ

  This ideal is not the whole set.

theorem Order.Ideal.isProper_iff {P : Type u_1} [LE P] (I : Ideal P) : I.IsProper ↔ ↑I ≠ Set.univ

theorem Order.Ideal.isProper_of_not_mem {P : Type u_1} [LE P] {I : Ideal P} {p : P} (nmem : p ∉ I) : I.IsProper

class Order.Ideal.IsMaximal {P : Type u_1} [LE P] (I : Ideal P) extends I.IsProper : Prop

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

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

• ne_univ : ↑I ≠ Set.univ
• maximal_proper ⦃J : Ideal P⦄ : I < J → ↑J = Set.univ

  This ideal is maximal in the collection of proper ideals.

theorem Order.Ideal.isMaximal_iff {P : Type u_1} [LE P] (I : Ideal P) : I.IsMaximal ↔ I.IsProper ∧ ∀ ⦃J : Ideal P⦄, I < J → ↑J = Set.univ

theorem Order.Ideal.inter_nonempty {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] (I J : Ideal P) : (↑I ∩ ↑J).Nonempty

instance Order.Ideal.instOrderTop {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] : OrderTop (Ideal P)

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

Equations

• Order.Ideal.instOrderTop = { top := { toLowerSet := ⊤, nonempty' := ⋯, directed' := ⋯ }, le_top := ⋯ }

@[simp]

theorem Order.Ideal.top_toLowerSet {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] : ⊤.toLowerSet = ⊤

@[simp]

theorem Order.Ideal.coe_top {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] : ↑⊤ = Set.univ

theorem Order.Ideal.isProper_of_ne_top {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] {I : Ideal P} (ne_top : I ≠ ⊤) : I.IsProper

theorem Order.Ideal.IsProper.ne_top {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] {I : Ideal P} : I.IsProper → I ≠ ⊤

theorem IsCoatom.isProper {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] {I : Order.Ideal P} (hI : IsCoatom I) : I.IsProper

theorem Order.Ideal.isProper_iff_ne_top {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] {I : Ideal P} : I.IsProper ↔ I ≠ ⊤

theorem Order.Ideal.IsMaximal.isCoatom {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] {I : Ideal P} : I.IsMaximal → IsCoatom I

theorem Order.Ideal.IsMaximal.isCoatom' {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] {I : Ideal P} [I.IsMaximal] : IsCoatom I

theorem IsCoatom.isMaximal {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] {I : Order.Ideal P} (hI : IsCoatom I) : I.IsMaximal

theorem Order.Ideal.isMaximal_iff_isCoatom {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≤ x2] [Nonempty P] {I : Ideal P} : I.IsMaximal ↔ IsCoatom I

@[simp]

theorem Order.Ideal.bot_mem {P : Type u_1} [LE P] [OrderBot P] (s : Ideal P) : ⊥ ∈ s

theorem Order.Ideal.top_of_top_mem {P : Type u_1} [LE P] [OrderTop P] {I : Ideal P} (h : ⊤ ∈ I) : I = ⊤

theorem Order.Ideal.IsProper.top_not_mem {P : Type u_1} [LE P] [OrderTop P] {I : Ideal P} (hI : I.IsProper) : ⊤ ∉ I

def Order.Ideal.principal {P : Type u_1} [Preorder P] (p : P) : Ideal P

The smallest ideal containing a given element.

Equations

• Order.Ideal.principal p = { toLowerSet := LowerSet.Iic p, nonempty' := ⋯, directed' := ⋯ }

@[simp]

theorem Order.Ideal.principal_toLowerSet {P : Type u_1} [Preorder P] (p : P) : (principal p).toLowerSet = LowerSet.Iic p

instance Order.Ideal.instInhabited {P : Type u_1} [Preorder P] [Inhabited P] : Inhabited (Ideal P)

Equations

• Order.Ideal.instInhabited = { default := Order.Ideal.principal default }

@[simp]

theorem Order.Ideal.principal_le_iff {P : Type u_1} [Preorder P] {I : Ideal P} {x : P} : principal x ≤ I ↔ x ∈ I

@[simp]

theorem Order.Ideal.mem_principal {P : Type u_1} [Preorder P] {x y : P} : x ∈ principal y ↔ x ≤ y

theorem Order.Ideal.mem_principal_self {P : Type u_1} [Preorder P] {x : P} : x ∈ principal x

instance Order.Ideal.instOrderBot {P : Type u_1} [Preorder P] [OrderBot P] : OrderBot (Ideal P)

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

Equations

• Order.Ideal.instOrderBot = { bot := Order.Ideal.principal ⊥, bot_le := ⋯ }

@[simp]

theorem Order.Ideal.principal_bot {P : Type u_1} [Preorder P] [OrderBot P] : principal ⊥ = ⊥

@[simp]

theorem Order.Ideal.principal_top {P : Type u_1} [Preorder P] [OrderTop P] : principal ⊤ = ⊤

theorem Order.Ideal.sup_mem {P : Type u_1} [SemilatticeSup P] {x y : P} {s : 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} [SemilatticeSup P] {x y : P} {I : Ideal P} : x ⊔ y ∈ I ↔ x ∈ I ∧ y ∈ I

@[simp]

theorem Order.Ideal.finsetSup_mem_iff {P : Type u_2} [SemilatticeSup P] [OrderBot P] (t : Ideal P) {ι : Type u_3} {f : ι → P} {s : Finset ι} : s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t

instance Order.Ideal.instMin {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] : Min (Ideal P)

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

Equations

• Order.Ideal.instMin = { min := fun (I J : Order.Ideal P) => let __LowerSet := I.toLowerSet ⊓ J.toLowerSet; { toLowerSet := __LowerSet, nonempty' := ⋯, directed' := ⋯ } }

instance Order.Ideal.instMax {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] : Max (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.instMax = { max := fun (I J : Order.Ideal P) => { carrier := {x : P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ } }

instance Order.Ideal.instLattice {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] : Lattice (Ideal P)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Order.Ideal.coe_sup {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] {s t : Ideal P} : ↑(s ⊔ t) = {x : P | ∃ a ∈ s, ∃ b ∈ t, x ≤ a ⊔ b}

@[simp]

theorem Order.Ideal.coe_inf {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] {s t : Ideal P} : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

theorem Order.Ideal.mem_inf {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] {x : P} {I J : Ideal P} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

@[simp]

theorem Order.Ideal.mem_sup {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] {x : P} {I J : Ideal P} : x ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j

theorem Order.Ideal.lt_sup_principal_of_not_mem {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 ≥ x2] {x : P} {I : Ideal P} (hx : x ∉ I) : I < I ⊔ principal x

instance Order.Ideal.instInfSet {P : Type u_1} [SemilatticeSup P] [OrderBot P] : InfSet (Ideal P)

Equations

• Order.Ideal.instInfSet = { sInf := fun (S : Set (Order.Ideal P)) => let __LowerSet := ⨅ s ∈ S, s.toLowerSet; { toLowerSet := __LowerSet, nonempty' := ⋯, directed' := ⋯ } }

@[simp]

theorem Order.Ideal.coe_sInf {P : Type u_1} [SemilatticeSup P] [OrderBot P] {S : Set (Ideal P)} : ↑(sInf S) = ⋂ s ∈ S, ↑s

@[simp]

theorem Order.Ideal.mem_sInf {P : Type u_1} [SemilatticeSup P] [OrderBot P] {x : P} {S : Set (Ideal P)} : x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

instance Order.Ideal.instCompleteLattice {P : Type u_1} [SemilatticeSup P] [OrderBot P] : CompleteLattice (Ideal P)

Equations

• One or more equations did not get rendered due to their size.

theorem Order.Ideal.eq_sup_of_le_sup {P : Type u_1} [DistribLattice P] {I J : Ideal P} {x i j : P} (hi : i ∈ I) (hj : j ∈ J) (hx : x ≤ i ⊔ j) : ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'

theorem Order.Ideal.coe_sup_eq {P : Type u_1} [DistribLattice P] {I J : Ideal P} : ↑(I ⊔ J) = {x : P | ∃ i ∈ I, ∃ j ∈ J, x = i ⊔ j}

theorem Order.Ideal.IsProper.not_mem_of_compl_mem {P : Type u_1} [BooleanAlgebra P] {x : P} {I : Ideal P} (hI : I.IsProper) (hxc : xᶜ ∈ I) : x ∉ I

theorem Order.Ideal.IsProper.not_mem_or_compl_not_mem {P : Type u_1} [BooleanAlgebra P] {x : P} {I : Ideal P} (hI : I.IsProper) : 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.

• carrier : Set P

  The carrier of a Cofinal is the underlying set.

• isCofinal : IsCofinal self.carrier

  The Cofinal contains arbitrarily large elements.

@[deprecated Order.Cofinal.isCofinal (since := "2024-12-02")]

theorem Order.Cofinal.mem_gt {P : Type u_2} [Preorder P] (self : Cofinal P) : IsCofinal self.carrier

Alias of Order.Cofinal.isCofinal.

---

The Cofinal contains arbitrarily large elements.

instance Order.Cofinal.instInhabited {P : Type u_1} [Preorder P] : Inhabited (Cofinal P)

Equations

• Order.Cofinal.instInhabited = { default := { carrier := Set.univ, isCofinal := ⋯ } }

instance Order.Cofinal.instMembership {P : Type u_1} [Preorder P] : Membership P (Cofinal P)

Equations

• Order.Cofinal.instMembership = { mem := fun (D : Order.Cofinal P) (x : P) => x ∈ D.carrier }

noncomputable def Order.Cofinal.above {P : Type u_1} [Preorder P] (D : Cofinal P) (x : P) : P

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

Equations

• D.above x = Classical.choose ⋯

theorem Order.Cofinal.above_mem {P : Type u_1} [Preorder P] (D : Cofinal P) (x : P) : D.above x ∈ D

theorem Order.Cofinal.le_above {P : Type u_1} [Preorder P] (D : Cofinal P) (x : P) : x ≤ D.above x

noncomputable def Order.sequenceOfCofinals {P : Type u_1} [Preorder P] (p : P) {ι : Type u_2} [Encodable ι] (𝒟 : ι → 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.sequenceOfCofinals p 𝒟 0 = p
• Order.sequenceOfCofinals p 𝒟 n.succ = match Encodable.decode n with | none => Order.sequenceOfCofinals p 𝒟 n | some i => (𝒟 i).above (Order.sequenceOfCofinals p 𝒟 n)

theorem Order.sequenceOfCofinals.monotone {P : Type u_1} [Preorder P] (p : P) {ι : Type u_2} [Encodable ι] (𝒟 : ι → Cofinal P) : Monotone (sequenceOfCofinals p 𝒟)

theorem Order.sequenceOfCofinals.encode_mem {P : Type u_1} [Preorder P] (p : P) {ι : Type u_2} [Encodable ι] (𝒟 : ι → Cofinal P) (i : ι) : sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i

def Order.idealOfCofinals {P : Type u_1} [Preorder P] (p : P) {ι : Type u_2} [Encodable ι] (𝒟 : ι → Cofinal P) : Ideal P

Given an element p : P and a family 𝒟 of cofinal subsets of a preorder P, indexed by a countable type, idealOfCofinals p 𝒟 is an ideal in P which

• contains p, according to mem_idealOfCofinals p 𝒟, and
• intersects every set in 𝒟, according to cofinal_meets_idealOfCofinals p 𝒟.

This proves the Rasiowa–Sikorski lemma.

Equations

• Order.idealOfCofinals p 𝒟 = { carrier := {x : P | ∃ (n : ℕ), x ≤ Order.sequenceOfCofinals p 𝒟 n}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }

theorem Order.mem_idealOfCofinals {P : Type u_1} [Preorder P] (p : P) {ι : Type u_2} [Encodable ι] (𝒟 : ι → Cofinal P) : p ∈ idealOfCofinals p 𝒟

theorem Order.cofinal_meets_idealOfCofinals {P : Type u_1} [Preorder P] (p : P) {ι : Type u_2} [Encodable ι] (𝒟 : ι → Cofinal P) (i : ι) : ∃ x ∈ 𝒟 i, x ∈ idealOfCofinals p 𝒟

idealOfCofinals p 𝒟 is 𝒟-generic.

theorem Order.isIdeal_sUnion_of_directedOn {P : Type u_1} [Preorder P] {C : Set (Set P)} (hidl : ∀ I ∈ C, IsIdeal I) (hD : DirectedOn (fun (x1 x2 : Set P) => x1 ⊆ x2) C) (hNe : C.Nonempty) : IsIdeal (⋃₀ C)

A non-empty directed union of ideals of sets in a preorder is an ideal.

theorem Order.isIdeal_sUnion_of_isChain {P : Type u_1} [Preorder P] {C : Set (Set P)} (hidl : ∀ I ∈ C, IsIdeal I) (hC : IsChain (fun (x1 x2 : Set P) => x1 ⊆ x2) C) (hNe : C.Nonempty) : IsIdeal (⋃₀ C)

A union of a nonempty chain of ideals of sets is an ideal.