Documentation

Mathlib.Order.CompactlyGenerated

Compactness properties for complete lattices #

For complete lattices, there are numerous equivalent ways to express the fact that the relation > is well-founded. In this file we define three especially-useful characterisations and provide proofs that they are indeed equivalent to well-foundedness.

Main definitions #

Main results #

The main result is that the following four conditions are equivalent for a complete lattice:

This is demonstrated by means of the following four lemmas:

We also show well-founded lattices are compactly generated (CompleteLattice.isCompactlyGenerated_of_wellFounded).

References #

Tags #

complete lattice, well-founded, compact

A compactness property for a complete lattice is that any sup-closed non-empty subset contains its sSup.

Equations
Instances For

    A compactness property for a complete lattice is that any subset has a finite subset with the same sSup.

    Equations
    Instances For

      An element k of a complete lattice is said to be compact if any set with sSup above k has a finite subset with sSup above k. Such an element is also called "finite" or "S-compact".

      Equations
      Instances For
        theorem CompleteLattice.isCompactElement_iff {α : Type u} [CompleteLattice α] (k : α) :
        CompleteLattice.IsCompactElement k ∀ (ι : Type u) (s : ια), k iSup st, k Finset.sup t s
        theorem CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le (α : Type u_2) [CompleteLattice α] (k : α) :
        CompleteLattice.IsCompactElement k ∀ (s : Set α), Set.Nonempty sDirectedOn (fun x x_1 => x x_1) sk sSup sx, x s k x

        An element k is compact if and only if any directed set with sSup above k already got above k at some point in the set.

        theorem CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (α : Type u_2) [CompleteLattice α] {k : α} (hk : CompleteLattice.IsCompactElement k) {ι : Type u_3} (f : ια) (h : k ⨆ (i : ι), f i) :
        s, k ⨆ (i : ι) (_ : i s), f i
        theorem CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt {α : Type u_3} [CompleteLattice α] {k : α} (hk : CompleteLattice.IsCompactElement k) {s : Set α} (hemp : Set.Nonempty s) (hdir : DirectedOn (fun x x_1 => x x_1) s) (hbelow : ∀ (x : α), x sx < k) :
        sSup s < k

        A compact element k has the property that any directed set lying strictly below k has its sSup strictly below k.

        theorem CompleteLattice.finset_sup_compact_of_compact {α : Type u_3} {β : Type u_4} [CompleteLattice α] {f : βα} (s : Finset β) (h : ∀ (x : β), x sCompleteLattice.IsCompactElement (f x)) :
        theorem CompleteLattice.WellFounded.finite_of_independent {α : Type u_2} [CompleteLattice α] (hwf : WellFounded fun x x_1 => x > x_1) {ι : Type u_3} {t : ια} (ht : CompleteLattice.Independent t) (h_ne_bot : ∀ (i : ι), t i ) :
        • exists_sSup_eq : ∀ (x : α), s, (∀ (x : α), x sCompleteLattice.IsCompactElement x) sSup s = x

          In a compactly generated complete lattice, every element is the sSup of some set of compact elements.

        A complete lattice is said to be compactly generated if any element is the sSup of compact elements.

        Instances
          theorem le_iff_compact_le_imp {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {b : α} :
          a b ∀ (c : α), CompleteLattice.IsCompactElement cc ac b
          theorem DirectedOn.inf_sSup_eq {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} (h : DirectedOn (fun x x_1 => x x_1) s) :
          a sSup s = ⨆ (b : α) (_ : b s), a b

          This property is sometimes referred to as α being upper continuous.

          theorem DirectedOn.sSup_inf_eq {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} (h : DirectedOn (fun x x_1 => x x_1) s) :
          sSup s a = ⨆ (b : α) (_ : b s), b a

          This property is sometimes referred to as α being upper continuous.

          theorem Directed.inf_iSup_eq {ι : Sort u_1} {α : Type u_2} {f : ια} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} (h : Directed (fun x x_1 => x x_1) f) :
          a ⨆ (i : ι), f i = ⨆ (i : ι), a f i
          theorem Directed.iSup_inf_eq {ι : Sort u_1} {α : Type u_2} {f : ια} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} (h : Directed (fun x x_1 => x x_1) f) :
          (⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
          theorem DirectedOn.disjoint_sSup_right {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} (h : DirectedOn (fun x x_1 => x x_1) s) :
          Disjoint a (sSup s) ∀ ⦃b : α⦄, b sDisjoint a b
          theorem DirectedOn.disjoint_sSup_left {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} (h : DirectedOn (fun x x_1 => x x_1) s) :
          Disjoint (sSup s) a ∀ ⦃b : α⦄, b sDisjoint b a
          theorem Directed.disjoint_iSup_right {ι : Sort u_1} {α : Type u_2} {f : ια} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} (h : Directed (fun x x_1 => x x_1) f) :
          Disjoint a (⨆ (i : ι), f i) ∀ (i : ι), Disjoint a (f i)
          theorem Directed.disjoint_iSup_left {ι : Sort u_1} {α : Type u_2} {f : ια} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} (h : Directed (fun x x_1 => x x_1) f) :
          Disjoint (⨆ (i : ι), f i) a ∀ (i : ι), Disjoint (f i) a
          theorem inf_sSup_eq_iSup_inf_sup_finset {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} :
          a sSup s = ⨆ (t : Finset α) (_ : t s), a Finset.sup t id

          This property is equivalent to α being upper continuous.

          theorem CompleteLattice.setIndependent_iUnion_of_directed {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {η : Type u_3} {s : ηSet α} (hs : Directed (fun x x_1 => x x_1) s) (h : ∀ (i : η), CompleteLattice.SetIndependent (s i)) :
          CompleteLattice.SetIndependent (⋃ (i : η), s i)

          A compact element k has the property that any b < k lies below a "maximal element below k", which is to say [⊥, k] is coatomic.

          Now we will prove that a compactly generated modular atomistic lattice is a complemented lattice. Most explicitly, every element is the complement of a supremum of indepedendent atoms.

          theorem exists_setIndependent_isCompl_sSup_atoms {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a | IsAtom a} = ) (b : α) :
          s, CompleteLattice.SetIndependent s IsCompl b (sSup s) ∀ ⦃a : α⦄, a sIsAtom a

          In an atomic lattice, every element b has a complement of the form sSup s, where each element of s is an atom. See also complementedLattice_of_sSup_atoms_eq_top.

          See [Theorem 6.6][calugareanu].