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.

      Instances For
        theorem Order.Ideal.toLowerSet_injective {P : Type u_1} [LE P] :
        Function.Injective Order.Ideal.toLowerSet
        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 => 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.

        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) :
        • ne_univ : ↑I β‰  Set.univ

          This ideal is not the whole set.

        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_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 :
          • 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.

          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.inter_nonempty {P : Type u_1} [LE P] [IsDirected P fun x x_1 => 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.

            @[simp]
            theorem Order.Ideal.top_toLowerSet {P : Type u_1} [LE P] [IsDirected P fun x x_1 => x ≀ x_1] [Nonempty P] :
            ⊀.toLowerSet = ⊀
            @[simp]
            theorem Order.Ideal.coe_top {P : Type u_1} [LE P] [IsDirected P fun x x_1 => 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 => 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 => x ≀ x_1] [Nonempty P] {I : Order.Ideal P} :
            theorem IsCoatom.isProper {P : Type u_1} [LE P] [IsDirected P fun x x_1 => 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 => 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 => 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 => 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.

            Instances For
              @[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.

              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.

              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.

              @[simp]
              theorem Order.Ideal.coe_sup {P : Type u_1} [SemilatticeSup P] [IsDirected P fun x x_1 => x β‰₯ x_1] {s : Order.Ideal P} {t : Order.Ideal P} :
              ↑(s βŠ” t) = {x | βˆƒ a, a ∈ s ∧ βˆƒ b, b ∈ t ∧ x ≀ a βŠ” b}
              @[simp]
              theorem Order.Ideal.coe_inf {P : Type u_1} [SemilatticeSup P] [IsDirected P fun x x_1 => 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 => 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 => x β‰₯ x_1] {x : P} {I : Order.Ideal P} {J : Order.Ideal P} :
              x ∈ I βŠ” J ↔ βˆƒ i, i ∈ I ∧ βˆƒ j, 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 => x β‰₯ x_1] {x : P} {I : Order.Ideal P} (hx : Β¬x ∈ I) :
              @[simp]
              theorem Order.Ideal.coe_sInf {P : Type u_1} [SemilatticeSup P] [OrderBot P] {S : Set (Order.Ideal P)} :
              ↑(sInf S) = β‹‚ (s : Order.Ideal P) (_ : 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 : Order.Ideal P), s ∈ S β†’ x ∈ s
              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' ∈ I ∧ βˆƒ j', 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 | βˆƒ i, i ∈ I ∧ βˆƒ j, j ∈ J ∧ x = i βŠ” j}
              structure Order.Cofinal (P : Type u_2) [Preorder P] :
              Type u_2
              • carrier : Set P

                The carrier of a Cofinal is the underlying set.

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

                The Cofinal contains arbitrarily large elements.

              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.

              Instances For
                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.

                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.

                    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, x ∈ π’Ÿ i ∧ x ∈ Order.idealOfCofinals p π’Ÿ

                      idealOfCofinals p π’Ÿ is π’Ÿ-generic.