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
• CompleteLattice.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, CompleteLattice.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 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

def CompleteLattice.IsCompactElement {α : Type u_3} [CompleteLattice α] (k : α) : Prop

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

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

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.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.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 ≤ ⨆ i ∈ s, 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 : ∀ 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, CompleteLattice.IsCompactElement (f x)) : CompleteLattice.IsCompactElement (s.sup f)

theorem CompleteLattice.WellFounded.isSupFiniteCompact (α : Type u_2) [CompleteLattice α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) : CompleteLattice.IsSupFiniteCompact α

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

theorem CompleteLattice.IsSupClosedCompact.wellFounded (α : Type u_2) [CompleteLattice α] (h : CompleteLattice.IsSupClosedCompact α) : WellFounded fun (x1 x2 : α) => x1 > x2

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

theorem CompleteLattice.wellFounded_characterisations (α : Type u_2) [CompleteLattice α] : [WellFounded fun (x1 x2 : α) => x1 > x2, CompleteLattice.IsSupFiniteCompact α, CompleteLattice.IsSupClosedCompact α, ∀ (k : α), CompleteLattice.IsCompactElement k].TFAE

theorem CompleteLattice.wellFounded_iff_isSupFiniteCompact (α : Type u_2) [CompleteLattice α] : (WellFounded fun (x1 x2 : α) => x1 > x2) ↔ CompleteLattice.IsSupFiniteCompact α

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

theorem CompleteLattice.isSupClosedCompact_iff_wellFounded (α : Type u_2) [CompleteLattice α] : CompleteLattice.IsSupClosedCompact α ↔ WellFounded fun (x1 x2 : α) => x1 > x2

theorem CompleteLattice.IsSupFiniteCompact.wellFounded (α : Type u_2) [CompleteLattice α] : CompleteLattice.IsSupFiniteCompact α → WellFounded fun (x1 x2 : α) => x1 > x2

Alias of the reverse direction of CompleteLattice.wellFounded_iff_isSupFiniteCompact.

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

Alias of the reverse direction of CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact.

theorem WellFounded.isSupClosedCompact (α : Type u_2) [CompleteLattice α] : (WellFounded fun (x1 x2 : α) => x1 > x2) → CompleteLattice.IsSupClosedCompact α

Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFounded.

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 ≠ ⊥) : 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, CompleteLattice.IsCompactElement x) ∧ sSup s = x

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

theorem IsCompactlyGenerated.exists_sSup_eq {α : Type u_3} : ∀ {inst : CompleteLattice α} [self : IsCompactlyGenerated α] (x : α), ∃ (s : Set α), (∀ x ∈ s, 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 sSup_compact_le_eq {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] (b : α) : sSup {c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b} = b

@[simp]

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

theorem le_iff_compact_le_imp {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {b : α} : a ≤ b ↔ ∀ (c : α), CompleteLattice.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 CompleteLattice.setIndependent_iff_finite {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {s : Set α} : CompleteLattice.SetIndependent s ↔ ∀ (t : Finset α), ↑t ⊆ s → CompleteLattice.SetIndependent ↑t

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)

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

theorem CompleteLattice.isCompactlyGenerated_of_wellFounded {α : Type u_2} [CompleteLattice α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) : IsCompactlyGenerated α

theorem CompleteLattice.Iic_coatomic_of_compact_element {α : Type u_2} [CompleteLattice α] {k : α} (h : CompleteLattice.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 : CompleteLattice.IsCompactElement ⊤) : IsCoatomic α

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

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 ∈ 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_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 ∈ 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 α