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

• CompleteLattice.IsSupClosedCompact
• CompleteLattice.IsSupFiniteCompact
• IsCompactElement
• IsCompactlyGenerated

Main results

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

• well_founded (>)
• CompleteLattice.IsSupClosedCompact
• CompleteLattice.IsSupFiniteCompact
• ∀ k, IsCompactElement k

This is demonstrated by means of the following four lemmas:

• CompleteLattice.WellFounded.isSupFiniteCompact
• CompleteLattice.IsSupFiniteCompact.isSupClosedCompact
• CompleteLattice.IsSupClosedCompact.wellFounded
• CompleteLattice.isSupFiniteCompact_iff_all_elements_compact

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

References

• [G. Călugăreanu, Lattice Concepts of Module Theory][calugareanu]

Tags

complete lattice, well-founded, compact

def IsCompactElement {α : Type u_1} [PartialOrder α] (k : α) : Prop

An element k is compact if any directed set with LUB (least upper bound) above k has already got above k at some point in the set. Such an element is also called "finite" or "S-compact".

Equations

• IsCompactElement k = ∀ (s : Set α) (u : α), s.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s → IsLUB s u → k ≤ u → ∃ x ∈ s, k ≤ x

def CompleteLattice.IsSupClosedCompact (α : Type u_2) [CompleteLattice α] : Prop

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

Equations

• CompleteLattice.IsSupClosedCompact α = ∀ (s : Set α), s.Nonempty → SupClosed s → sSup s ∈ s

def CompleteLattice.IsSupFiniteCompact (α : Type u_2) [CompleteLattice α] : Prop

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

Equations

• CompleteLattice.IsSupFiniteCompact α = ∀ (s : Set α), ∃ (t : Finset α), ↑t ⊆ s ∧ sSup s = t.sup id

theorem CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le (α : Type u_2) [CompleteLattice α] (k : α) : IsCompactElement k ↔ ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s → k ≤ sSup s → ∃ 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_iff_exists_le_sSup_of_le_sSup (α : Type u_2) [CompleteLattice α] (k : α) : IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), ↑t ⊆ s ∧ k ≤ t.sup id

An element k of is compact if any set with sSup above k has a finite subset with sSup above k.

theorem CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup {α : Type u} [CompleteLattice α] (k : α) : IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s

theorem CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (α : Type u_2) [CompleteLattice α] {k : α} (hk : IsCompactElement k) {ι : Type u_3} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i) : ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i

theorem CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt {α : Type u_3} [CompleteLattice α] {k : α} (hk : IsCompactElement k) {s : Set α} (hemp : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hbelow : ∀ x ∈ s, 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 : ∀ x ∈ s, IsCompactElement (f x)) : IsCompactElement (s.sup f)

theorem CompleteLattice.WellFoundedGT.isSupFiniteCompact (α : Type u_2) [CompleteLattice α] [WellFoundedGT α] : IsSupFiniteCompact α

theorem CompleteLattice.IsSupFiniteCompact.isSupClosedCompact (α : Type u_2) [CompleteLattice α] (h : IsSupFiniteCompact α) : IsSupClosedCompact α

theorem CompleteLattice.IsSupClosedCompact.wellFoundedGT (α : Type u_2) [CompleteLattice α] (h : IsSupClosedCompact α) : WellFoundedGT α

theorem CompleteLattice.isSupFiniteCompact_iff_all_elements_compact (α : Type u_2) [CompleteLattice α] : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k

theorem CompleteLattice.wellFoundedGT_characterisations (α : Type u_2) [CompleteLattice α] : [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

theorem CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact (α : Type u_2) [CompleteLattice α] : WellFoundedGT α ↔ IsSupFiniteCompact α

theorem CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact (α : Type u_2) [CompleteLattice α] : IsSupFiniteCompact α ↔ IsSupClosedCompact α

theorem CompleteLattice.isSupClosedCompact_iff_wellFoundedGT (α : Type u_2) [CompleteLattice α] : IsSupClosedCompact α ↔ WellFoundedGT α

theorem CompleteLattice.IsSupFiniteCompact.wellFoundedGT (α : Type u_2) [CompleteLattice α] : IsSupFiniteCompact α → WellFoundedGT α

Alias of the reverse direction of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact.

theorem CompleteLattice.IsSupClosedCompact.isSupFiniteCompact (α : Type u_2) [CompleteLattice α] : IsSupClosedCompact α → IsSupFiniteCompact α

Alias of the reverse direction of CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact.

theorem CompleteLattice.WellFoundedGT.isSupClosedCompact (α : Type u_2) [CompleteLattice α] : WellFoundedGT α → IsSupClosedCompact α

Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT.

theorem WellFoundedGT.finite_of_sSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {s : Set α} (hs : sSupIndep s) : s.Finite

theorem WellFoundedGT.finite_ne_bot_of_iSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) : {i : ι | t i ≠ ⊥}.Finite

theorem WellFoundedGT.finite_of_iSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) : Finite ι

theorem WellFoundedLT.finite_of_sSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {s : Set α} (hs : sSupIndep s) : s.Finite

theorem WellFoundedLT.finite_ne_bot_of_iSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) : {i : ι | t i ≠ ⊥}.Finite

theorem WellFoundedLT.finite_of_iSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) : Finite ι

class IsCompactlyGenerated (α : Type u_3) [CompleteLattice α] : Prop

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

• exists_sSup_eq (x : α) : ∃ (s : Set α), (∀ x ∈ s, IsCompactElement x) ∧ sSup s = x

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

@[simp]

theorem sSup_compact_le_eq {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] (b : α) : sSup {c : α | IsCompactElement c ∧ c ≤ b} = b

@[simp]

theorem sSup_compact_eq_top {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] : sSup {a : α | IsCompactElement a} = ⊤

theorem le_iff_compact_le_imp {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a b : α} : a ≤ b ↔ ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ 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 = ⨆ 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 (x1 x2 : α) => x1 ≤ x2) s) : sSup s ⊓ a = ⨆ 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} [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 ∈ s → Disjoint 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 ∈ s → Disjoint 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 sSupIndep_iff_finite {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {s : Set α} : sSupIndep s ↔ ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t

theorem iSupIndep_iff_supIndep_of_injOn {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} {f : ι → α} (hf : Set.InjOn f {i : ι | f i ≠ ⊥}) : iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

theorem sSupIndep_iUnion_of_directed {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {η : Type u_3} {s : η → Set α} (hs : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (h : ∀ (i : η), sSupIndep (s i)) : sSupIndep (⋃ (i : η), s i)

theorem iSupIndep_sUnion_of_directed {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {s : Set (Set α)} (hs : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (h : ∀ a ∈ s, sSupIndep a) : sSupIndep (⋃₀ s)

theorem CompleteLattice.isCompactlyGenerated_of_wellFoundedGT {α : Type u_2} [CompleteLattice α] [h : WellFoundedGT α] : IsCompactlyGenerated α

theorem CompleteLattice.Iic_coatomic_of_compact_element {α : Type u_2} [CompleteLattice α] {k : α} (h : IsCompactElement k) : IsCoatomic ↑(Set.Iic k)

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.

theorem CompleteLattice.coatomic_of_top_compact {α : Type u_2} [CompleteLattice α] (h : IsCompactElement ⊤) : IsCoatomic α

theorem iSupIndep.iInf {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] {ι : Type u_3} {κ : ι → Type u_4} (f : (i : ι) → κ i → α) (h_indep : ∀ (i : ι), iSupIndep (f i)) : iSupIndep fun (k : (i : ι) → κ i) => ⨅ (i : ι), f i (k i)

If each family f i is iSupIndep, then the family of pointwise infima k ↦ ⨅ i, f i (k i) is also iSupIndep.

@[instance 100]

instance isAtomic_of_complementedLattice {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [ComplementedLattice α] : IsAtomic α

@[instance 100]

instance isAtomistic_of_complementedLattice {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [ComplementedLattice α] : IsAtomistic α

See [Lemma 5.1][calugareanu].

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 independent atoms.

theorem exists_sSupIndep_disjoint_sSup_atoms {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (b c : α) (hbc : b ≤ c) (h : sSup {a : α | a ≤ c ∧ IsAtom a} = c) : ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

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

theorem exists_sSupIndep_isCompl_sSup_atoms {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a : α | IsAtom a} = ⊤) (b : α) : ∃ (s : Set α), sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom 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_sSupIndep_of_sSup_atoms {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (b : α) (h : sSup {a : α | a ≤ b ∧ IsAtom a} = b) : ∃ (s : Set α), sSupIndep s ∧ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

theorem exists_sSupIndep_of_sSup_atoms_eq_top {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a : α | IsAtom a} = ⊤) : ∃ (s : Set α), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

theorem complementedLattice_of_sSup_atoms_eq_top {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a : α | IsAtom a} = ⊤) : ComplementedLattice α

See [Theorem 6.6][calugareanu].

theorem complementedLattice_of_isAtomistic {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [IsAtomistic α] : ComplementedLattice α

See [Theorem 6.6][calugareanu].

theorem complementedLattice_iff_isAtomistic {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] : ComplementedLattice α ↔ IsAtomistic α