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

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 : 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' : Set.Nonempty self.carrier

  The ideal is nonempty.

• directed' : DirectedOn (fun (x x_1 : P) => x ≤ x_1) self.carrier

  The ideal is upward directed.

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

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 : IsLowerSet I

  The ideal is downward closed.

• Nonempty : Set.Nonempty I

  The ideal is nonempty.

• Directed : DirectedOn (fun (x x_1 : P) => x ≤ x_1) I

  The ideal is upward directed.

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

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

Equations

• Order.IsIdeal.toIdeal h = { toLowerSet := { carrier := I, lower' := (_ : IsLowerSet I) }, nonempty' := (_ : Set.Nonempty I), directed' := (_ : DirectedOn (fun (x x_1 : P) => x ≤ x_1) I) }

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

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

Equations

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

• Order.Ideal.instPartialOrderIdeal = PartialOrder.lift SetLike.coe (_ : Function.Injective SetLike.coe)

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

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

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

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

class Order.Ideal.IsProper {P : Type u_1} [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.

• ne_univ : ↑I ≠ Set.univ

  This ideal is not the whole set.

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

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

class Order.Ideal.IsMaximal {P : Type u_1} [LE P] (I : Order.Ideal P) extends Order.Ideal.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 : Order.Ideal P⦄, I < J → ↑J = Set.univ

  This ideal is maximal in the collection of proper ideals.

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

instance Order.Ideal.instOrderTopIdealToLEToPreorderInstPartialOrderIdeal {P : Type u_1} [LE P] [IsDirected P fun (x x_1 : P) => x ≤ x_1] [Nonempty P] : OrderTop (Order.Ideal P)

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

Equations

• Order.Ideal.instOrderTopIdealToLEToPreorderInstPartialOrderIdeal = OrderTop.mk (_ : ∀ (x : Order.Ideal P), ∀ x_1 ∈ ↑x, x_1 ∈ ⊤)

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

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

The smallest ideal containing a given element.

Equations

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

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

Equations

• Order.Ideal.instInhabitedIdealToLE = { 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 : P} {y : P} : x ∈ Order.Ideal.principal y ↔ x ≤ y

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

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

Equations

• Order.Ideal.instOrderBotIdealToLEToPreorderInstPartialOrderIdeal = OrderBot.mk (_ : ∀ (a : Order.Ideal P), Order.Ideal.principal ⊥ ≤ a)

@[simp]

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

@[simp]

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

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

instance Order.Ideal.instInfIdealToLEToPreorderToPartialOrder {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x x_1 : P) => x ≥ x_1] : Inf (Order.Ideal P)

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

Equations

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

instance Order.Ideal.instSupIdealToLEToPreorderToPartialOrder {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x x_1 : P) => x ≥ x_1] : 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

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

instance Order.Ideal.instLatticeIdealToLEToPreorderToPartialOrder {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x x_1 : P) => x ≥ x_1] : Lattice (Order.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 (x x_1 : P) => x ≥ x_1] {s : Order.Ideal P} {t : Order.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 (x x_1 : P) => x ≥ x_1] {s : Order.Ideal P} {t : Order.Ideal P} : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

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

@[simp]

theorem Order.Ideal.mem_sup {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x x_1 : P) => x ≥ x_1] {x : P} {I : Order.Ideal P} {J : Order.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 (x x_1 : P) => x ≥ x_1] {x : P} {I : Order.Ideal P} (hx : x ∉ I) : I < I ⊔ Order.Ideal.principal x

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

Equations

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

@[simp]

theorem Order.Ideal.coe_sInf {P : Type u_1} [SemilatticeSup P] [OrderBot P] {S : Set (Order.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 (Order.Ideal P)} : x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

instance Order.Ideal.instCompleteLatticeIdealToLEToPreorderToPartialOrder {P : Type u_1} [SemilatticeSup P] [OrderBot P] : CompleteLattice (Order.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 : Order.Ideal P} {J : Order.Ideal P} {x : P} {i : P} {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 : Order.Ideal P} {J : Order.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 : Order.Ideal P} (hI : Order.Ideal.IsProper I) (hxc : xᶜ ∈ I) : x ∉ I

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

• mem_gt : ∀ (x : P), ∃ y ∈ self.carrier, x ≤ y

  The Cofinal contains arbitrarily large elements.

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

Equations

• Order.Cofinal.instInhabitedCofinal = { default := { carrier := Set.univ, mem_gt := (_ : ∀ (x : P), ∃ y ∈ Set.univ, x ≤ y) } }

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

Equations

• Order.Cofinal.instMembershipCofinal = { mem := fun (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

• Order.Cofinal.above D x = Classical.choose (_ : ∃ y ∈ D.carrier, x ≤ y)

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

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

noncomputable def Order.sequenceOfCofinals {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.sequenceOfCofinals p 𝒟 0 = p
• Order.sequenceOfCofinals p 𝒟 (Nat.succ n) = match Encodable.decode n with | none => Order.sequenceOfCofinals p 𝒟 n | some i => Order.Cofinal.above (𝒟 i) (Order.sequenceOfCofinals p 𝒟 n)

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

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

def Order.idealOfCofinals {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, 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

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

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

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

idealOfCofinals p 𝒟 is 𝒟-generic.