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 :
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
    theorem Order.Ideal.nonempty' {P : Type u_2} [LE P] (self : Order.Ideal P) :
    self.carrier.Nonempty

    The ideal is nonempty.

    theorem Order.Ideal.directed' {P : Type u_2} [LE P] (self : Order.Ideal P) :
    DirectedOn (fun (x1 x2 : P) => x1 ≀ x2) 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 ∧ I.Nonempty ∧ DirectedOn (fun (x1 x2 : P) => x1 ≀ x2) I
    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).
    • IsLowerSet : 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
      theorem Order.IsIdeal.IsLowerSet {P : Type u_2} [LE P] {I : Set P} (self : Order.IsIdeal I) :

      The ideal is downward closed.

      theorem Order.IsIdeal.Nonempty {P : Type u_2} [LE P] {I : Set P} (self : Order.IsIdeal I) :
      I.Nonempty

      The ideal is nonempty.

      theorem Order.IsIdeal.Directed {P : Type u_2} [LE P] {I : Set P} (self : Order.IsIdeal I) :
      DirectedOn (fun (x1 x2 : P) => x1 ≀ x2) I

      The ideal is upward directed.

      def Order.IsIdeal.toIdeal {P : Type u_1} [LE P] {I : Set P} (h : Order.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' := β‹― }
      Instances For
        theorem Order.Ideal.toLowerSet_injective {P : Type u_1} [LE P] :
        Function.Injective Order.Ideal.toLowerSet
        instance Order.Ideal.instSetLike {P : Type u_1} [LE P] :
        Equations
        • Order.Ideal.instSetLike = { coe := fun (s : Order.Ideal P) => s.carrier, coe_injective' := β‹― }
        theorem Order.Ideal.ext_iff {P : Type u_1} [LE P] {s : Order.Ideal P} {t : Order.Ideal P} :
        s = t ↔ ↑s = ↑t
        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) :
        (↑s).Nonempty
        theorem Order.Ideal.directed {P : Type u_1} [LE P] (s : Order.Ideal P) :
        DirectedOn (fun (x1 x2 : P) => x1 ≀ x2) ↑s
        theorem Order.Ideal.isIdeal {P : Type u_1} [LE P] (s : Order.Ideal P) :
        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)ᢜ

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

        Equations
        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) :
        I.IsProper ↔ ↑I β‰  Set.univ
        class Order.Ideal.IsProper {P : Type u_1} [LE P] (I : Order.Ideal P) :

        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
          theorem Order.Ideal.IsProper.ne_univ {P : Type u_1} :
          βˆ€ {inst : LE P} {I : Order.Ideal P} [self : I.IsProper], ↑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) :
          I.IsProper
          theorem Order.Ideal.isMaximal_iff {P : Type u_1} [LE P] (I : Order.Ideal P) :
          I.IsMaximal ↔ I.IsProper ∧ βˆ€ ⦃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 :

          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.

          Instances
            theorem Order.Ideal.IsMaximal.maximal_proper {P : Type u_1} :
            βˆ€ {inst : LE P} {I : Order.Ideal P} [self : I.IsMaximal] ⦃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 (x1 x2 : P) => x1 β‰₯ x2] (I : Order.Ideal P) (J : Order.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] :
            ⊀.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 : Order.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 : Order.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 : Order.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 : Order.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 : Order.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) :
            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 : Order.Ideal P} :
            I.IsMaximal ↔ IsCoatom I
            @[simp]
            theorem Order.Ideal.bot_mem {P : Type u_1} [LE P] [OrderBot P] (s : Order.Ideal P) :
            theorem Order.Ideal.top_of_top_mem {P : Type u_1} [LE P] [OrderTop P] {I : Order.Ideal P} (h : ⊀ ∈ I) :
            theorem Order.Ideal.IsProper.top_not_mem {P : Type u_1} [LE P] [OrderTop P] {I : Order.Ideal P} (hI : I.IsProper) :
            ⊀ βˆ‰ I
            @[simp]
            theorem Order.Ideal.principal_toLowerSet {P : Type u_1} [Preorder P] (p : P) :
            def Order.Ideal.principal {P : Type u_1} [Preorder P] (p : P) :

            The smallest ideal containing a given element.

            Equations
            Instances For
              Equations
              @[simp]
              theorem Order.Ideal.mem_principal {P : Type u_1} [Preorder P] {x : P} {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 : P} {y : P} {s : Order.Ideal P} (hx : x ∈ s) (hy : 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} :
              instance Order.Ideal.instInf {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
              • Order.Ideal.instInf = { inf := fun (I J : Order.Ideal P) => { toLowerSet := I.toLowerSet βŠ“ J.toLowerSet, nonempty' := β‹―, directed' := β‹― } }
              instance Order.Ideal.instSup {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
              • Order.Ideal.instSup = { sup := 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] :
              Equations
              • Order.Ideal.instLattice = Lattice.mk β‹― β‹― β‹―
              @[simp]
              theorem Order.Ideal.coe_sup {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 β‰₯ x2] {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 (x1 x2 : P) => x1 β‰₯ x2] {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 (x1 x2 : P) => x1 β‰₯ x2] {x : P} {I : Order.Ideal P} {J : Order.Ideal P} :
              @[simp]
              theorem Order.Ideal.mem_sup {P : Type u_1} [SemilatticeSup P] [IsDirected P fun (x1 x2 : P) => x1 β‰₯ x2] {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 (x1 x2 : P) => x1 β‰₯ x2] {x : P} {I : Order.Ideal P} (hx : x βˆ‰ I) :
              Equations
              • Order.Ideal.instInfSet = { sInf := fun (S : Set (Order.Ideal P)) => { toLowerSet := β¨… s ∈ S, s.toLowerSet, nonempty' := β‹―, directed' := β‹― } }
              @[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
              Equations
              • Order.Ideal.instCompleteLattice = CompleteLattice.mk β‹― β‹― β‹― β‹― β‹― β‹―
              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 : 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 : Order.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.

              • mem_gt : βˆ€ (x : P), βˆƒ y ∈ self.carrier, x ≀ y

                The Cofinal contains arbitrarily large elements.

              Instances For
                theorem Order.Cofinal.mem_gt {P : Type u_2} [Preorder P] (self : Order.Cofinal P) (x : P) :
                βˆƒ y ∈ self.carrier, x ≀ y

                The Cofinal contains arbitrarily large elements.

                Equations
                • Order.Cofinal.instInhabited = { default := { carrier := Set.univ, mem_gt := β‹― } }
                Equations
                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
                Instances For
                  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.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
                  Instances For
                    theorem Order.sequenceOfCofinals.monotone {P : Type u_1} [Preorder P] (p : P) {ΞΉ : Type u_2} [Encodable ΞΉ] (π’Ÿ : ΞΉ β†’ Order.Cofinal P) :
                    theorem Order.sequenceOfCofinals.encode_mem {P : Type u_1} [Preorder P] (p : P) {ΞΉ : Type u_2} [Encodable ΞΉ] (π’Ÿ : ΞΉ β†’ Order.Cofinal P) (i : ΞΉ) :
                    def Order.idealOfCofinals {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, idealOfCofinals p π’Ÿ is an ideal in P which

                    This proves the Rasiowa–Sikorski lemma.

                    Equations
                    Instances For
                      theorem Order.mem_idealOfCofinals {P : Type u_1} [Preorder P] (p : P) {ΞΉ : Type u_2} [Encodable ΞΉ] (π’Ÿ : ΞΉ β†’ Order.Cofinal 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.

                      theorem Order.isIdeal_sUnion_of_directedOn {P : Type u_1} [Preorder P] {C : Set (Set P)} (hidl : βˆ€ I ∈ C, Order.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, Order.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.