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 #
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
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
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.
A compact element k
has the property that any directed set lying strictly below k
has
its sSup
strictly below k
.
Alias of the reverse direction of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact
.
Alias of the reverse direction of CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact
.
Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT
.
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.
Instances
In a compactly generated complete lattice,
every element is the sSup
of some set of compact elements.
This property is sometimes referred to as α
being upper continuous.
This property is sometimes referred to as α
being upper continuous.
This property is equivalent to α
being upper continuous.
Alias of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact
.
Alias of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT
.
Alias of the reverse direction of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact
.
Alias of the reverse direction of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact
.
Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT
.
Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT
.
Alias of CompleteLattice.WellFoundedGT.finite_of_setIndependent
.
Alias of CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent
.
Alias of CompleteLattice.WellFoundedGT.finite_of_independent
.
Alias of CompleteLattice.isCompactlyGenerated_of_wellFoundedGT
.
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.
Equations
- ⋯ = ⋯
See Lemma 5.1.
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.
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
.
See Theorem 6.6.
See Theorem 6.6.