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

source

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.

Instances For

source

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.

Instances For

source

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

source

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' := ⋯ }

Instances For

source

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

Function.Injective toLowerSet

source

@[implicit_reducible]

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' := ⋯ }

source

@[implicit_reducible]

instance Order.Ideal.instPartialOrder {P : Type u_1} [LE P] :

PartialOrder (Ideal P)

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

Equations

Order.Ideal.instPartialOrder = PartialOrder.ofSetLike (Order.Ideal P) P

source

@[deprecated Order.Ideal.instPartialOrder (since := "2026-04-01")]

def Order.Ideal.instPartialOrderIdeal {P : Type u_1} [LE P] :

PartialOrder (Ideal P)

Alias of Order.Ideal.instPartialOrder.

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

Equations

@Order.Ideal.instPartialOrderIdeal = @Order.Ideal.instPartialOrder

Instances For

source

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

↑s = ↑t → s = t

source

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

s = t ↔ ↑s = ↑t

source

@[simp]

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

s.carrier = ↑s

source

@[simp]

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

↑s.toLowerSet = ↑s

source

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

IsLowerSet ↑s

source

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

(↑s).Nonempty

source

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

DirectedOn (fun (x1 x2 : P) => x1 ≤ x2) ↑s

source

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

IsIdeal ↑s

source

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

source

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

↑s ⊆ ↑t ↔ s ≤ t

source

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

↑s ⊂ ↑t ↔ s < t

source

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

source

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.

Instances

source

theorem Order.Ideal.isProper_iff {P : Type u_1} [LE P] (I : Ideal P) :

I.IsProper ↔ ↑I ≠ Set.univ

source

theorem Order.Ideal.isProper_of_notMem {P : Type u_1} [LE P] {I : Ideal P} {p : P} (notMem : p ∉ I) :

I.IsProper

source

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.

Instances

source

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

source

theorem Order.Ideal.inter_nonempty {P : Type u_1} [LE P] [IsCodirectedOrder P] (I J : Ideal P) :

(↑I ∩ ↑J).Nonempty

source

@[implicit_reducible]

instance Order.Ideal.instOrderTop {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] :

OrderTop (Ideal P)

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

Equations

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

source

@[simp]

theorem Order.Ideal.top_toLowerSet {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] :

⊤.toLowerSet = ⊤

source

@[simp]

theorem Order.Ideal.coe_top {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] :

↑⊤ = Set.univ

source

theorem Order.Ideal.isProper_of_ne_top {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] {I : Ideal P} (ne_top : I ≠ ⊤) :

I.IsProper

source

theorem Order.Ideal.IsProper.ne_top {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] {I : Ideal P} :

I.IsProper → I ≠ ⊤

source

theorem IsCoatom.isProper {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] {I : Order.Ideal P} (hI : IsCoatom I) :

I.IsProper

source

theorem Order.Ideal.isProper_iff_ne_top {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] {I : Ideal P} :

I.IsProper ↔ I ≠ ⊤

source

theorem Order.Ideal.IsMaximal.isCoatom {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] {I : Ideal P} :

I.IsMaximal → IsCoatom I

source

theorem Order.Ideal.IsMaximal.isCoatom' {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] {I : Ideal P} [I.IsMaximal] :

IsCoatom I

source

theorem IsCoatom.isMaximal {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] {I : Order.Ideal P} (hI : IsCoatom I) :

I.IsMaximal

source

theorem Order.Ideal.isMaximal_iff_isCoatom {P : Type u_1} [LE P] [IsDirectedOrder P] [Nonempty P] {I : Ideal P} :

I.IsMaximal ↔ IsCoatom I

source

@[simp]

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

⊥ ∈ s

source

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

I = ⊤

source

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

⊤ ∉ I

source

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' := ⋯ }

Instances For

source

@[simp]

theorem Order.Ideal.principal_toLowerSet {P : Type u_1} [Preorder P] (p : P) :

(principal p).toLowerSet = LowerSet.Iic p

source

@[implicit_reducible]

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

Inhabited (Ideal P)

Equations

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

source

@[simp]

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

principal x ≤ I ↔ x ∈ I

source

@[simp]

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

x ∈ principal y ↔ x ≤ y

source

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

x ∈ principal x

source

@[implicit_reducible]

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

source

@[simp]

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

principal ⊥ = ⊥

source

@[simp]

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

principal ⊤ = ⊤

source

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.

source

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

source

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

source

@[implicit_reducible]

instance Order.Ideal.instMin {P : Type u_1} [SemilatticeSup P] [IsCodirectedOrder P] :

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' := ⋯ } }

source

@[implicit_reducible]

instance Order.Ideal.instMax {P : Type u_1} [SemilatticeSup P] [IsCodirectedOrder P] :

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' := ⋯ } }

source

@[implicit_reducible]

instance Order.Ideal.instLattice {P : Type u_1} [SemilatticeSup P] [IsCodirectedOrder P] :

Lattice (Ideal P)

Equations

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

source

@[simp]

theorem Order.Ideal.coe_sup {P : Type u_1} [SemilatticeSup P] [IsCodirectedOrder P] {s t : Ideal P} :

↑(s ⊔ t) = {x : P | ∃ a ∈ s, ∃ b ∈ t, x ≤ a ⊔ b}

source

@[simp]

theorem Order.Ideal.coe_inf {P : Type u_1} [SemilatticeSup P] [IsCodirectedOrder P] {s t : Ideal P} :

↑(s ⊓ t) = ↑s ∩ ↑t

source

@[simp]

theorem Order.Ideal.mem_inf {P : Type u_1} [SemilatticeSup P] [IsCodirectedOrder P] {x : P} {I J : Ideal P} :

x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

source

@[simp]

theorem Order.Ideal.mem_sup {P : Type u_1} [SemilatticeSup P] [IsCodirectedOrder P] {x : P} {I J : Ideal P} :

x ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j

source

theorem Order.Ideal.lt_sup_principal_of_notMem {P : Type u_1} [SemilatticeSup P] [IsCodirectedOrder P] {x : P} {I : Ideal P} (hx : x ∉ I) :

I < I ⊔ principal x

source

@[implicit_reducible]

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' := ⋯ } }

source

@[simp]

theorem Order.Ideal.coe_sInf {P : Type u_1} [SemilatticeSup P] [OrderBot P] {S : Set (Ideal P)} :

↑(sInf S) = ⋂ s ∈ S, ↑s

source

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

source

@[implicit_reducible]

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.

source

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'

source

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}

source

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

x ∉ I

source

theorem Order.Ideal.IsProper.notMem_or_compl_notMem {P : Type u_1} [BooleanAlgebra P] {x : P} {I : Ideal P} (hI : I.IsProper) :

x ∉ I ∨ xᶜ ∉ I

source

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.

Instances For

source

@[implicit_reducible]

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

Inhabited (Cofinal P)

Equations

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

source

@[implicit_reducible]

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 }

source

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

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

Equations

D.above x = Classical.choose ⋯

Instances For

source

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

D.above x ∈ D

source

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

x ≤ D.above x

source

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)

Instances For

source

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

Monotone (sequenceOfCofinals p 𝒟)

source

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

source

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' := ⋯ }

Instances For

source

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

p ∈ idealOfCofinals p 𝒟

source

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.

source

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.

source

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.

Documentation

Mathlib.Order.Ideal

Order ideals, cofinal sets, and the Rasiowa–Sikorski lemma #

Main definitions #

References #

Tags #