Documentation

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

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

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

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

Equations
  • h.toIdeal = { carrier := I, lower' := β‹―, nonempty' := β‹―, directed' := β‹― }
instance Order.Ideal.instSetLike {P : Type u_1} [LE P] :
Equations
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)ᢜ

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

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

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.isProper_iff {P : Type u_1} [LE P] (I : Ideal P) :
    theorem Order.Ideal.isProper_of_notMem {P : Type u_1} [LE P] {I : Ideal P} {p : P} (notMem : p βˆ‰ I) :
    @[deprecated Order.Ideal.isProper_of_notMem (since := "2025-05-23")]
    theorem Order.Ideal.isProper_of_not_mem {P : Type u_1} [LE P] {I : Ideal P} {p : P} (notMem : p βˆ‰ I) :

    Alias of Order.Ideal.isProper_of_notMem.

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

    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.

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

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

      Equations
      @[simp]
      theorem Order.Ideal.top_toLowerSet {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≀ x2] [Nonempty P] :
      @[simp]
      theorem Order.Ideal.coe_top {P : Type u_1} [LE P] [IsDirected P fun (x1 x2 : P) => x1 ≀ x2] [Nonempty P] :
      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 β‰  ⊀) :
      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} :
      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) :
      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} :
      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] :
      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) :
      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} :
      @[simp]
      theorem Order.Ideal.bot_mem {P : Type u_1} [LE P] [OrderBot P] (s : Ideal P) :
      theorem Order.Ideal.top_of_top_mem {P : Type u_1} [LE P] [OrderTop P] {I : Ideal P} (h : ⊀ ∈ I) :
      theorem Order.Ideal.IsProper.top_notMem {P : Type u_1} [LE P] [OrderTop P] {I : Ideal P} (hI : I.IsProper) :
      ⊀ βˆ‰ I
      @[deprecated Order.Ideal.IsProper.top_notMem (since := "2025-05-23")]
      theorem Order.Ideal.IsProper.top_not_mem {P : Type u_1} [LE P] [OrderTop P] {I : Ideal P} (hI : I.IsProper) :
      ⊀ βˆ‰ I

      Alias of Order.Ideal.IsProper.top_notMem.

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

      The smallest ideal containing a given element.

      Equations
      @[simp]
      theorem Order.Ideal.principal_le_iff {P : Type u_1} [Preorder P] {I : Ideal P} {x : P} :
      @[simp]
      theorem Order.Ideal.mem_principal {P : Type u_1} [Preorder P] {x y : P} :

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

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

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

      Equations
      instance Order.Ideal.instMax {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 β‰₯ x2] :

      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
      instance Order.Ideal.instLattice {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 β‰₯ x2] :
      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_notMem {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
      @[deprecated Order.Ideal.lt_sup_principal_of_notMem (since := "2025-05-23")]
      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

      Alias of Order.Ideal.lt_sup_principal_of_notMem.

      Equations
      @[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
      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.notMem_of_compl_mem {P : Type u_1} [BooleanAlgebra P] {x : P} {I : Ideal P} (hI : I.IsProper) (hxc : xᢜ ∈ I) :
      x βˆ‰ I
      @[deprecated Order.Ideal.IsProper.notMem_of_compl_mem (since := "2025-05-23")]
      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

      Alias of Order.Ideal.IsProper.notMem_of_compl_mem.

      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
      @[deprecated Order.Ideal.IsProper.notMem_or_compl_notMem (since := "2025-05-23")]
      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

      Alias of Order.Ideal.IsProper.notMem_or_compl_notMem.

      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.

      @[deprecated Order.Cofinal.isCofinal (since := "2024-12-02")]
      theorem Order.Cofinal.mem_gt {P : Type u_2} [Preorder P] (self : Cofinal P) :

      Alias of Order.Cofinal.isCofinal.


      The Cofinal contains arbitrarily large elements.

      Equations
      Equations
      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
      theorem Order.Cofinal.above_mem {P : Type u_1} [Preorder P] (D : Cofinal P) (x : P) :
      theorem Order.Cofinal.le_above {P : Type u_1} [Preorder P] (D : Cofinal P) (x : P) :
      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
      theorem Order.sequenceOfCofinals.monotone {P : Type u_1} [Preorder P] (p : P) {ΞΉ : Type u_2} [Encodable ΞΉ] (π’Ÿ : ΞΉ β†’ Cofinal 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) :

      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

      This proves the Rasiowa–Sikorski lemma.

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

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

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