The MacNeille or Dedekind–MacNeille (not ‘Mac Neille’) completion of a lattice (or even poset) is the universal complete lattice containing . In Pos, the MacNeille completion of an object is its injective hull.
A MacNeille completion of is any complete lattice containing as a sublattice, with both join-dense and meet-dense in (that is, each element of is both a join of elements of and a meet of elements of ), and such that if is another such lattice then there is a unique isomorphism from to fixing . In particular, this allows us to speak of the MacNeille completion of .
A MacNeille completion may be constructed as follows. Let be the set of all subsets of , ordered by inclusion. For any let
These form a Galois connection on ; the condition defines a closure operation on . The lattice of all -closed subsets of is complete. For any the set is the principal ideal generated by . Then is an isomorphic embedding of into the complete lattice that preserves all least upper bounds (joins) and greatest lower bounds (meets) existing in .
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 , but the extended real line . In constructive mathematics, we may get additional finite elements, since the Dedekind sections are not required to be located; if we then drop , we get the MacNeille real numbers.