# 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

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
def CompleteLattice.IsCompactElement {α : Type u_3} [] (k : α) :

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} [] (k : α) :
∀ (ι : Type u) (s : ια), k iSup s∃ (t : ), k t.sup s
theorem CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le (α : Type u_2) [] (k : α) :
∀ (s : Set α), s.NonemptyDirectedOn (fun (x x_1 : α) => x x_1) 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) [] {k : α} (hk : ) {ι : Type u_3} (f : ια) (h : k ⨆ (i : ι), f i) :
∃ (s : ), k is, f i
theorem CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt {α : Type u_3} [] {k : α} (hk : ) {s : Set α} (hemp : s.Nonempty) (hdir : DirectedOn (fun (x x_1 : α) => x x_1) 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} [] {f : βα} (s : ) (h : xs, ) :
theorem CompleteLattice.WellFounded.isSupFiniteCompact (α : Type u_2) [] (h : WellFounded fun (x x_1 : α) => x > x_1) :
theorem CompleteLattice.IsSupClosedCompact.wellFounded (α : Type u_2) [] :
WellFounded fun (x x_1 : α) => x > x_1
theorem CompleteLattice.wellFounded_characterisations (α : Type u_2) [] :
[WellFounded fun (x x_1 : α) => x > x_1, , , ∀ (k : α), ].TFAE
theorem CompleteLattice.wellFounded_iff_isSupFiniteCompact (α : Type u_2) [] :
(WellFounded fun (x x_1 : α) => x > x_1)
theorem CompleteLattice.isSupClosedCompact_iff_wellFounded (α : Type u_2) [] :
WellFounded fun (x x_1 : α) => x > x_1
theorem CompleteLattice.IsSupFiniteCompact.wellFounded (α : Type u_2) [] :
WellFounded fun (x x_1 : α) => x > x_1

Alias of the reverse direction of CompleteLattice.wellFounded_iff_isSupFiniteCompact.

Alias of the reverse direction of CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact.

theorem WellFounded.isSupClosedCompact (α : Type u_2) [] :
(WellFounded fun (x x_1 : α) => x > x_1)

Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFounded.

theorem CompleteLattice.WellFounded.finite_of_setIndependent {α : Type u_2} [] (h : WellFounded fun (x x_1 : α) => x > x_1) {s : Set α} (hs : ) :
s.Finite
theorem CompleteLattice.WellFounded.finite_ne_bot_of_independent {α : Type u_2} [] (hwf : WellFounded fun (x x_1 : α) => x > x_1) {ι : Type u_3} {t : ια} (ht : ) :
{i : ι | t i }.Finite
theorem CompleteLattice.WellFounded.finite_of_independent {α : Type u_2} [] (hwf : WellFounded fun (x x_1 : α) => x > x_1) {ι : Type u_3} {t : ια} (ht : ) (h_ne_bot : ∀ (i : ι), t i ) :
class IsCompactlyGenerated (α : Type u_3) [] :

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

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

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

Instances
theorem IsCompactlyGenerated.exists_sSup_eq {α : Type u_3} [] [self : ] (x : α) :
∃ (s : Set α), () 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} [] (b : α) :
sSup {c : α | } = b
@[simp]
theorem sSup_compact_eq_top {α : Type u_2} [] :
sSup {a : α | } =
theorem le_iff_compact_le_imp {α : Type u_2} [] {a : α} {b : α} :
a b ∀ (c : α), c ac b
theorem DirectedOn.inf_sSup_eq {α : Type u_2} [] {a : α} {s : Set α} (h : DirectedOn (fun (x x_1 : α) => x x_1) 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} [] {a : α} {s : Set α} (h : DirectedOn (fun (x x_1 : α) => x x_1) 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} {f : ια} [] {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 : ια} [] {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} [] {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} [] {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 : ια} [] {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 : ια} [] {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} [] {a : α} {s : Set α} :
a sSup s = ⨆ (t : ), ⨆ (_ : t s), a t.sup id

This property is equivalent to α being upper continuous.

theorem CompleteLattice.setIndependent_iff_finite {α : Type u_2} [] {s : Set α} :
∀ (t : ), t s
theorem CompleteLattice.independent_iff_supIndep_of_injOn {α : Type u_2} [] {ι : Type u_3} {f : ια} (hf : Set.InjOn f {i : ι | f i }) :
∀ (s : ), s.SupIndep f
theorem CompleteLattice.setIndependent_iUnion_of_directed {α : Type u_2} [] {η : Type u_3} {s : ηSet α} (hs : Directed (fun (x x_1 : Set α) => x x_1) s) (h : ∀ (i : η), ) :
CompleteLattice.SetIndependent (⋃ (i : η), s i)
theorem CompleteLattice.independent_sUnion_of_directed {α : Type u_2} [] {s : Set (Set α)} (hs : DirectedOn (fun (x x_1 : Set α) => x x_1) s) (h : ) :
theorem CompleteLattice.isCompactlyGenerated_of_wellFounded {α : Type u_2} [] (h : WellFounded fun (x x_1 : α) => x > x_1) :

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]
instance isAtomic_of_complementedLattice {α : Type u_2} [] [] :
Equations
• =
@[instance 100]
instance isAtomistic_of_complementedLattice {α : Type u_2} [] [] :

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} [] [] (h : sSup {a : α | } = ) (b : α) :
∃ (s : Set α), IsCompl b (sSup s) ∀ ⦃a : α⦄, a s

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} [] [] (h : sSup {a : α | } = ) :
∃ (s : Set α), sSup s = ∀ ⦃a : α⦄, a s
theorem complementedLattice_of_sSup_atoms_eq_top {α : Type u_2} [] [] (h : sSup {a : α | } = ) :

See [Theorem 6.6][calugareanu].

theorem complementedLattice_of_isAtomistic {α : Type u_2} [] [] [] :

See [Theorem 6.6][calugareanu].