Documentation

Mathlib.Order.CompactlyGenerated.Basic

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 s∃ (t : Finset ι), k t.sup s
        theorem CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le (α : Type u_2) [CompleteLattice α] (k : α) :
        CompleteLattice.IsCompactElement k ∀ (s : Set α), s.NonemptyDirectedOn (fun (x1 x2 : α) => x1 x2) sk sSup sxs, 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 : Finset ι), k is, f i
        theorem CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt {α : Type u_3} [CompleteLattice α] {k : α} (hk : CompleteLattice.IsCompactElement k) {s : Set α} (hemp : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) => x1 x2) s) (hbelow : xs, x < 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.isCompactElement_finsetSup {α : Type u_3} {β : Type u_4} [CompleteLattice α] {f : βα} (s : Finset β) (h : xs, CompleteLattice.IsCompactElement (f x)) :
        theorem CompleteLattice.WellFounded.finite_of_setIndependent {α : Type u_2} [CompleteLattice α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) {s : Set α} (hs : CompleteLattice.SetIndependent s) :
        s.Finite
        theorem CompleteLattice.WellFounded.finite_ne_bot_of_independent {α : Type u_2} [CompleteLattice α] (hwf : WellFounded fun (x1 x2 : α) => x1 > x2) {ι : Type u_3} {t : ια} (ht : CompleteLattice.Independent t) :
        {i : ι | t i }.Finite
        theorem CompleteLattice.WellFounded.finite_of_independent {α : Type u_2} [CompleteLattice α] (hwf : WellFounded fun (x1 x2 : α) => x1 > x2) {ι : Type u_3} {t : ια} (ht : CompleteLattice.Independent t) (h_ne_bot : ∀ (i : ι), t i ) :

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

        Instances
          theorem IsCompactlyGenerated.exists_sSup_eq {α : Type u_3} :
          ∀ {inst : CompleteLattice α} [self : IsCompactlyGenerated α] (x : α), ∃ (s : Set α), (∀ xs, CompleteLattice.IsCompactElement x) sSup s = x

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

          @[simp]
          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 (x1 x2 : α) => x1 x2) s) :
          a sSup s = bs, 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 (x1 x2 : α) => x1 x2) s) :
          sSup s a = bs, b a

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

          theorem Directed.inf_iSup_eq {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ια} [IsCompactlyGenerated α] {a : α} (h : Directed (fun (x1 x2 : α) => x1 x2) f) :
          a ⨆ (i : ι), f i = ⨆ (i : ι), a f i
          theorem Directed.iSup_inf_eq {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ια} [IsCompactlyGenerated α] {a : α} (h : Directed (fun (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) s) :
          Disjoint (sSup s) a ∀ ⦃b : α⦄, b sDisjoint b a
          theorem Directed.disjoint_iSup_right {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ια} [IsCompactlyGenerated α] {a : α} (h : Directed (fun (x1 x2 : α) => x1 x2) f) :
          Disjoint a (⨆ (i : ι), f i) ∀ (i : ι), Disjoint a (f i)
          theorem Directed.disjoint_iSup_left {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ια} [IsCompactlyGenerated α] {a : α} (h : Directed (fun (x1 x2 : α) => x1 x2) 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 t.sup id

          This property is equivalent to α being upper continuous.

          theorem CompleteLattice.independent_iff_supIndep_of_injOn {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} {f : ια} (hf : Set.InjOn f {i : ι | f i }) :
          CompleteLattice.Independent f ∀ (s : Finset ι), s.SupIndep f
          theorem CompleteLattice.setIndependent_iUnion_of_directed {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {η : Type u_3} {s : ηSet α} (hs : Directed (fun (x1 x2 : Set α) => x1 x2) 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.

          @[instance 100]
          Equations
          • =
          @[instance 100]

          See [Lemma 5.1][calugareanu].

          Equations
          • =

          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 : Set α), 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.

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

          See [Theorem 6.6][calugareanu].