nLab MacNeille completion

MacNeille completion

MacNeille completion


The MacNeille or Dedekind–MacNeille (not ‘Mac Neille’) completion of a lattice (or even poset) LL is the universal complete lattice containing LL. In Pos, the MacNeille completion of an object is its injective hull.


A MacNeille completion of LL is any complete lattice CC containing LL as a sublattice, with LL both join-dense and meet-dense in CC (that is, each element of CC is both a join of elements of LL and a meet of elements of LL), and such that if CC' is another such lattice then there is a unique isomorphism from CC to CC' fixing LL. In particular, this allows us to speak of the MacNeille completion of LL.

A MacNeille completion may be constructed as follows. Let P(L)P(L) be the set of all subsets of LL, ordered by inclusion. For any XP(L)X \in P(L) let

  • X Δ={αLxX.αx}X^{\Delta} = \{\alpha \in L \mid \forall x \in X . \alpha \geq x \}

  • X ={αLxX.αx}X^{\nabla} = \{\alpha \in L \mid \forall x \in X . \alpha \leq x \}

These form a Galois connection on P(L)P(L); the condition ϕ(X)=(X Δ) \phi(X) = (X^{\Delta})^{\nabla} defines a closure operation ϕ\phi on P(L)P(L). The lattice CC of all ϕ\phi-closed subsets of LL is complete. For any xLx \in L the set i(x)=({x} Δ) i(x) = (\{x\}^{\Delta})^{\nabla} is the principal ideal generated by xx. Then ii is an isomorphic embedding of LL into the complete lattice CC that preserves all least upper bounds (joins) and greatest lower bounds (meets) existing in LL.


When applied to the ordered set of rational numbers, the construction described above gives the completion of the set of rational numbers by Dedekind sections, including the empty sections. Thus we get, not the real line =],[\mathbb{R} = {]{-\infty},\infty[}, but the extended real line ¯=[,]\overline{\mathbb{R}} = [-\infty,\infty]. In constructive mathematics, we may get additional finite elements, since the Dedekind sections are not required to be located; if we then drop ±\pm\infty, we get the (bounded) MacNeille real numbers.


Last revised on September 9, 2019 at 19:42:19. See the history of this page for a list of all contributions to it.