scilib documentation

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 #

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 (complete_lattice.compactly_generated_of_well_founded).

References #

Tags #

complete lattice, well-founded, compact

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

Alias of the forward direction of directed_on_range.

source
def complete_lattice.is_sup_closed_compact (α : Type u_2) [complete_lattice α] :
Prop

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

Equations
source
def complete_lattice.is_Sup_finite_compact (α : Type u_2) [complete_lattice α] :
Prop

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

Equations
source
def complete_lattice.is_compact_element {α : Type u_1} [complete_lattice α] (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
source
theorem complete_lattice.is_compact_element_iff {α : Type u} [complete_lattice α] (k : α) :
complete_lattice.is_compact_element k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ supr s → (∃ (t : finset ι), k ≤ t.sup s)
source
theorem complete_lattice.is_compact_element_iff_le_of_directed_Sup_le (α : Type u_2) [complete_lattice α] (k : α) :
complete_lattice.is_compact_element k ↔ ∀ (s : set α), s.nonempty → directed_on has_le.le s → k ≤ has_Sup.Sup s → (∃ (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.

source
theorem complete_lattice.is_compact_element.exists_finset_of_le_supr (α : Type u_2) [complete_lattice α] {k : α} (hk : complete_lattice.is_compact_element k) {ι : Type u_1} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i) :
∃ (s : finset ι), k ≤ ⨆ (i : ι) (H : i ∈ s), f i
source
theorem complete_lattice.is_compact_element.directed_Sup_lt_of_lt {α : Type u_1} [complete_lattice α] {k : α} (hk : complete_lattice.is_compact_element k) {s : set α} (hemp : s.nonempty) (hdir : directed_on has_le.le s) (hbelow : ∀ (x : α), x ∈ s → x < k) :
has_Sup.Sup s < k

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

source
theorem complete_lattice.finset_sup_compact_of_compact {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} (s : finset β) (h : ∀ (x : β), x ∈ s → complete_lattice.is_compact_element (f x)) :
complete_lattice.is_compact_element (s.sup f)
source
theorem complete_lattice.well_founded.is_Sup_finite_compact (α : Type u_2) [complete_lattice α] (h : well_founded gt) :
complete_lattice.is_Sup_finite_compact α
source
theorem complete_lattice.is_Sup_finite_compact.is_sup_closed_compact (α : Type u_2) [complete_lattice α] (h : complete_lattice.is_Sup_finite_compact α) :
complete_lattice.is_sup_closed_compact α
source
theorem complete_lattice.is_sup_closed_compact.well_founded (α : Type u_2) [complete_lattice α] (h : complete_lattice.is_sup_closed_compact α) :
well_founded gt
source
theorem complete_lattice.is_Sup_finite_compact_iff_all_elements_compact (α : Type u_2) [complete_lattice α] :
complete_lattice.is_Sup_finite_compact α ↔ ∀ (k : α), complete_lattice.is_compact_element k
source
theorem complete_lattice.well_founded_characterisations (α : Type u_2) [complete_lattice α] :
[well_founded gt, complete_lattice.is_Sup_finite_compact α, complete_lattice.is_sup_closed_compact α, ∀ (k : α), complete_lattice.is_compact_element k].tfae
source
theorem complete_lattice.well_founded_iff_is_Sup_finite_compact (α : Type u_2) [complete_lattice α] :
well_founded gt ↔ complete_lattice.is_Sup_finite_compact α
source
theorem complete_lattice.is_Sup_finite_compact_iff_is_sup_closed_compact (α : Type u_2) [complete_lattice α] :
complete_lattice.is_Sup_finite_compact α ↔ complete_lattice.is_sup_closed_compact α
source
theorem complete_lattice.is_sup_closed_compact_iff_well_founded (α : Type u_2) [complete_lattice α] :
complete_lattice.is_sup_closed_compact α ↔ well_founded gt
source
theorem complete_lattice.is_Sup_finite_compact.well_founded (α : Type u_2) [complete_lattice α] :
complete_lattice.is_Sup_finite_compact α → well_founded gt

Alias of the reverse direction of complete_lattice.well_founded_iff_is_Sup_finite_compact.

source
theorem complete_lattice.is_sup_closed_compact.is_Sup_finite_compact (α : Type u_2) [complete_lattice α] :
complete_lattice.is_sup_closed_compact α → complete_lattice.is_Sup_finite_compact α

Alias of the reverse direction of complete_lattice.is_Sup_finite_compact_iff_is_sup_closed_compact.

source
theorem well_founded.is_sup_closed_compact (α : Type u_2) [complete_lattice α] :
well_founded gt → complete_lattice.is_sup_closed_compact α

Alias of the reverse direction of complete_lattice.is_sup_closed_compact_iff_well_founded.

source
theorem complete_lattice.well_founded.finite_of_set_independent {α : Type u_2} [complete_lattice α] (h : well_founded gt) {s : set α} (hs : complete_lattice.set_independent s) :
s.finite
source
theorem complete_lattice.well_founded.finite_of_independent {α : Type u_2} [complete_lattice α] (hwf : well_founded gt) {ι : Type u_1} {t : ι → α} (ht : complete_lattice.independent t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :
finite ι
source
@[class]
structure is_compactly_generated (α : Type u_3) [complete_lattice α] :
Prop

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

Instances of this typeclass
source
@[simp]
theorem Sup_compact_le_eq {α : Type u_2} [complete_lattice α] [is_compactly_generated α] (b : α) :
has_Sup.Sup {c : α | complete_lattice.is_compact_element c ∧ c ≤ b} = b
source
@[simp]
theorem Sup_compact_eq_top {α : Type u_2} [complete_lattice α] [is_compactly_generated α] :
has_Sup.Sup {a : α | complete_lattice.is_compact_element a} = ⊤
source
theorem le_iff_compact_le_imp {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {a b : α} :
a ≤ b ↔ ∀ (c : α), complete_lattice.is_compact_element c → c ≤ a → c ≤ b
source
theorem directed_on.inf_Sup_eq {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {a : α} {s : set α} (h : directed_on has_le.le s) :
a ⊓ has_Sup.Sup s = ⨆ (b : α) (H : b ∈ s), a ⊓ b

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

source
@[protected]
theorem directed_on.Sup_inf_eq {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {a : α} {s : set α} (h : directed_on has_le.le s) :
has_Sup.Sup s ⊓ a = ⨆ (b : α) (H : b ∈ s), b ⊓ a

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

source
@[protected]
theorem directed.inf_supr_eq {ι : Sort u_1} {α : Type u_2} [complete_lattice α] {f : ι → α} [is_compactly_generated α] {a : α} (h : directed has_le.le f) :
(a ⊓ ⨆ (i : ι), f i) = ⨆ (i : ι), a ⊓ f i
source
@[protected]
theorem directed.supr_inf_eq {ι : Sort u_1} {α : Type u_2} [complete_lattice α] {f : ι → α} [is_compactly_generated α] {a : α} (h : directed has_le.le f) :
(⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
source
@[protected]
theorem directed_on.disjoint_Sup_right {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {a : α} {s : set α} (h : directed_on has_le.le s) :
disjoint a (has_Sup.Sup s) ↔ ∀ ⦃b : α⦄, b ∈ s → disjoint a b
source
@[protected]
theorem directed_on.disjoint_Sup_left {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {a : α} {s : set α} (h : directed_on has_le.le s) :
disjoint (has_Sup.Sup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → disjoint b a
source
@[protected]
theorem directed.disjoint_supr_right {ι : Sort u_1} {α : Type u_2} [complete_lattice α] {f : ι → α} [is_compactly_generated α] {a : α} (h : directed has_le.le f) :
disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), disjoint a (f i)
source
@[protected]
theorem directed.disjoint_supr_left {ι : Sort u_1} {α : Type u_2} [complete_lattice α] {f : ι → α} [is_compactly_generated α] {a : α} (h : directed has_le.le f) :
disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), disjoint (f i) a
source
theorem inf_Sup_eq_supr_inf_sup_finset {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {a : α} {s : set α} :
a ⊓ has_Sup.Sup s = ⨆ (t : finset α) (H : ↑t ⊆ s), a ⊓ t.sup id

This property is equivalent to α being upper continuous.

source
theorem complete_lattice.set_independent_iff_finite {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {s : set α} :
complete_lattice.set_independent s ↔ ∀ (t : finset α), ↑t ⊆ s → complete_lattice.set_independent ↑t
source
theorem complete_lattice.set_independent_Union_of_directed {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {η : Type u_1} {s : η → set α} (hs : directed has_subset.subset s) (h : ∀ (i : η), complete_lattice.set_independent (s i)) :
complete_lattice.set_independent (⋃ (i : η), s i)
source
theorem complete_lattice.independent_sUnion_of_directed {α : Type u_2} [complete_lattice α] [is_compactly_generated α] {s : set (set α)} (hs : directed_on has_subset.subset s) (h : ∀ (a : set α), a ∈ s → complete_lattice.set_independent a) :
complete_lattice.set_independent (⋃₀ s)
source
theorem complete_lattice.compactly_generated_of_well_founded {α : Type u_2} [complete_lattice α] (h : well_founded gt) :
is_compactly_generated α
source
theorem complete_lattice.Iic_coatomic_of_compact_element {α : Type u_2} [complete_lattice α] {k : α} (h : complete_lattice.is_compact_element k) :
is_coatomic ↥(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.

source
theorem complete_lattice.coatomic_of_top_compact {α : Type u_2} [complete_lattice α] (h : complete_lattice.is_compact_element ⊤) :
is_coatomic α
source
@[protected, instance]
def is_atomic_of_complemented_lattice {α : Type u_2} [complete_lattice α] [is_modular_lattice α] [is_compactly_generated α] [complemented_lattice α] :
is_atomic α
source
@[protected, instance]
def is_atomistic_of_complemented_lattice {α : Type u_2} [complete_lattice α] [is_modular_lattice α] [is_compactly_generated α] [complemented_lattice α] :
is_atomistic α

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.

source
theorem exists_set_independent_is_compl_Sup_atoms {α : Type u_2} [complete_lattice α] [is_modular_lattice α] [is_compactly_generated α] (h : has_Sup.Sup {a : α | is_atom a} = ⊤) (b : α) :
∃ (s : set α), complete_lattice.set_independent s ∧ is_compl b (has_Sup.Sup s) ∧ ∀ ⦃a : α⦄, a ∈ s → is_atom a

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.

source
theorem exists_set_independent_of_Sup_atoms_eq_top {α : Type u_2} [complete_lattice α] [is_modular_lattice α] [is_compactly_generated α] (h : has_Sup.Sup {a : α | is_atom a} = ⊤) :
∃ (s : set α), complete_lattice.set_independent s ∧ has_Sup.Sup s = ⊤ ∧ ∀ ⦃a : α⦄, a ∈ s → is_atom a
source
theorem complemented_lattice_of_Sup_atoms_eq_top {α : Type u_2} [complete_lattice α] [is_modular_lattice α] [is_compactly_generated α] (h : has_Sup.Sup {a : α | is_atom a} = ⊤) :
complemented_lattice α

See Theorem 6.6.

source
theorem complemented_lattice_of_is_atomistic {α : Type u_2} [complete_lattice α] [is_modular_lattice α] [is_compactly_generated α] [is_atomistic α] :
complemented_lattice α

See Theorem 6.6.

source
theorem complemented_lattice_iff_is_atomistic {α : Type u_2} [complete_lattice α] [is_modular_lattice α] [is_compactly_generated α] :
complemented_lattice α ↔ is_atomistic α