higherRT.tex

%%
% Toward a higher realizability topos
% Begun October 2024
%
%
\documentclass[12pt]{article}
\usepackage{amsmath,amssymb,amsthm,latexsym}
\usepackage{bm,bbm}
\usepackage[all,cmtip]{xy}
\input{diagxy}
%\CompileMatrices       
\usepackage{url}
%\usepackage{fullpage}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage[colorlinks=true,linkcolor=blue,anchorcolor=blue,citecolor=blue,filecolor=blue,urlcolor=blue]{hyperref}

\newcommand{\jcomment}[1]{\textcolor{JungleGreen}{[Jonas: #1]}}
\newcommand{\ednote}[1]{[\textit{\color{red}{#1}}]} % editorial note

% RT macros:
\newcommand{\natpair}[1]{\langle{#1}\rangle}
\newcommand{\such}{\;{\big|}\;}
\newcommand{\parto}{\mathrel{\rightharpoonup}}
\newcommand{\cc}{\colon}
\newcommand{\tcc}{\,{:}\,}
\newcommand{\pcacomb}[1]{\mathsf{#1}}
\newcommand{\brset}[1]{\left\{#1\right\}}
\newcommand{\defined}{\,{\downarrow}}
\newcommand{\divergent}{\,{\uparrow}}
\newcommand{\combK}{\pcacomb{K}}
\newcommand{\combS}{\pcacomb{S}}
\newcommand{\combI}{\pcacomb{I}}
\newcommand{\kleq}{\doteq}

\newcommand{\tand}{\ \text{\textnormal{and}}\ }
\newcommand{\tor}{\ \text{\textnormal{or}}\ }
\newcommand{\tiff}{\,\ \text{\textnormal{if and only if}}\ \,}

\newcommand{\finsetsym}{\mathsf{finset}}
\newcommand{\finset}[1]{\finsetsym\,#1}
\newcommand{\all}[3]{\forall\, #1 \,{\in}\, #2\,.\left(#3\right)}
\newcommand{\some}[3]{\exists\, #1 \,{\in}\, #2\,.\left(#3\right)}

\newcommand{\xulam}[2]{\lambda #1 .\,#2}
\newcommand{\xtlam}[3]{\lambda #1 \tcc #2\,.\,#3}



% categories
\newcommand{\cattwo}{\ensuremath{\mathbbm{2}}}
\newcommand{\A}{\ensuremath{\mathbb{A}}}
\newcommand{\B}{\ensuremath{\mathbb{B}}}
\newcommand{\C}{\ensuremath{\mathbb{C}}}
\newcommand{\D}{\ensuremath{\mathbb{D}}}
\newcommand{\N}{\ensuremath{\mathbb{N}}}
\newcommand{\T}{\ensuremath{\mathbb{T}}}
\renewcommand{\P}{\ensuremath{\mathbb{P}}}
\renewcommand{\AA}{\ensuremath{\mathcal{A}}}
\newcommand{\BB}{\ensuremath{\mathcal{B}}}
\newcommand{\CC}{\ensuremath{\mathcal{C}}}
\newcommand{\DD}{\ensuremath{\mathcal{D}}}
\newcommand{\EE}{\ensuremath{\mathcal{E}}}
\newcommand{\FF}{\ensuremath{\mathcal{F}}}
\newcommand{\PP}{\ensuremath{\mathcal{P}}}
\newcommand{\WW}{\ensuremath{\mathcal{W}}}

\newcommand{\op}[1]{\ensuremath{{#1}^{\mathsf{op}}}}
\newcommand{\pshx}[1]{\ensuremath{\mathsf{Set}^{\op{#1}}}}
\newcommand{\psh}[1]{\ensuremath{[\op{#1},\mathsf{Set}]}}
\newcommand{\pshat}[1]{\ensuremath{\widehat{#1}}}

\newcommand{\Set}{\ensuremath{\mathsf{Set}}}
\newcommand{\set}{\ensuremath{\mathsf{set}}}
\newcommand{\Cat}{\ensuremath{\mathsf{Cat}}}
\newcommand{\cat}{\ensuremath{\mathsf{cat}}}
\newcommand{\Pos}{\ensuremath{\mathsf{Pos}}}
\newcommand{\pos}{\ensuremath{\mathsf{pos}}}
\newcommand{\covpshx}[1]{\ensuremath{\mathsf{Set}^{#1}}}
\newcommand{\cSet}{\ensuremath{\mathsf{cSet}}}

\newcommand{\Hom}{\ensuremath{\mathsf{Hom}}}
\renewcommand{\hom}{\ensuremath{\mathsf{Hom}}}
\newcommand{\y}{\ensuremath{\mathsf{y}}} % Yoneda embedding
\newcommand{\elem}[1]{\textstyle\int\!{#1}}% category of elements
\newcommand{\colim}{\varinjlim}% colimit with subscript

\newcommand{\FP}{\ensuremath{\mathsf{FP}}}
\newcommand{\ModT}{\ensuremath{\mathsf{Mod}(\T)}}
\newcommand{\TAlg}{\ensuremath{\T\text{-}\mathsf{Alg}}}

% Algebras
\newcommand{\alg}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\algA}{\ensuremath{\mathsf{A}}}
\newcommand{\algB}{\ensuremath{\mathsf{B}}}
\newcommand{\algC}{\ensuremath{\mathsf{C}}}
\newcommand{\algD}{\ensuremath{\mathsf{D}}}

% arrows
\newcommand{\hook}{\ensuremath{\hookrightarrow}}
\newcommand{\mono}{\ensuremath{\rightarrowtail}}
\newcommand{\ra}{\ensuremath{\rightarrow}}
\newcommand{\cof}{\ensuremath{\rightarrowtail}}
\newcommand{\fib}{\ensuremath{\epi}}
\renewcommand{\to}{\ensuremath{\rightarrow}}
\newcommand{\too}{\ensuremath{\longrightarrow}}

% cubical sets
\newcommand{\I}{\ensuremath{\mathrm{I}}}
\newcommand{\II}{\ensuremath{\mathbb{I}}}
\renewcommand{\H}{\ensuremath{\mathbb{H}}}
\newcommand{\HH}{\ensuremath{\mathcal{H}}}

% type theory
\newcommand{\G}{\ensuremath{\Gamma}}
\newcommand{\defeq}{=_{\mathrm{def}}}
\newcommand{\type}{\mathsf{type}}       
\newcommand{\types}[2]{#1 \vdash #2:\type}
\newcommand{\Gtypes}[1]{\types{\Gamma}{#1}}
\newcommand{\term}[2]{#1\,:\,#2}
\newcommand{\terms}[2]{#1 \vdash #2}
\newcommand{\Gterms}[1]{\terms{\Gamma}{#1}}
\newcommand{\ext}[2]{{#1\!\centerdot\! #2}}
\newcommand{\ty}{\ensuremath{\,:\,}}
\newcommand{\pair}[1]{\ensuremath{\langle #1\rangle}}
\newcommand{\exdot}{\ensuremath{\!\centerdot\!}}
\newcommand{\texdot}{\ensuremath{\centerdot}}

% Id types
\newcommand{\Id}{\mathsf{Id}}
\newcommand{\id}[1]{\Id_{#1}}
\newcommand{\refl}{\mathsf{refl}}
\newcommand{\idrec}{\mathsf{idrec}}
\newcommand{\jay}{\mathsf{j}}
\renewcommand{\i}{\mathsf{i}}


% Universes
\newcommand{\U}{\ensuremath{\mathcal{U}}}
\newcommand{\UU}{\ensuremath{\,\dot{\mathcal{U}}}}
\newcommand{\V}{\ensuremath{\mathcal{V}}}
\newcommand{\VV}{\ensuremath{\dot{\mathcal{V}}}}
\newcommand{\SSet}{\ensuremath{\,\dot{\Set}}}
\newcommand{\sset}{\ensuremath{\,\dot{\set}}}
\newcommand{\Fib}{\ensuremath{\mathsf{Fib}}}
\newcommand{\FFib}{\ensuremath{\dot{\mathsf{Fib}}}}

% Adjunctions
\newcommand{\adjunction}[2]{%
  \begin{tabular}{c}
    $#1$ \\
    \noalign{
      \vskip 2pt      
      \hrule
      \vskip 1pt      
      \hrule
      \vskip 2pt      
      }
    $#2$
  \end{tabular}
  }

\newcommand{\adjunctionx}[3]{%
  \begin{tabular}{c}
    $#1$ \\
    \noalign{
      \vskip 2pt      
      \hrule
      \vskip 1pt
      \hrule
      \vskip 2pt      
      }
    $#2$ \\
    \noalign{
      \vskip 2pt      
      \hrule
      \vskip 1pt
      \hrule
      \vskip 2pt      
      }
    $#3$
  \end{tabular}
  }

\newcommand{\adjrule}{\noalign{\vskip 2pt \hrule \vskip 1pt \hrule \vskip 2pt}}
\newcommand{\longadjunction}[1]{
\begin{tabular}{>{$}c<{$}}
#1
\end{tabular}
}

% Commutative diagrams in tikz
\usepackage{tikz}
\usepackage{pdfpages}
\usepackage{tikz-cd}

\newcommand{\pbcorner}{\arrow[dr,phantom,"\lrcorner" very near start, shift right=.5ex]} % tikz pullback corners
\newcommand{\ppbcorner}{\arrow[drr,phantom,"\lrcorner" very near start, shift right=.5ex]}
\newcommand{\pocorner}{\arrow[dr,phantom,"\ulcorner" very near end]} % tikz pushout corners
\newcommand{\ppocorner}{\arrow[dr,phantom,"\ulcorner" very near end]}

\newcommand{\xypbcorner}[1][dr]{\save*!/#1-1.5pc/#1:(-1,1)@^{|-}\restore}% pullback corner in xypic


% Theorem styles
\newtheorem{theorem}{Theorem}
\newtheorem*{theorem*}{Theorem}
\newtheorem{proposition}[theorem]{Proposition} 
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary} 

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark} 
\newtheorem*{remarks*}{Remarks}
\newtheorem{example}[theorem]{Example}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Toward a higher realizability topos (Notes)}
\author{Steve Awodey}
\date{\today}
\maketitle

Here are some conventions:
%
\begin{itemize}
\item For a small category $\C$ let $\pshat{\C} = \psh{\C}$ be the category of presheaves, and
\[
\y : \C \hook\pshat{\C}
\]
the Yoneda embedding.
%
\item 

\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{PCAs}

We review the basic definitions of partial combinatory algebras and applicative morphisms, which can be found in \cite{Hoefstra, completions in realizability}.  For a partial
function $f\cc X \parto Y$  the notation $f x \defined$
means that $f$ is defined for the argument $x\in X$. For a partial binary operation $x\cdot y$,  the expression $x\cdot y\kleq u\cdot v$ means that if one side is defined then so is the other and they are equal. 

\begin{definition}
  A \emph{partial combinatory algebra (PCA)} $(A, \cdot, \combK, \combS)$ is a set $A$ together with a
  partial binary operation 
  \[
  \cdot \ \cc A \times A \parto A
  \]
  called \emph{application}, and distinguished elements $\combK, \combS \in A$,
  such that for all $x, y, z \in A$,
  %
  \begin{equation*}
    \combK x y \kleq x \;,
    \qquad
    \combS x y \defined \;,
    \qquad
    \combS x y z \kleq (x z)(y z) \;,
  \end{equation*}
  %
  where write $x y$ instead of $x \cdot y$,
  and associate application to the left. We only consider
  non-trivial PCAs, satisfying $\combK \neq \combS$.
\end{definition}

%\begin{example}
%  Scott's \emph{graph model} $\P = \PP{\N}$, \cite{Scott:76}, is a
%  model of the untyped $\lambda$-calculus, therefore a (total)
%  combinatory algebra. The algebraic lattice of continuous maps
%  $\P^\P$ is a retract of the algebraic lattice~$\P$. The embedding
%  $\Gamma\cc \P^\P \to \P$ is defined by
%                                %
%  \begin{equation*}
%    \Gamma f =
%    \brset{\natpair{m, n} \such n \in \N \tand
%      m \in f(\finset{n})
%      }\;,
%  \end{equation*}
%                                %
%  where $\natpair{m, n}$ is an effective pairing of natural numbers
%  and $\finset{n}$ is an effective enumeration of finite subsets
%  of~$\N$. The set $\Gamma f$ is called the \emph{graph} of~$f$. For
%  a continuous map $f\cc \P \to \P$ the graph~$\Gamma f$ uniquely
%  determines~$f$ because the value of~$f$ at any element $x \in \P$
%  is the union of values of~$f$ at finite subsets of~$x$. The
%  retraction $\Lambda\cc \P \to \P^\P$ is defined by
%                                %
%  \begin{equation*}
%    (\Lambda x) y =
%    \brset{m \in \N \such \some{n}{\N}{\natpair{m,n} \in x \tand
%        \finset{n} \subseteq y}}.
%  \end{equation*}
%                                %
%  Define application on~$\P$ by
%                                %
%  \begin{equation*}
%    x \cdot y = (\Lambda x) y \;,
%  \end{equation*}
%                                %
%  and $\lambda$-abstraction by
%                                %
%  \begin{equation*}
%    \xulam{u}{\phi(u)} = \Gamma(\xtlam{x}{\P}{\phi(x)}) \;.
%  \end{equation*}
%  %
%  Here $\phi(u)$ is an expression with $u$ occurring as a free
%  variable, and involving further $\lambda$-abstractions and
%  applications of elements of~$\P$. By taking $\combK =
%  \xulam{xy}{x}$ and $\combS = \xulam{xyz}{(xz)(yz)}$, $\P$ becomes a
%  total combinatory algebra for the above application operation.
%\end{example}
%

\begin{example}
  The \emph{first Kleene Algebra~$\N$} is the set of natural
  numbers~$\N$ equipped with \emph{Kleene application} $n \cdot m =
  \{n\} m$ which applies the $n$-th partial recursive function~$\{n\}$
  to~$m$.  The existence of~$\combK$ and~$\combS$ is a consequence of
  the s-m-n theorem~\cite{Rogers:87}.
\end{example}

%%%%%%%%%%%%%%%%%%%%%%
\section{Assemblies}

\begin{definition}
  An \emph{assembly} $(X, \alpha)$ over a PCA $\A$ is a set $X$ together with a map $\alpha : X \to \PP{A}$ such that $\alpha(x) \neq\emptyset$ for all $x\in X$. One says that the elements $a\in \alpha(x)\subseteq A$  \emph{realize} the element $x$.  Thus every element in the carrier $X$ of the assembly is realized by (at least one) $a\in A$. 
  
The assembly is called \emph{partitioned} if  the subsets $\alpha(x)\subseteq A$ are all singletons, so that each $x\in X$ has exactly one realizer.  In that case, we may regard $\alpha$ as a map $\alpha : X \to A$.

A \emph{morphism of assemblies} $f : (X, \alpha) \to (Y, \beta)$ is a function $f : X \to Y$ for which there is an element $\phi\in A$ such that, for all $x\in X$ and all $a\in \alpha(x)$, 
\[
\phi\cdot a \in \beta(f(x))\,.
\]
One says that ``$\phi$ \emph{tracks} $f$''.
\end{definition}

For \emph{partitioned} assemblies, this condition reduces to 
\[
\phi \cdot \alpha(x) \kleq \beta(f(x)) \,,
\]
which means that (the left action of) $\phi$ fits into a commutative diagram as follows.
\[
\begin{tikzcd}
X \ar[d, swap,"\alpha"]  \ar[r,"f"] & Y \ar[d, "\beta"] \\  
A \ar[r,swap,"{\phi\cdot(-)}"] & A	
 \end{tikzcd}
 \]

\begin{proposition}
The category $\mathsf{PAsm}$ of partitioned assemblies has all finite limits. The category $\mathsf{Asm}$ of assemblies is regular and locally cartesian closed.
\end{proposition}

%%%%%%%%%%%%%%%%%%%%%%
\section{Completions}


\begin{proposition} For any partial combinatory algebra $\A$,
\begin{enumerate}
\item
the category of assemblies is the regular completion of the category of partitioned assemblies,
\[
\mathsf{Asm} \ =\ \mathsf{PAsm}_{\mathsf{reg/lex}}\,,
\]
\item the \emph{realizability topos} $\mathsf{RT}(\A)$ is the exact completion of the lex category $\mathsf{PAsm}(\A)$, which can therefore be constructed as the exact completion of the regular category $\mathsf{Asm}(\A)$,
\[
\mathsf{RT(\A)}\ =\ \mathsf{Asm}(\A)_{\mathsf{ex/reg}} \ =\ \mathsf{PAsm}_{\mathsf{ex/lex}}(\A)\,.
\]
\end{enumerate}
The \emph{effective topos} ${\EE}{\!f\!f}$ is the realizability topos of the first Kleene Algebra, 
\[
{\EE}{\!f\!f} = \mathsf{RT(\N)}\,.
\]
\end{proposition}

In more detail, 

\bibliographystyle{alpha}
\bibliography{../references}

%%%
\end{document}
%%%

%%%%%%%%%%%%%%%%%%%%%%%
\section{Old Stuff}

\begin{proposition}
The presheaf topos $\pshat{\T}$ is the classifying topos for flat $\T$-algebras.  Specifically, for any Grothendieck topos $\EE$, the category of geometric morphisms $\EE \to \pshat{\T}$ is naturally equivalent to the category of $\FP$-functors $\FP(\T,\EE)$ and natural transformations, which may be identified with the category $\TAlg_{\mathrm{flat}}(\EE)$ of flat (internal) $\T$-algebras in $\EE$,
\[
\TAlg_{\mathrm{flat}}(\EE)\ \simeq\  \mathsf{Top}(\EE, \pshat{\T})\,.
\]
\end{proposition}

Now recall that $\T$ may be taken to be the opposite of the full subcategory of all finitely generated free algebras $\alg{F(n)}$ (in $\Set$),
\[
\op{\T}\ \cong\  {\TAlg_{\mathrm{fgf}}(\Set)}\,.
\]

Unwinding the refinement property of Lemma \ref{lemma:refinement} in terms of the theory $\T$, we obtain a syntactic criterion of flatness:

\begin{proposition}\label{prop:flatalgebra} 
For any algebraic theory \jcomment{this should be single-sorted, to make sense
of free algebras} $\T$ and any $\T$-algebra $\algA$ (in $\Set$), the following are
equivalent.
%
\begin{enumerate}
%
\item $\algA$ is flat, i.e.\ it is  a filtered colimit, in the category ${\TAlg}$, of finitely generated free algebras $\alg{F(n)}$. The index category of the colimit  may be taken to be the opposite category of elements of the $\FP$-functor $A : \T\to\Set$.
%
\item The left Kan extension $A_! : \pshat{\T}\to \Set$ is left exact, and is therefore the inverse image part of a geometric morphism
\[
A_!\dashv A^* : \Set\to\pshat{\C}\,.
\]
%
\item (Refinement)\label{refinemnent} for any $\T$-terms  $\tt{f}[\bf{x}], \tt{g}[\bf{x}]$ in $n$-variables ${\bf{x}}= \tt{x}_1, \dots, \tt{x}_n$, and any elements ${\bf{a}} = a_1, \dots, a_n  \in \algA$ satisfying the equation
\[
\tt{f}[\bf{a}] = {\tt{g}}[\bf{a}]\,,
\] 
there is some $k\in\N$ and terms ${\bf{s}[\bf{y}]} = {\tt{s}}_1[{\tt{y}}], \dots, {\tt{s}}_n[{\tt{y}}]$, in $k$-many variables ${\bf{y}} = {\tt{y}}_1, \dots, {\tt{y}}_k$ such that in $\T$,
\[
\tt{f}[{\bf{s}[\bf{y}]}] = {\tt{g}}[{\bf{s}[\bf{y}]}]
\] 
and for which there are $k$-many elements ${\bf{a'}} = a'_1, \dots, a'_k  \in \algA$ such that
\[
{\bf{a}}\ =\ {\bf{s}[\bf{a'}]} \,.
\] 
\ednote{ToDo: add the reduction from $m$-many pairs of terms $(\tt{f}_1[\bf{x}], \tt{g}_1[\bf{x}]), ..., (\tt{f}_m[\bf{x}], \tt{g}_m[\bf{x}])$ to a single pair of terms $(\tt{f}_1[\bf{x}], \tt{g}_1[\bf{x}])$.}
%
\end{enumerate}
\end{proposition}

Let us define the \emph{geometric theory of flat algebras} $\mathsf{Th}(\T,\mathrm{flat})$ to consist of all geometric formulas $\phi$ in the signature of $\T$ that are satisfied by all finitely generated free algebras $\alg{F(n)}$,
\[
\mathsf{Th}(\T,\mathrm{flat})\ :=\ \{\, \phi\ |\ \alg{F(n)}\models \phi\ \text{for all $n$}\,\} \,.
\]
Since satisfaction of geometric formulas is preserved by left exact left adjoints, any flat $\T$-algebra will also model all the formulas in $\mathsf{Th}(\T,\mathrm{flat})$. \ednote{elaborate!} In fact, the universal model $\mathcal{U}$ in the classifying topos $\pshat{\C}$ is easily seen to model exactly the formulas in $\mathsf{Th}(\T,\mathrm{flat})$ (by evaluating it at the objects of $\T$, which are exactly the models $\alg{F(n)}$), as does any image of it under (the inverse image of) any geometric morphism $\pshat{\C} \to \EE$.  But since these are \emph{all} of the models classified by the topos $\pshat{\T}$, we have that $\mathsf{Th}(\T,\mathrm{flat})$ is indeed exactly the geometric theory of flat $\T$-algebras.

\begin{proposition}
A $\T$-algebra $\algA$ in a topos $\EE$ is flat (i.e.\ a filtered colimit in $\TAlg(\EE)$ of finitely generated free algebras $\alg{F(n)}$) iff it is a model of the geometric theory $\mathsf{Th}(\T,\mathrm{flat})$,
\[
\algA\models_{\EE} \mathsf{Th}(\T,\mathrm{flat})\,.
\]
\end{proposition}

\ednote{fill in the proof, which is standard.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Flat theories}

The refinement condition ({\ref{refinemnent}) of Proposition \ref{prop:flatalgebra} is only a bit more explicit than saying that an algebra is a filtered colimit of finitely generated free ones (even if such a colimit can be reduced to a directed one, see \cite{AR:}).  But in some cases it can also be used to determine simplified axioms for $\mathsf{Th}(\T,\mathrm{flat})$.  This makes it possible to relate the present notion of flatness to the classical one from commutative algebra, given in terms of tensoring with monomorphisms, as will be considered in Section \ref{section:algebraic_flat}.

We next consider two cases in which such an axiomatization is possible.

\subsection{Monoids}

In a series of papers \cite{Grillet:69a,Grillet:69b, Grillet:76} the author Grillet studies flatness of commutative semigroups, both with and without units, and colimits thereof.  One result is the following:

\begin{proposition}[\cite{Grillet:76}, Theorem 2.1]
For a commutative monoid $\alg{M}$ the following are equivalent.
%
\begin{enumerate}
%
\item $\alg{M}$ is a filtered colimit of finitely generated free monoids $\alg{F}(n)$.
%
\item $\alg{M}$ has the ``Killing Interpretation Property'' (KIP).
%
\item $\alg{M}$ is \emph{cancellative}, has \emph{no units}, and if $a,b,c,d \in \alg{S}$ satisfy $$na + b = nc+d$$ for $n > 1$, then
\begin{align*}
a&= u + v\\
b &= nw+z\\
c &= u+w\\
d &= nv + z
\end{align*}
for some $u, v, w, z \in \alg{S}$. 
\end{enumerate}
%
\end{proposition}

 The KIP is essentially what we called Refinement in Proposition \ref{prop:flatalgebra}.   Cancellative means ..., no units means ....
 The proof proceeds by ...
 
 \ednote{add a brief summary} 
 
\subsection{Semilattices}

In \cite{BF-MD:78} the authors Bulman-Fleming and McDowell specialize the results of Grillet to (join) semilattices with and without unit and establish the following result.

\begin{proposition}[\cite{BF-MD:78}, Theorem 3.1]
A semilattice $\algA$ is flat iff it satisfies the following condition of \emph{distributivity}.
\begin{equation}\label{prop:flatequalsdist}\tag{D}
a \leq b\vee c\qquad\text{implies}\qquad a = b' \vee c'\ \ \text{for}\  b'\leq b\ \text{and}\ c'\leq c\,.
\end{equation}
\end{proposition} 

Our notion of flatness (directed colimit of fgf-algebras) is there called ``L-flat'', in reference to the theorem of Lazard \cite{L:1969}.  The proof proceeds by first reducing (L-)flatness to the previously mentioned  KIP, using the results of \cite{Grillet} and \cite{Shannon}.  As said, the KIP is essentially what we have called Refinement.  The main step of the proof is then the further reduction of KIP to the condition (D) using the following argument:
\ednote{summarize the proof of 2.7}. 

\bigskip

\ednote{Other theories to consider: (not nec.\ commutative) monoids, distributive lattices with and w/o $0,1$, abelian groups, commutative rings, frames, boolean algebras.}

\section{Algebraic flatness}\label{section:algebraic_flat}

\begin{definition}[Algebraically flat algebra]  Suppose the category $\TAlg$ has a tensor product $\alg{A} \otimes \alg{B}$. An object $\alg{A}$ will be called \emph{algebraically flat} (or \emph{$\otimes$-flat}) if the functor $$(-)\otimes \alg{A} : \TAlg \too \TAlg$$ preserves monos. 
%\[
%\begin{tikzcd}
%\pshat{\C} \ar[rr, "F_!"] && \Set\\  
%	 \\
%	\C \ar[uu, hook, "\y"] \ar[rruu, swap,"{F}"] ,&&
% \end{tikzcd}
%\]
%preserves all finite limits (whether or not $\C$ has any).
\end{definition}

Briefly review the classical case of $\alg{R}$-modules and Lazard's theorem.

\subsection{Tensor products of commutative algebras}

Let $\CC$ be a category of (commutative) algebras, such as semilattices, $\bigvee$-lattices, commutative monoids, abelian groups, $\alg{R}$-modules for a commutative ring $\alg{R}$, or frames (called \emph{locales} in \cite{JT}).  The tensor product $\alg{A}\otimes\alg{B}$, when it exists, represents the functor $$\alg{BiHom}_{\alg{A},\alg{B}}: \CC \to\Set$$ of \emph{bihomomorphisms}, which are maps $h : |\alg{A}\times\alg{B}| \to |\alg{C}|$ (in $\Set$) that are homomorphisms in each argument separately.   When it exists, there is a universal bihomomorphism
\[
|\alg{A} \times \alg{B}| \to |\alg{A}\otimes\alg{B}| \,,
\]
precomposing with which gives rise to all others. 

Banaschewski and Nelson \cite{Tensor products and bimorphisms, Canadian Math. Bull. 19(4) (1976).} relate tensor products to the presence of internal $\Hom$-algebras $[\alg{A},\alg{B}]$ consisting of $\T$-algebra homomorphisms, 
\begin{equation*}\label{monoidalclosed}
|[\alg{A},\alg{B}]| = \TAlg(\alg{A},\alg{B})\,,
\end{equation*}
and determine necessary and sufficient conditions for the usual adjunction, 
\begin{equation}\label{monoidalclosed1}
\TAlg\big(\alg{A}\otimes\alg{B},\alg{C}\big) \cong \TAlg\big(\alg{A}, [\alg{B},\alg{C}]\big)\,,
\end{equation}
to obtain a symmetric monoidal closed structure on $\CC$.  

\begin{remark}\label{remark:noCCCwithzero}
Note that when the monoidal product is the cartesian one $\alg{A}\otimes\alg{B} = \alg{A}\times\alg{B}$ an associated closure $[\alg{A},\alg{B}]$ will necessarily be a cartesian closed structure.  Since a non-trivial category with a zero object $0=1$ is never cartesian closed, a monoidal closure $[\alg{A},\alg{B}]$ satisfying \eqref{monoidalclosed1} must have a non-cartesian monoidal product $\alg{A}\otimes\alg{B}$. Several of the examples mentioned above are of this kind,  including $\vee$-semilattices and commutative monoids.
\end{remark}

Let $\CC, \otimes, \I$ be a symmetric monoidal category.  A \emph{commutative $\otimes$-monoid} in $\CC$ is an object $M$ equipped with $m : M \otimes M \to M$ and $u : \I\to M$ satisfying the usual laws for a commutative monoid.
The Elephant C.1.1.8.\ cites (a dual form of) the following result of T.~Fox \cite{Coalgebras and cartesian categories Communications in Algebra 4(7) pp 665--667 1976}.

\begin{proposition}\label{prop:Foxtheorem}
The category $\alg{CMon}(\CC)$ of commutative monoids in $\CC$ has all finite coproducts, and the forgetful functor $\alg{CMon}(\CC) \to\CC$ is the universal monoidal one from a cocartesian monoidal category.  If $\CC$ is closed, the forgetful functor also creates filtered colimits.
\end{proposition}

Here are some examples:
\ednote{Are these correct applications of this?}
\begin{enumerate}
\item $\CC = \Set$ cartesian monoidal, $\alg{cMon}(\CC) = \alg{cMon}$ commutative monoids: the theorem shows that the underlying set of the coproduct $M+N$ is the product $|M|\times |N|$.
\item $\CC = \alg{Mon}$ the cartesian monoidal category of monoids, $\alg{cMon}(\CC) = \alg{cMon}$ commutative monoids, by Eckmann-Hilton: the theorem shows that the underlying monoid of the coproduct of commutative monoids $M+N$ is their product $|M|\times |N|$ as monoids.
\item $\CC = \Set$ cartesian monoidal, $\alg{cMon}(\CC) = \alg{{\vee}SLat}$, the category of $\vee$-semilattices: the theorem shows that the underlying set of the coproduct $M+N$ is the product $|M|\times |N|$.
\item $\CC = \bigvee\!\alg{Lat}$ complete sup-lattices with tensor products $\otimes$ from $\alg{cMon}(\CC) = \alg{Frames}$: the theorem shows that the underlying suplattice of the coproduct of frames $\alg{A}+\alg{B}$ is the tensor product $|\alg{A}|\otimes |\alg{B}|$ of the underlying suplattices.
\item Are there any familiar cases in which this theorem implies that the tensor product $\alg{A}\otimes\alg{B}$ and the coproduct $\alg{A}+\alg{B}$ agree?
\end{enumerate} 

\ednote{But what does this theorem say about $A\otimes B$?  It would be nice to use the preservation of filtered colimits to show $\otimes$-flatness of a flat algebra $\alg{F} = \colim \alg{F(n)}$ as follows: let $\alg{A}\mono\alg{B}$ and try to show $\alg{A}\otimes\alg{F}\mono\alg{B}\otimes\alg{F}$. Since a filtered colimit of monos is monic, it suffices to show it for $\alg{F}=\alg{F(n)}$.  Now show that fgf algebras $\alg{F(n)}$ are $\otimes$-flat, provided $\alg{A}\otimes \alg{F(1)} = \alg{A}$.} 
\bigskip

\ednote{When do we have $\alg{A}\otimes \alg{F(1)} = \alg{A}$ ?  When is $\alg{F(1)} = I$ the unit for the $\otimes$-product? }
\bigskip

\ednote{Other theories to consider: distributive lattices, abelian groups, commutative rings, frames, boolean algebras.}
\bigskip

Bulman-Fleming and  McDowell \cite{BMMD:1979} show that the only $\otimes$-flat distributive lattice is the  trivial one $1$, but they consider distrubutive lattices w/o $0,1$. For the variety of \emph{bounded} distributive lattices, they claim that all of them are flat! It seems that \emph{locality} ($a\vee b = 1$ implies $a=1$ or $b=1$), and its dual, should be true for all $\alg{F(n)}$ and so for all (colimit) flat d-lattices, so maybe this is an example where $\otimes$-flat and flat don't coincide?

\subsection{Semilattices}

The category $\alg{Pos}$ of posets and monotone functions is cartesian closed, with the categorical product $\alg{P}\times\alg{Q}$ as the cartesian monoidal product and the functor category $\alg{Q}^\alg{P} = [\alg{P}, \alg{Q}]$ as the internal $\Hom$.  A $\vee$-semilattice (always with unit) is a idempotent, commutative monoid in $\alg{Pos}$, and the \emph{coproduct} of two such monoids can be seen to again be idempotent and commutative \ednote{proof!}, and so by Proposition \ref{prop:Foxtheorem}, the binary coproduct of $\vee$-semilattices has as its underlying poset the product in $\alg{Pos}$, 
$$|\alg{A}+\alg{B}| = |\alg{A}|\times|\alg{B}|\,,$$
(the underlying set of which is the product of the underlying sets).  

The cartesian monoidal structure of $\alg{Pos}$ creates the same on $\alg{SLat}$, which cannot be closed by Remark \ref{remark:noCCCwithzero}, since $\alg{SLat}$ has a zero object, namely the poset $\mathbbm{1} = \{\emptyset\}$, the free $\vee$-semilattice on $\emptyset$.

There is also a monoidal closed structure on $\alg{SLat}$, with the subposet of all $\alg{SLat}$ homomorphisms as the internal $\Hom$,
\[
[\alg{A}, \alg{B}] =  \alg{SLat}(\alg{A}, \alg{B}) \subseteq \Pos(|\alg{A}|, |\alg{B}|)\,,
\] 
whereby the join of two monotone maps is taken pointwise, $(f\vee g)(a) = f(a)\vee g(a)$ (as is the unit).
It is not hard to see that this internal $\Hom$ for the monoidal closed structure is \emph{not} an exponential for the cartesian closed structure \ednote{(briefly ...)}.  The associated tensor product $\alg{A}\otimes\alg{B}$ satisfying the adjunction
\[
\alg{SLat}\big( \alg{A}\otimes\alg{B}, \alg{C} \big) \cong \alg{SLat}\big( \alg{A}, [\alg{B}, \alg{C}] \big)
\]
is determined by the result of Banaschewsky above to be ...

\bigskip

Next: equivalence theorems for flat semilattices and $\otimes$-flat ones (via Lambek's theorem) and flat/$\otimes$-flat commutative monoids.

\bibliographystyle{alpha}
\bibliography{../references}

%%%
\end{document}
%%%