# mathlib3documentation

order.compactly_generated

# Compactness properties for complete lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• complete_lattice.is_sup_closed_compact
• complete_lattice.is_Sup_finite_compact
• complete_lattice.is_compact_element
• complete_lattice.is_compactly_generated

## Main results #

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

• well_founded (>)
• complete_lattice.is_sup_closed_compact
• complete_lattice.is_Sup_finite_compact
• ∀ k, complete_lattice.is_compact_element k

This is demonstrated by means of the following four lemmas:

• complete_lattice.well_founded.is_Sup_finite_compact
• complete_lattice.is_Sup_finite_compact.is_sup_closed_compact
• complete_lattice.is_sup_closed_compact.well_founded
• complete_lattice.is_Sup_finite_compact_iff_all_elements_compact

We also show well-founded lattices are compactly generated (complete_lattice.compactly_generated_of_well_founded).

## Tags #

complete lattice, well-founded, compact

@[protected]
theorem directed.directed_on_range {α : Type u} {ι : Sort w} {r : α α Prop} {f : ι α} :
f (set.range f)

Alias of the forward direction of directed_on_range.

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

Equations

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

Equations
def complete_lattice.is_compact_element {α : Type u_1} (k : α) :
Prop

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

Equations
theorem complete_lattice.is_compact_element_iff {α : Type u} (k : α) :
(ι : Type u) (s : ι α), k supr s ( (t : finset ι), k t.sup s)
theorem complete_lattice.is_compact_element_iff_le_of_directed_Sup_le (α : Type u_2) (k : α) :
(s : set α), s.nonempty k ( (x : α), x s k x)

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

theorem complete_lattice.is_compact_element.exists_finset_of_le_supr (α : Type u_2) {k : α} {ι : Type u_1} (f : ι α) (h : k (i : ι), f i) :
(s : finset ι), k (i : ι) (H : i s), f i
theorem complete_lattice.is_compact_element.directed_Sup_lt_of_lt {α : Type u_1} {k : α} {s : set α} (hemp : s.nonempty) (hdir : s) (hbelow : (x : α), x s x < k) :
< k

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

theorem complete_lattice.finset_sup_compact_of_compact {α : Type u_1} {β : Type u_2} {f : β α} (s : finset β) (h : (x : β), x s ) :

Alias of the reverse direction of complete_lattice.well_founded_iff_is_Sup_finite_compact.

Alias of the reverse direction of complete_lattice.is_Sup_finite_compact_iff_is_sup_closed_compact.

theorem well_founded.is_sup_closed_compact (α : Type u_2)  :

Alias of the reverse direction of complete_lattice.is_sup_closed_compact_iff_well_founded.

theorem complete_lattice.well_founded.finite_of_independent {α : Type u_2} (hwf : well_founded gt) {ι : Type u_1} {t : ι α} (ht : complete_lattice.independent t) (h_ne_bot : (i : ι), t i ) :
@[class]
structure is_compactly_generated (α : Type u_3)  :
Prop

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

Instances of this typeclass
@[simp]
theorem Sup_compact_le_eq {α : Type u_2} (b : α) :
has_Sup.Sup {c : α | = b
@[simp]
theorem Sup_compact_eq_top {α : Type u_2}  :
has_Sup.Sup {a : α | =
theorem le_iff_compact_le_imp {α : Type u_2} {a b : α} :
a b (c : α), c a c b
theorem directed_on.inf_Sup_eq {α : Type u_2} {a : α} {s : set α} (h : s) :
a = (b : α) (H : b s), a b

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

@[protected]
theorem directed_on.Sup_inf_eq {α : Type u_2} {a : α} {s : set α} (h : s) :
a = (b : α) (H : b s), b a

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

@[protected]
theorem directed.inf_supr_eq {ι : Sort u_1} {α : Type u_2} {f : ι α} {a : α} (h : f) :
(a (i : ι), f i) = (i : ι), a f i
@[protected]
theorem directed.supr_inf_eq {ι : Sort u_1} {α : Type u_2} {f : ι α} {a : α} (h : f) :
( (i : ι), f i) a = (i : ι), f i a
@[protected]
theorem directed_on.disjoint_Sup_right {α : Type u_2} {a : α} {s : set α} (h : s) :
(has_Sup.Sup s) ⦃b : α⦄, b s b
@[protected]
theorem directed_on.disjoint_Sup_left {α : Type u_2} {a : α} {s : set α} (h : s) :
a ⦃b : α⦄, b s a
@[protected]
theorem directed.disjoint_supr_right {ι : Sort u_1} {α : Type u_2} {f : ι α} {a : α} (h : f) :
( (i : ι), f i) (i : ι), (f i)
@[protected]
theorem directed.disjoint_supr_left {ι : Sort u_1} {α : Type u_2} {f : ι α} {a : α} (h : f) :
disjoint ( (i : ι), f i) a (i : ι), disjoint (f i) a
theorem inf_Sup_eq_supr_inf_sup_finset {α : Type u_2} {a : α} {s : set α} :
a = (t : finset α) (H : t s), a t.sup id

This property is equivalent to α being upper continuous.

theorem complete_lattice.set_independent_iff_finite {α : Type u_2} {s : set α} :
(t : finset α),
theorem complete_lattice.set_independent_Union_of_directed {α : Type u_2} {η : Type u_1} {s : η set α} (hs : s) (h : (i : η), ) :
theorem complete_lattice.independent_sUnion_of_directed {α : Type u_2} {s : set (set α)} (hs : s) (h : (a : set α), ) :
theorem complete_lattice.Iic_coatomic_of_compact_element {α : Type u_2} {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.

@[protected, instance]
@[protected, instance]

See Lemma 5.1.

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_set_independent_is_compl_Sup_atoms {α : Type u_2} (h : has_Sup.Sup {a : α | is_atom a} = ) (b : α) :
(s : set α), (has_Sup.Sup s) ⦃a : α⦄, a s

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

theorem exists_set_independent_of_Sup_atoms_eq_top {α : Type u_2} (h : has_Sup.Sup {a : α | is_atom a} = ) :
(s : set α), ⦃a : α⦄, a s