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).
Instances For
    theorem Order.isIdeal_iff {P : Type u_2} [LE P] (I : Set P) :
    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).
    Instances For
      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
      • Order.IsIdeal.toIdeal h = { toLowerSet := { carrier := I, lower' := β‹― }, nonempty' := β‹―, directed' := β‹― }
      Instances For
        theorem Order.Ideal.toLowerSet_injective {P : Type u_1} [LE P] :
        Function.Injective Order.Ideal.toLowerSet
        Equations
        • Order.Ideal.instSetLikeIdeal = { coe := fun (s : Order.Ideal P) => s.carrier, coe_injective' := β‹― }
        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) :
        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) :
        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_of_not_mem {P : Type u_1} [LE P] {I : Order.Ideal P} {p : P} (nmem : p βˆ‰ 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 :

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

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

            Equations
            • Order.Ideal.instOrderTopIdealToLEToPreorderInstPartialOrderIdeal = OrderTop.mk β‹―
            @[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 β‰  ⊀) :
            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} :
            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) :
            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} :
            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] :
            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) :
            @[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) :
            @[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
              • Order.Ideal.instOrderBotIdealToLEToPreorderInstPartialOrderIdeal = OrderBot.mk β‹―
              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} :

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

              Equations
              • Order.Ideal.instInfIdealToLEToPreorderToPartialOrder = { inf := fun (I J : Order.Ideal P) => { toLowerSet := I.toLowerSet βŠ“ J.toLowerSet, nonempty' := β‹―, directed' := β‹― } }

              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.
              Equations
              • Order.Ideal.instLatticeIdealToLEToPreorderToPartialOrder = let __src := Order.Ideal.instPartialOrderIdeal; Lattice.mk β‹― β‹― β‹―
              @[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} :
              @[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) :
              Equations
              • Order.Ideal.instInfSetIdealToLEToPreorderToPartialOrder = { 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
              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.

              Instances For
                Equations
                • Order.Cofinal.instInhabitedCofinal = { default := { carrier := Set.univ, mem_gt := β‹― } }
                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
                Instances For
                  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.