More formally: given a complete lattice and functions and , we have
where “section” means section of . Complete distributivity states that this inequality is an equality, for all . The same statement then holds upon switching and , i.e., complete distributivity is a self-dual property.
This appears as remark 4.3 in (Caramello 2011).
A complete totally ordered poset is completely distributive.
(Note: this uses the axiom of choice.) Suppose we had a strict inequality
Denote the left side by and the right by . Either there is no element strictly between and , or there is. In the former case, we have for each that , and so (using trichotomy) we have for some . Choosing such a for each , we obtain a section with for all , whence for this case, so that , contradiction. If there is with , we argue similarly to obtain a section with for all , whence , and we obtain a contradiction as before with replacing .
For a complete atomic Boolean algebra , it is classical that the canonical map , sending each to the set of atoms below it, is an isomorphism. Such power sets are products of copies of , which is completely distributive by the lemma, and products of completely distributive lattices are completely distributive.
In the other direction, suppose is completely distributive. Take , and by and . Sections of correspond to functions , and so complete distributivity gives
Write as abbreviation for , we have
so for some if . Notice that implies , from which we infer two things:
Whenever with , then ; therefore is an atom whenever ;
Provided that , the preceding point gives that is an atom below .
The last point shows every element has an atom below it, so that is atomic, as was to be shown.
A complete lattice is called constructively completely distributive (CCD) if the join-assigning morphism has a left adjoint, with the poset of downsets.
Completely distributive lattices correspond to tight Galois connections (Raney 1953). This generalizes to a correspondence between totally distributive toposes and essential localizations (Lucyshyn-Wright 2011).
CCD lattices are precisely the nuclear objects in the category of complete lattices.
The (bi-) category with CCD lattices and sup-preserving maps is the idempotent splitting of the (bi-) category of relations . This plays an important role in domain-theoretical approaches to the semantics of linear logic.
R. Guitart, J. Riguet, Enveloppe Karoubienne de Catégories de Kleisli , Cah. Top. Geom. Diff. Cat. XXXIII no.3 (1992) pp.261-266. (pdf)
G. N. Raney, Tight Galois Connections and Complete Distributivity , Trans.Amer.Math.Soc 97 (1960) pp.418-426. (pdf)
R. Rosebrugh, R. J. Wood, Constructive complete distributivity IV , App. Cat. Struc. 2 (1994) pp.119-144. (preprint)
I. Stubbe, Towards “Dynamic Domains”: Totally Continuous Complete Q-Categories , Theo. Comp. Sci. 373 no.1-2 (2007) pp.142-160.