nLab completely distributive lattice

Redirected from "constructive completely distributive lattices".
Contents

Contents

Definition

A completely distributive lattice is a complete lattice LL in which arbitrary joins and arbitrary meets distribute over each other.

More formally: given a complete lattice LL and functions p:JIp: J \to I and f:JLf: J \to L, we have

iI jp 1(i)f(j) sectionss:IJ iIf(s(i))\bigwedge_{i \in I} \bigvee_{j \in p^{-1}(i)} f(j) \geq \bigvee_{sections\; s: I \to J} \bigwedge_{i \in I} f(s(i))

where “section” means section of pp. Complete distributivity states that this inequality is an equality, for all f,pf, p. The same statement then holds upon switching \bigwedge and \bigvee, i.e., complete distributivity is a self-dual property.

Properties

Algebraic lattices

Proposition

The category of Alexandroff locales is equivalent to that of completely distributive algebraic lattices.

This appears as remark 4.3 in (Caramello 2011).

Completely distributive Boolean algebras

Lemma

A complete totally ordered poset is completely distributive.

Proof

(Note: this uses the axiom of choice.) Suppose we had a strict inequality

iI jp 1(i)f(j)> sectionss:IJ iIf(s(i)).\bigwedge_{i \in I} \bigvee_{j \in p^{-1}(i)} f(j) \gt \bigvee_{sections\; s: I \to J} \bigwedge_{i \in I} f(s(i)).

Denote the left side by xx and the right by yy. Either there is no element zz strictly between xx and yy, or there is. In the former case, we have for each ii that jp 1(i)f(j)x\bigvee_{j \in p^{-1}(i)} f(j) \geq x, and so (using trichotomy) we have f(j)>yf(j) \gt y for some jp 1(i)j \in p^{-1}(i). Choosing such a jj for each ii, we obtain a section ss with f(s(i))>yf(s(i)) \gt y for all yy, whence f(s(i))xf(s(i)) \geq x for this case, so that sectionss:IJ iIf(s(i))x>y\bigvee_{sections\; s: I \to J} \bigwedge_{i \in I} f(s(i)) \geq x \gt y, contradiction. If there is zz with x>z>yx \gt z \gt y, we argue similarly to obtain a section ss with f(s(i))>zf(s(i)) \gt z for all ii, whence iIf(s(i))z\bigwedge_{i \in I} f(s(i)) \geq z, and we obtain a contradiction as before with zz replacing xx.

Proposition

A complete Boolean algebra BB is completely distributive iff it is atomic (a CABA), i.e., is a power set as a Boolean algebra.

Proof

For a complete atomic Boolean algebra BB, it is classical that the canonical map BP(atoms(B))B \to P(atoms(B)), sending each bBb \in B to the set of atoms below it, is an isomorphism. Such power sets are products of copies of 2={01}\mathbf{2} = \{0 \leq 1\}, which is completely distributive by the lemma, and products of completely distributive lattices are completely distributive.

In the other direction, suppose BB is completely distributive. Take p=π 2:2×BBp = \pi_2: \mathbf{2} \times B \to B, and α:2×BB\alpha: \mathbf{2} \times B \to B by α(0,b)¬b\alpha(0, b) \coloneqq \neg b and α(1,b)b\alpha(1, b) \coloneqq b. Sections of pp correspond to functions g:B2g: B \to \mathbf{2}, and so complete distributivity gives

1= bB(b¬b)= g:B2 bBα(g(b),b).1 = \bigwedge_{b \in B} (b \vee \neg b) = \bigvee_{g: B \to \mathbf{2}} \bigwedge_{b \in B} \alpha(g(b), b).

Write a(g)a(g) as abbreviation for bBα(g(b),b)\bigwedge_{b \in B} \alpha(g(b), b), we have

b=b1=b g:B2a(g)= g:B2ba(g)b = b \wedge 1 = b \wedge \bigvee_{g: B \to \mathbf{2}} a(g) = \bigvee_{g: B \to \mathbf{2}} b \wedge a(g)

so ba(g)0b \wedge a(g) \neq 0 for some gg if b0b \neq 0. Notice that ba(g)0b \wedge a(g) \neq 0 implies g(b)=1g(b) = 1, from which we infer two things:

  • Whenever ba(g)b \leq a(g) with b0b \neq 0, then a(g)α(g(b),b)=α(1,b)=ba(g) \leq \alpha(g(b), b) = \alpha(1, b) = b; therefore a(g)a(g) is an atom whenever a(g)0a(g) \neq 0;

  • Provided that ba(g)0b \wedge a(g) \neq 0, the preceding point gives that a(g)a(g) is an atom below ba(g)bb \wedge a(g) \leq b.

The last point shows every element bb has an atom a(g)a(g) below it, so that BB is atomic, as was to be shown.

Constructive complete distributivity

A complete lattice AA is called constructively completely distributive (CCD) if the join-assigning morphism DAAD A \to A has a left adjoint, with DAD A the poset of downsets.

Constructive complete distributivity is equivalent to complete distributivity if and only if the axiom of choice holds (Wood&Fawcett (1990)).

Constructively completely distributive lattices are an example of continuous algebras for a lax-idempotent 2-monad.

Remark

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 ℭℭ𝔇\mathfrak{CCD} with CCD lattices and sup-preserving maps is the idempotent splitting of the (bi-) category of relations ℜ𝔢𝔩\mathfrak{Rel}. This plays an important role in domain-theoretical approaches to the semantics of linear logic.

References

  • Barry Fawcett, Richard J. Wood, Constructive complete distributivity I , Math. Proc. Camb. Phil. Soc. 107 (1990) 81-89 [doi:10.1017/S0305004100068377]

  • R. Guitart, J. Riguet, Enveloppe Karoubienne de Catégories de Kleisli , Cah. Top. Geom. Diff. Cat. XXXIII no.3 (1992) pp.261-266. (pdf)

  • R. Lucyshyn-Wright, Totally Distributive Toposes , arXiv.1108.4032 (2011). (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.

Last revised on April 27, 2023 at 06:25:58. See the history of this page for a list of all contributions to it.