# Constructive lattice completion

The Dedekind–MacNeille Completion is the generalized way of completing an arbitrary lattice $$L$$. We will call $$C$$ the Dedekind–MacNeille completion of $$L$$ (I will not go into the details of the Completion but see the comment below.) The completion includes an embedding $$i: L \to C$$ which preserves existing arbitrary meets and joins. The completion is universal in the sense that for any other complete lattice $$C'$$ and map $$f: L \to C'$$ that preserves arbitrary meets and joins there exists a unique map $$g: C \to C'$$ which preserves arbitrary meets and joins such that $$f = g \circ i$$. (I'm still learning category theory so please let me know if any of the above is incorrect.)

I have found an alternative completion specifically for Heyting algebras, which instead of considering the powerset of a Heyting algebra $$H$$ only considers the subsets of $$H$$ which are called complete ideals. Which are essentially ideals that additionally contain the join of any subset of the ideal, if that join exists. This completion must be equivalent to the Dedekind–MacNeille Completion by the universal property, right?

This is of interest to me because I want to peform a completion in a setting that does not have access to the powerset axiom (particularly CZF). The standard approach is to develop lattice theory for classes and give up the fact that the completion of an arbitrary lattice is provably a set. Before I pursue this I want to tie up this loose end in my mind. Because initially I was under the impression that I may be able to collect the complete ideals into a set without use of the powerset axiom, but that seems to not be the case.

• "The completion requires one to order the powerset of $L$ such that it is a complete lattice"-The only ordering on the powerset of $L$ is a pre-ordering, and the quotient of this is a complete lattice. It is more proper to say the ordering relation on $L$ induces a Galois connection on $L$ which then induces closure operators on $L$, and the closed sets with respect to these closure operators are complete lattices. Oct 13, 2021 at 20:53
• @JosephVanName thanks! Oct 13, 2021 at 22:04
• You can show that if there is a complete lattice such that $\bot \neq \top$ then there is a set containing every subset $p$ of $\{0\}$ such that $\neg \neg 0 \in p \to 0 \in p$ (by considering the join of the set $\{ \top \;|\; 0 \in p\}$) and this is already not provable in CZF. So it doesn't matter which method you use to get a complete lattice - in any case it won't give something set sized in CZF.
– aws
Oct 14, 2021 at 19:27
• To show the set of $\neg \neg$-stable subsets is not provably a set, you can use e.g. the model in www2.mathematik.tu-darmstadt.de/~streicher/CIZF/rmczfnp.pdf . It is possible to show this directly, but also you can derive it from the fact that every set is subcountable in the model. If there was a set of all $\neg \neg$-stable subsets of $\{0\}$ you could use it with exponentiation to construct a set of all $\neg \neg$-stable subsets of $\mathbb{N}$. However, this cannot be subcountable by a diagonal argument.
– aws
Oct 18, 2021 at 2:50
• If we had a nontrivial set sized complete lattice L, we can construct a set containing every $\neg \neg$-stable subset of $\{0\}$ by considering all sets containing 0 if $x = \top$ for $x \in L$. This is as required, because given $p$ such that $\neg \neg p \to p$, we can define the join of the set $\{ \top \;|\; 0 \in p \}$. If $0 \in p$ then this is equal to top. On the other hand, suppose the join of the set is $\top$ and assume $0 \notin p$. In this case the set would be empty, and so its join would be $\bot$, giving a contradiction. Since $p$ is $\neg \neg$-stable we can deduce $0 \in p$.
– aws
Oct 18, 2021 at 3:00

Joseph Van Name’s answer is correct for the general case. However, the OP indicated in comments that they are interested in the case where $$L$$ is a Heyting algebra, and then it turns out that the Dedekind–MacNeille completion can be constructed by taking the set of complete ideals of $$L$$ ordered by inclusion. (I’m frankly quite surprised, since for Heyting algebras, typically ideals are broken, and what works are filters. But here it seems to be the opposite.)

Using the notation in Joseph Van Name’s answer, it suffices to show that if $$I\subseteq L$$ is a complete ideal, and $$a\in{\downarrow\uparrow}I$$, then $$a\in I$$. Now, if $$c\in L$$ is any element such that $$a\land b\le c$$ for all $$b\in I$$, then $$a\to c\in{\uparrow}I$$, hence $$a\le a\to c$$, i.e., $$a\le c$$. Thus, we have established $$a=\bigvee\{a\land b:b\in I\}=\bigvee\{b\in I:b\le a\}.$$ Since $$I$$ is a complete ideal, it follows that $$a\in I$$.

It is also easy to check that the Dedekind–MacNeille completion of $$L$$ is a Heyting algebra, with relative pseudocomplement operation (extending that of $$L$$) defined for complete ideals $$I$$, $$J$$ by $$I\to J=\{a\in L:I\cap{\downarrow}a\subseteq J\}.$$ In particular, $$I\to J$$ is itself a complete ideal: if $$a=\bigvee_ia_i$$ with $$a_i\in I\to J$$, and $$b\in I\cap{\downarrow}a$$, then $$b\land a_i\in J$$ for each $$i$$, and $$b=\bigvee_i(b\land a_i)$$, hence $$b\in J$$.

• Well, aws’s comment indicates otherwise, but I know next to nothing about CZF, so I cannot tell. Oct 17, 2021 at 6:27
• Additionally, you say “it suffices to show… if 𝑎∈↓↑𝐼, then 𝑎∈𝐼.” Is this because we are showing that every element in the dedekind completion is in the set of complete ideals? Oct 17, 2021 at 18:49
• No, that's trivial. We are showing the converse, that every complete ideal is in the completion. Oct 17, 2021 at 19:35
• This proof seems to hold for all Heyting semilattices $(X,\wedge,\rightarrow,1)$ (where finite joins do not necessarily exist) as well. Oct 18, 2021 at 16:21
• From this proof, we can conclude something stronger; if $(L,\wedge,\rightarrow,1)$ is a Heyting semi-lattice, and $D\subseteq L$ is downwards closed, then $\downarrow\uparrow D=\{\bigvee R\mid R\subseteq D,\bigvee R\,\text{exists}\}.$ Oct 20, 2021 at 18:01

I claim that for lattices, the Dedekind-MacNeille completion is generally different from simply the collection of all ideals that are closed under taking all least upper bounds.

If $$X$$ is a poset, and $$A\subseteq X$$, then let $${\uparrow}A$$ be the set of all upper bounds of $$A$$, and let $${\downarrow}A$$ be the set of all lower bounds of $$A$$ (if there is any possible confusion about the set $$X$$, then write $${\uparrow}_{X}A$$ for $${\uparrow}A$$ and $${\downarrow}_{X}A$$ for $${\downarrow}A$$).

The Dedekind-MacNeille completion $$DM(X)$$ of a poset $$X$$ is typically defined to be the collection of all sets of the form $${\downarrow}A$$ where $$A\subseteq X$$. Equivalently, $$DM(X)$$ is the collection of all subsets $$A\subseteq X$$ such that $$A={\downarrow\uparrow}A$$. Clearly, each set of the form $${\downarrow}A$$ is downwards closed and also closed under taking all least upper bounds. However, I claim that even for lattices, there are subsets that are closed under taking all least upper bounds which are not of the form $${\downarrow}A$$.

If $$C$$ is a set and $$\lambda$$ is a cardinal, then define $$P_{\lambda}(C)$$ to be $$\{R\subseteq C:|R|<\lambda\}$$. Let $$A,B$$ be infinite sets with $$A\subseteq B,A\neq B$$. Then let $$X=P_{\omega}(B)$$. Then whenever $$\mathcal{R}\subseteq P_{\omega}(A)$$ is a subset with a least upper bound in $$X$$, we necessarily have $$\bigvee\mathcal{R}\in P_{\omega}(A)$$, so $$P_{\omega}(A)$$ is an ideal in $$X$$ closed under taking all least upper bounds. On the other hand, $${\uparrow}_{X}P_{\omega}(A)=\emptyset$$, so $${\downarrow_{X}\uparrow_{X}}P_{\omega}(A)=X$$, so the ideal $$P_{\omega}(A)$$ is not contained in the Dedekind-MacNeille completion of $$X$$.

It is well known that if $$B$$ is a Boolean algebra, then the Dedekind-MacNeille completion $$DM(B)$$ is also a Boolean algebra, and $$DM(B)$$ is simply the collection of all complete ideals of $$B$$.

• The lattice that I am interested in completing is in fact a Heyting algebra. If $H$ is a Heyting algebra is $DM(H)$ a Heyting algebra? Is it also simply a collection of complete ideals? Oct 15, 2021 at 5:23
• "If H is a Heyting algebra is DM(H) a Heyting algebra?"-This is an interesting question. You should consider asking this as an entirely new question on this site. Oct 15, 2021 at 12:32
• Yes, the completion of a Heyting algebra is a Heyting algebra. More generally, the Dedekind–MacNeille completion of a residuated lattice is a residuated lattice. Oct 15, 2021 at 12:58