\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{distributive lattice}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{category_theory}{}\paragraph*{{$(0,1)$-Category theory}}\label{category_theory}

[[!include (0,1)-category theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{alternative_characterizations}{Alternative characterizations}\dotfill \pageref*{alternative_characterizations} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{infinitely_distributive_property}{Infinitely distributive property}\dotfill \pageref*{infinitely_distributive_property} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{OppositeCategory}{Finite distributive lattices}\dotfill \pageref*{OppositeCategory} \linebreak
\noindent\hyperlink{categorification}{Categorification}\dotfill \pageref*{categorification} \linebreak
\noindent\hyperlink{completion}{Completion}\dotfill \pageref*{completion} \linebreak


\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

\begin{defn}
\label{}\hypertarget{}{}
A \textbf{distributive lattice} is a [[lattice]] in which [[join]] $\vee$ and [[meet]] $\wedge$ \emph{distribute} over each other, in that for all $x,y,z$ in the lattice, the \emph{distributivity laws} are satisfied:

\begin{itemize}%
\item $x \vee (y \wedge z) = (x \vee y) \wedge (x \vee z)$,
\item $x \wedge (y \vee z) = (x \wedge y) \vee (x \wedge z)$.

\end{itemize}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
The nullary forms of distributivity hold in any lattice:

\begin{itemize}%
\item $x \vee \top = \top$,
\item $x \wedge \bot = \bot$.

\end{itemize}
Distributive lattices and [[lattice]] [[homomorphisms]] form a [[concrete category]] [[DistLat]].

\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
Any lattice that satisfies one of the two binary distributivity laws must also satisfy the other; isn't that nice? (This may safely be left as an [[exercise]].) This convenience does \emph{not} extend to infinitary distributivity, however.

\end{remark}
\hypertarget{alternative_characterizations}{}\subsection*{{Alternative characterizations}}\label{alternative_characterizations}

As mentioned above, the theory of distributive lattices is self-dual, something that is proved in almost any account (or left as an exercise), but which is not manifestly obvious from the standard definition which chooses one of the two distributivity laws and goes from there. In this section we provide some other characterizations or axiomatizations which \emph{are} manifestly self-dual.

Here is one such characterization:

\begin{prop}
\label{sd1}\hypertarget{sd1}{}
A lattice is distributive if and only if the identity

\begin{displaymath}
(a \wedge b) \vee (a \wedge c) \vee (b \wedge c) = (a \vee b) \wedge (a \vee c) \wedge (b \vee c)
\end{displaymath}
is satisfied.

\end{prop}
Again this may be left as a (somewhat mechanical) exercise.

Perhaps more useful in practice is the characterization in terms of ``forbidden sublattices'' due to Birkhoff. Namely, introduce the ``pentagon'' $N_5$ as the 5-element lattice $\{\bot \leq a, b, c \leq \top\}$ where $b \leq c$ and $a$ is incomparable to $b, c$, so that $\bot = a \wedge c$ and $a \vee b = \top$. Introduce the ``thick diamond'' $M_3$ as the 5-element lattice $\{\bot \leq a', b', c' \leq \top\}$ with $a', b', c'$ pairwise incomparable. Both $N_5$ and $M_3$ are self-dual. Birkhoff's characterization is the following (manifestly self-dual) criterion.

\begin{theorem}
\label{}\hypertarget{}{}
A lattice $L$ is distributive if and only if there is no [[injective function|embedding]] of $N_5$ or $M_3$ into $L$ that preserves binary meets and binary joins.

\end{theorem}
This can be useful for determining distributivity or its failure, especially in cases where one can visualize a lattice via its [[Hasse diagram]].

The necessity of the forbidden sublattice condition is clear in view of the fact that the cancellation law stated in the next result fails in $N_5$ and $M_3$. This result gives another self-dual axiomatization of distributive lattices.

\begin{prop}
\label{sd2}\hypertarget{sd2}{}
A lattice $L$ is distributive if and only if the cancellation law holds: for all $y, z \in L$, we have $y = z$ whenever $x \wedge y = x \wedge z$ and $x \vee y = x \vee z$ (for some $x$).

\end{prop}
\begin{proof}
``Only if'': if $x \wedge y = x \wedge z$ and $x \vee y = x \vee z$, then

\begin{displaymath}
y = y \vee (x \wedge y) = y \vee (x \wedge z) = (y \vee x) \wedge (y \vee z) = (x \vee z) \wedge (y \vee z) = (x \wedge y) \vee z
\end{displaymath}
which implies $z \leq y$, and similarly we have $y \leq z$.

``If'': this is harder. Assuming the cancellation law for $L$, we first show $L$ is modular. Recall from [[modular lattice]] that for any lattice $L$ and $a, b \in L$, there is a covariant [[Galois connection]]

\begin{displaymath}
([a \wedge b, b] \to [a, a \vee b]: x \mapsto a \vee x) \; \dashv \; ([a, a \vee b] \to [a \wedge b, b]: y \mapsto b \wedge y)
\end{displaymath}
and that $L$ is \emph{modular} if this Galois connection is a [[Galois correspondence]] (or [[adjoint equivalence]]) for all $a, b$. Now, if $x \in [a \wedge b, b]$, then $a \vee x = a \vee (b \wedge (a \vee x))$ because $f = f g f$ for any Galois connection $f \dashv g$. From $a \wedge b \leq x \leq b$ we also have

\begin{displaymath}
a \wedge x = a \wedge b \wedge x = a \wedge b = a \wedge b \wedge (a \vee x)
\end{displaymath}
and so by cancellation of the $a$'s, we conclude $x = b \wedge (a \vee x)$. Similarly (dually), for $y \in [a, a \vee b]$, we have $y = a \vee (b \wedge y)$. Hence $L$ is modular.

Now we show $L$ is distributive. Let $x, y, z \in L$ and consider the three elements

\begin{displaymath}
\itexarray{
u & \coloneqq & [x \wedge (y \vee z)] \vee (y \wedge z) & = & [x \vee (y \wedge z)] \wedge (y \vee z) \\ 
v & \coloneqq & [y \wedge (x \vee z)] \vee (x \wedge z) & = & [y \vee (x \wedge z)] \wedge (x \vee z) \\ 
w & \coloneqq & [z \wedge (x \vee y)] \vee (x \wedge y) & = & [z \vee (x \wedge y)] \wedge (x \vee y)
}
\end{displaymath}
where the non-definitional equalities follow from modularity. Using the first expressions, we compute

\begin{displaymath}
\itexarray{
u \vee v & = & [x \wedge (y \vee z)] \vee (y \wedge z) \vee [y \wedge (x \vee z)] \vee (x \wedge z) \\ 
 & = & [x \wedge (y \vee z)] \vee [y \wedge (x \vee z)] \\ 
 & = & [(x \wedge (y \vee z)) \vee y] \wedge (x \vee z) \\ 
 & = & (x \vee y) \wedge (x \vee z) \wedge (y \vee z)
}
\end{displaymath}
where the third and fourth lines use modularity. By symmetry in the letters $x, y, z$, we also have $u \vee w = v \vee w = (x \vee y) \wedge (x \vee z) \wedge (y \vee z)$. Now the second expressions are dual to the first, so by duality we compute

\begin{displaymath}
u \wedge v = u \wedge w = v \wedge w = (x \wedge y) \vee (x \wedge z) \vee (y \wedge z).
\end{displaymath}
Now by cancellation of the $u$'s, we may conclude $v = w$, but in that case we obtain

\begin{displaymath}
(x \vee y) \wedge (x \vee z) \wedge (y \vee z) = v \vee w = v \wedge w = (x \wedge y) \vee (x \wedge z) \vee (y \wedge z)
\end{displaymath}
so that $L$ is distributive by Proposition \ref{sd1}.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
While the expressions for $u, v, w$ in the preceding proof may look as though they come out of thin air, the underlying idea is that the sublattice of $L$ generated by $x, y, z$ is the [[image]] of a lattice map $F(3) \to L$ out of the free modular lattice $F(3)$ on three elements. The only obstruction to distributivity in $F(3)$ is the presence of an $M_3$-sublattice appearing in the center of its \href{https://golem.ph.utexas.edu/category/2015/09/the_free_modular_lattice_on_3.html#c049685}{Hasse diagram}. The middle elements of that sublattice correspond to the formal expressions for $u, v, w$ given above, and the proof shows that under the cancellation law, we have $u = v = w$ in $L$, making the thick diamond collapse to a point in $L$ and removing the obstruction to distributivity.

\end{remark}
From Proposition \ref{sd2}, it is not very hard to deduce Birkhoff's theorem. The presence of a copy of $M_3$ or $N_5$ in a non-distributive lattice $L$ is deduced from a failure of the cancellation law where we have three elements $x, y, z$ with $x \wedge y = x \wedge z$, $x \vee y = x \vee z$, and $y \neq z$. If $y, z$ are comparable, say $y \leq z$, then the set $\{x \wedge y, x, y, z, x \vee y\}$ forms an $N_5$. If $y, z$ are incomparable, then we have either $y \vee z \lt x \vee y$, or $y \wedge z \gt x \wedge y$, or both $y \vee z = x \vee y$ and $y \wedge z = x \wedge y$; in the first two cases we get an $N_5$ (e.g., $\{x \wedge y, x, y, y \vee z, x \vee y\}$ for the first case), and in the third case the set $\{x \wedge y, x, y, z, x \vee y\}$ forms an $M_3$.

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

Any [[Boolean algebra]], and even any [[Heyting algebra]], is a distributive lattice.

Any [[linear order]] is a distributive lattice.

An [[integral domain]] is a [[Prüfer domain]] iff its lattice of [[ideals]] is distributive. The classical example is $\mathbb{Z}$; equivalently, the (opposite of the) multiplicative monoid $\mathbb{N}$ ordered by divisibility, with $1$ at the bottom and $0$ at the top.

The lattice of [[Young diagrams]] ordered by inclusion is distributive.

\hypertarget{infinitely_distributive_property}{}\subsection*{{Infinitely distributive property}}\label{infinitely_distributive_property}

A distributive lattice that is complete (not necessarily [[completely distributive lattice |completely distributive]]) may be \textbf{infinitely distributive} or said to satisfiy the \textbf{infinite distributive law} :

\begin{displaymath}
x \wedge (\bigvee_i y_i) = \bigvee_i (x\wedge y_i)
\end{displaymath}
This property is sufficient to give the lattice [[Heyting algebra]] stucture where the implication $a\Rightarrow b$ (or [[exponential object]] $b^a$) is:

\begin{displaymath}
(u \Rightarrow v) = \bigvee_{x \wedge u \leq v} x
\end{displaymath}
Note that this property does not imply the dual \textbf{co-infinitely distributive} property:

\begin{displaymath}
x \vee (\bigwedge_i y_i) = \bigwedge_i (x\vee y_i)
\end{displaymath}
Instead this dual gives the lattice [[co-Heyting algebra|co-Heyting]] structure where the co-implication or ``subtraction'' ($\backslash$) is

\begin{displaymath}
(u \backslash v) = \bigwedge_{u \leq v \vee x} x
\end{displaymath}
If a lattice has both properties, as in a [[completely distributive lattice]], then it has [[bi-Heyting algebra|bi-Heyting]] structure (both Heyting and co-Heyting) and the two exponentials are equal.

\begin{displaymath}
(u \Rightarrow v) = \bigvee_{x \wedge u \leq v} x \qquad  = \qquad (u \backslash v) = \bigwedge_{u \leq v \vee x} x
\end{displaymath}
\begin{quote}%
Does it make sense to define ``infinitely distributive property'' for non-complete lattices? (Something like: ``Whenever the join exists, it satisfies the infinite distributive law.'')


\end{quote}
\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{OppositeCategory}{}\subsubsection*{{Finite distributive lattices}}\label{OppositeCategory}

Since a finite distributive lattice is [[completely distributive lattice |completely distributive]] it is a bi-Heyting lattice, as shown above.

Let $FinDistLat$ be the category of finite distributive lattices and lattice homomorphisms, and let $FinPoset$ be the category of finite [[posets]] and order-preserving functions. These are contravariantly equivalent, thanks to the presence of an [[ambimorphic object]]:

\textbf{Proposition.} The [[opposite category]] of $FinDistLat$ is [[equivalence of categories|equivalent]] to $FinPoset$:

\begin{displaymath}
FinDistLat^{op} \simeq FinPoset
  \,.
\end{displaymath}
This equivalence is given by the hom-functor

\begin{displaymath}
[-,2] \;\colon\; FinDistLat^{op} \stackrel{\simeq}{\to} FinPoset
\end{displaymath}
where $2$ is the 2-element distributive lattice, and in the other direction by

\begin{displaymath}
[-,2] \;\colon\; FinPoset^{op} \stackrel{\simeq}{\to} FinDistLat
\end{displaymath}
where $2 = \{0,1\}$ is the 2-element poset with $0 \lt 1$.

This baby form of \textbf{Birkhoff duality} is (in one form or another) mentioned in many places; the formulation in terms of hom-functors may be found in

\begin{itemize}%
\item [[Gavin C. Wraith]], \emph{Using the generic interval}, Cah. Top. G\'e{}om. Diff. Cat. \textbf{XXXIV} 4 (1993) pp.259-266. (\href{http://archive.numdam.org/ARCHIVE/CTGDC/CTGDC_1993__34_4/CTGDC_1993__34_4_259_0/CTGDC_1993__34_4_259_0.pdf}{pdf})

\end{itemize}
Every finite distributive lattice has an underlying finite poset, and this defines a functor

\begin{displaymath}
U \;\colon\; FinDistLat \to FinPoset
\end{displaymath}
which has a left adjoint

\begin{displaymath}
F \;\colon\; FinPoset \to FinDistLat
\end{displaymath}
given by the composite

\begin{displaymath}
FinPoset \stackrel{hom(-, 2)^{op}}{\to} FinPoset^{op} \stackrel{[-, 2]}{\to} FinDistLat
\end{displaymath}
where $hom$ denotes the internal hom of $FinPos$ regarded as a cartesian closed category, so that

\begin{displaymath}
hom(-,2) \; \colon \; FinPoset^{op} \to FinPoset
\end{displaymath}
We can interpret this formula for $F$ as follows. To compute $FP$ for a finite poset $P$, first form the poset of upsets in $P$ with the reverse ordering (this is the free finite meet completion). Then form the distributive lattice of finitely generated downsets in that.

\hypertarget{categorification}{}\subsubsection*{{Categorification}}\label{categorification}

Every distributive lattice, regarded as a [[category]] (a [[(0,1)-category]]), is a \emph{[[coherent category]]}. Conversely, the notion of coherent category may be understood as a [[categorification]] of the notion of distributive lattice. A different categorification is the notion of [[distributive category]].

\hypertarget{completion}{}\subsubsection*{{Completion}}\label{completion}

The [[completely distributive lattice|completely distributive]] [[algebraic lattices]] (the [[frames of opens]] of [[Alexandroff locales]] ) form a [[reflective subcategory]] of that of all distributive lattices. The reflector is called \emph{[[canonical extension]]}.

[[!redirects distributive lattices]]



\end{document}