\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*{regular and exact completions} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{category_theory}{}\paragraph*{{Category theory}}\label{category_theory} [[!include category theory - contents]] \hypertarget{regular_and_exact_completions}{}\section*{{Regular and exact completions}}\label{regular_and_exact_completions} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{constructions}{Constructions}\dotfill \pageref*{constructions} \linebreak \noindent\hyperlink{TheExLexCompletion}{The ex/lex completion}\dotfill \pageref*{TheExLexCompletion} \linebreak \noindent\hyperlink{the_reglex_completion}{The reg/lex completion}\dotfill \pageref*{the_reglex_completion} \linebreak \noindent\hyperlink{the_exreg_completion}{The ex/reg completion}\dotfill \pageref*{the_exreg_completion} \linebreak \noindent\hyperlink{the_higher_categorical_approach}{The higher categorical approach}\dotfill \pageref*{the_higher_categorical_approach} \linebreak \noindent\hyperlink{completions_of_unary_sites}{Completions of unary sites}\dotfill \pageref*{completions_of_unary_sites} \linebreak \noindent\hyperlink{generalizations_to_higher_arity}{Generalizations to higher arity}\dotfill \pageref*{generalizations_to_higher_arity} \linebreak \noindent\hyperlink{properties_of_regular_and_exact_completions}{Properties of regular and exact completions}\dotfill \pageref*{properties_of_regular_and_exact_completions} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} The [[forgetful functor|forgetful]] [[2-functors]] \begin{itemize}% \item from [[regular categories]] to [[lex categories]], \item from [[exact categories]] to [[lex categories]], and \item from [[exact categories]] to [[regular categories]] \end{itemize} have [[left adjoints]], and in fact are [[monadic adjunction|(2-)monadic]]. Their left adjoints are called ([[free construction|free]]) regular or exact completions. In the third case the [[2-monad]] is [[idempotent monad|idempotent]], so the left adjoint can properly be called a [[completion]], while in the first two cases, the 2-monad is only [[lax-idempotent monad|lax-idempotent]], so the left adjoint should technically be called a [[free completion]]. However, the phrases \emph{regular completion} and \emph{exact completion} are also commonly used for the first two cases. To disambiguate the second and third cases the phrases \emph{ex/lex completion} and \emph{ex/reg completion} are also used, and so by analogy the first case is called \emph{reg/lex completion}. In fact, the reg/lex and ex/lex completion can be applied to a category that merely has [[weak finite limits]], although in this case they are not left adjoint to the obvious forgetful functor. A general context which includes \emph{all} of these types of these completions is the 2-category of [[unary sites]], in which the categories of regular and exact categories form reflective sub-2-categories. \hypertarget{constructions}{}\subsection*{{Constructions}}\label{constructions} \hypertarget{TheExLexCompletion}{}\subsubsection*{{The ex/lex completion}}\label{TheExLexCompletion} There are several constructions of the ex/lex completion. Perhaps the quickest one to state (Hu-Tholen 1996) is that if $C$ is [[small category|small]], then $C_{ex/lex}$ is the full subcategory of its [[presheaf category]] $Set^{C^{op}}$ spanned by those presheaves $F$ such that \begin{itemize}% \item $F$ admits a [[regular epimorphism]] $y(X)\twoheadrightarrow F$ from a [[representable presheaf]], \item with the additional property that if $K\rightrightarrows y(X)$ is the [[kernel pair]] of $y(X)\twoheadrightarrow F$, then $K$ also admits a regular epi $y(Z)\to K$ from a representable presheaf. \end{itemize} A more explicit construction is as follows. Let us think, informally, of the objects of $C$ as [[presets]] and the morphisms of $C$ as ``proofs''. An object of $C_{ex} = C_{ex/lex}$ will then be a ``set'' or [[setoid]] constructed from $C$. Precisely, we take the objects of $C_{ex}$ to be the \textbf{pseudo-equivalence relations} in $C$: a pseudo-equivalence relation consists of: \begin{itemize}% \item an object $X\in C$ and \item a parallel pair $s,t\colon R\rightrightarrows X$, such that \item there exists an arrow $i\colon X\to R$ with $s i = t i = 1_X$, \item there exists an arrow $v\colon R\to R$ with $s v = t$ and $t v = s$, and \item there exists an arrow $c\colon R\times_X R \to R$ with $s c = s \pi_1$ and $t c = t \pi_2$. (If $C$ has merely weak finite limits, we assert this for some, and hence every, weak pullback $R\times^w_X R$.) \end{itemize} If $(s,t)\colon R\to X\times X$ is a [[monomorphism]], then these conditions make it precisely a [[congruence]] or internal [[equivalence relation]] in $C$. In general, we can think of the fiber of $R$ over $(x_1,x_2)$ as giving a collection of ``reasons'' or ``proofs'' that $x_1 \mathrel{R} x_2$. Then $i$ supplies a uniform proof that $x \mathrel{R} x$ for every $x$, while $v$ supplies a uniform proof that $x \mathrel{R} y$ implies $y \mathrel{R} x$, and $c$ supplies a uniform proof that $x \mathrel{R} y$ and $y \mathrel{R} z$ imply $x \mathrel{R} z$. If $R\rightrightarrows X$ and $S\rightrightarrows Y$ are two pseudo-equivalence relations, a morphism between them in $C_{ex}$ is defined to be a morphism $f\colon X\to Y$ in $C$, such that there exists a morphism $f_1\colon R\to S$ with $s f_1 = f s$ and $t f_1 = f t$. That is, $f_1$ supplies a uniform proof that if $x \mathrel{R} y$ then $f(x) \mathrel{S} f(y)$. Moreover, we declare two such morphisms $f,g\colon X\to Y$ to be \emph{equal} if there exists a morphism $h\colon X\to S$ such that $s h = f$ and $t h = g$ (that is, a uniform proof that $f(x) \mathrel{S} g(x)$). Because $S\rightrightarrows Y$ is a pseudo-equivalence relation, this defines an actual equivalence relation on the morphisms $f\colon X\to Y$, which is compatible with composition; thus we have a well-defined category $C_{ex}$. We have a [[full and faithful functor]] $C\to C_{ex}$ sending an object $X$ to the pseudo-equivalence relation $X\rightrightarrows X$. One can then verify directly that $C_{ex}$ is exact, that this embedding preserves finite limits, and that it is universal with respect to lex functors from $C$ into exact categories. There are also other constructions. Of course, the ex/lex completion can also be obtained by composing (any construction of) the reg/lex completion with (any construction of) the ex/reg completion. \hypertarget{the_reglex_completion}{}\subsubsection*{{The reg/lex completion}}\label{the_reglex_completion} The reg/lex completion $C_{reg}= C_{reg/lex}$ of a lex category $C$ is perhaps most succinctly described as the subcategory of $C_{ex}$ consisting of those objects which admit monomorphisms into objects of $C$. That is, instead of adding \emph{all} quotients of pseudo-equivalence relations in $C$, we only add those quotients which are necessary in order to be able to construct [[images]] of morphisms in $C$. For many construction of $C_{ex}$, this idea can then be made more explicit and sometimes simplified. For instance, if we regard $C_{ex}$ as a full subcategory of $Set^{C^{op}}$ as above, then we can likewise regard $C_{reg}$ as the full subcategory of $Set^{C^{op}}$ determined by those presheaves $F$ such that \begin{itemize}% \item $F$ admits a regular epimorphism $y(X) \twoheadrightarrow F$ from a representable presheaf, and \item $F$ admits a monomorphism $F\rightarrowtail y(Z)$ into a representable presheaf. \end{itemize} If we construct $C_{ex}$ using pseudo-equivalence relations, as above, then we can characterize the pseudo-equivalence relations which we need to form $C_{reg}$ as precisely the [[kernel pairs]] of morphisms of $C$ (or finite families of such). Therefore, we obtain an equivalent definition of $C_{reg}$ as follows. Its objects are morphisms of $C$ (regarded as stand-ins for their formally added images). A morphism from $p\colon X\to Y$ to $q\colon Z\to W$ should be a morphism $f\colon X\to Z$ for which there exists an $f_1$ relating the kernel of $p$ to the kernel of $q$, modulo an equivalence relation generated by maps from $X$ to the kernel of $q$. But by definition of kernel pairs, two morphisms will be identified under this latter equivalence relation if and only if they have the same composite with $q$, so it makes sense to define the morphisms of $C_{reg}$ from $p\colon X\to Y$ to $q\colon Z\to W$ to be certain morphisms $\overline{f}\colon X\to W$ which factor through $q$ (non-uniquely). We still have to impose the condition that $f$ should preserve the kernel pairs, but in terms of $\overline{f}$ this is simply the statement that $\overline{f} r = \overline{f} s$, where $(r,s)$ is the kernel pair of $p$. This is the definition of $C_{reg}$ given in the [[Elephant]]. We can then verify that $C_{reg}$ is regular, that we have a full and faithful functor $C\to C_{reg}$, which preserves finite limits, and is universal among lex functors from $C$ to regular categories. Again, there are also other constructions. Also, just as for the free exact completion, the construction works essentially the same if $C$ has only weak finite limits. In this case, instead of the objects of $C_{ex}$ admitting a monomorphism to a single object of $C$, we have to consider those admitting a jointly-monic finite family of morphisms into objects of $C$, with similar modifications for the other descriptions. \hypertarget{the_exreg_completion}{}\subsubsection*{{The ex/reg completion}}\label{the_exreg_completion} If $C$ is regular, a quick definition of $C_{ex/reg}$ is as the full subcategory of the category $Sh(C)$ of [[sheaves]] for the [[regular coverage]] on $C$ spanned by those sheaves which are quotients of [[congruences]] in $C$. (Lack 1999) A more explicit description can be obtained by first passing from $C$ to its [[allegory]] of internal relations, then [[split idempotent|splitting]] the idempotents which are equivalence relations in $C$, and finally reconstructing a regular category from the resulting allegory. Yet more explicitly, this means that the objects of $C_{ex/reg}$ are congruences in $C$, and the morphisms are relations which are [[entire relation|entire]] and [[functional relation|functional]] relative to the given congruences. \hypertarget{the_higher_categorical_approach}{}\subsubsection*{{The higher categorical approach}}\label{the_higher_categorical_approach} A somewhat more unified approach to all these completions can be obtained as follows. Observe that in the classical situation (that is, in the presence of choice), \emph{sets} can be identified with all of the following: \begin{itemize}% \item 0-trivial [[groupoids]], i.e. groupoids in which any two parallel morphisms are equal, i.e. [[equivalence relations]]. \item 0-trivial [[2-groupoids]], i.e. 2-groupoids in which any two parallel 2-morphisms are equal and any two parallel 1-morphisms are isomorphic. \item and so on\ldots{} \item 0-trivial [[n-groupoids]] for any $0\le n \le \infty$. \end{itemize} In the absence of choice, this is still true as long as the morphisms between 0-trivial n-groupoids are $n$-[[anafunctors]]. If instead we consider only actual functors, however, in the absence of choice what we obtain are various completions of $Set$. Specifically: \begin{itemize}% \item $Set_{reg/lex}$ can be identified with the category whose objects are 0-trivial groupoids, and whose morphisms are natural isomorphism classes of functors. \item $Set_{ex/lex}$ can be identified with the category whose objects are 0-trivial 2-groupoids, and whose morphisms are pseudonatural equivalence classes of 2-functors. In the notion of 2-groupoid here we also demand that each 1-cell be equipped with a \emph{specified} inverse [[equivalence]]. \end{itemize} This idea can be generalized to provide alternate constructions of the completions for an arbitrary $C$ with finite limits. The notions of [[internal category|internal]] $n$-category and internal $n$-functor in such a $C$ make perfect sense for any $n$. The same is true of the notion of $n$-groupoid, as long as we interpret this to mean the \emph{structure} of ``inverse-assigning'' morphisms in $C$. The statement ``any two parallel $n$-cells are equal'' also makes sense in any lex category, since it demands that a certain specified morphism is monic. Finally, we can also interpret ``any two parallel $k$-cells are equivalent'' algebraically by specifying a particular equivalence between any such pair. (Note that for $k=(n-1)$, since parallel $n$-cells are equal there is a unique way to do this.) We thereby obtain a notion of internal 0-trivial $n$-groupoid in any lex category, and we write $0 triv n Gpd(C)$ for the category of such things and internal $n$-natural equivalence classes of functors. We then have: \begin{itemize}% \item It is fairly clear from the above explicit description that $C_{reg/lex}$ is the full subcategory of $0 triv 1 Gpd(C)$ determined by the [[kernel pairs]] (which are [[congruences]], i.e. internal 0-trivial 1-groupoids). If, like $Set$, $C$ is already exact, so that every congruence is a kernel pair, then $C_{reg/lex}\simeq 0 triv 1 Gpd(C)$. \item $C_{ex/lex}$ is always equivalent to $0 triv 2 Gpd(C)$. To see this, note that a pseudo-equivalence relation (together with chosen maps $i$, $c$, and $v$) can be regarded as the 1-skeleton of an internal [[bicategory]] in $C$ with specified inverse equivalences for every 1-cell. There is then a unique way to add 2-cells to make it a 0-trivial bigroupoid. \end{itemize} It is not clear how 0-trivial $n$-groupoids fit into this picture for $n\gt 2$, although it seems likely that the objects of \emph{iterated} reg/lex and ex/lex completions can be identified with some type of internal [[n-fold category]]. Now if $C$ is already regular, then we can define a notion of internal [[anafunctor]] between internal $n$-categories. It is then easily seen that \begin{itemize}% \item $C_{ex/reg}$ is equivalent to the category of 0-trivial 1-groupoids, and natural isomorphism classes of internal anafunctors between them. \end{itemize} Again, it is not entirely clear how the 0-trivial $n$-groupoids and anafunctors behave for $n\gt 1$, although it seems fairly likely (to [[Mike Shulman|me]]) that in this case the process will stabilize at $n=1$, i.e. 0-trivial $n$-groupoids with equivalence classes of ana-$n$-functors will give $C_{ex/reg}$ for all $n\ge 1$. \hypertarget{completions_of_unary_sites}{}\subsubsection*{{Completions of unary sites}}\label{completions_of_unary_sites} The descriptions of the ex/lex and ex/reg completions in terms of pseudo-equivalence relations and equivalence relations, respectively, have a common generalization. Let $C$ be a [[unary site]], so that it has a notion of ``covering morphism'' and admits ``finite local unary prelimits''. In particular, any cospan $X\to Z\leftarrow Y$ has a \emph{local unary pre-pullback}, which is a commutative square \begin{displaymath} \itexarray{ P & \to & Y \\ \downarrow && \downarrow\\ X & \to & Z } \end{displaymath} such that for any other commutative square \begin{displaymath} \itexarray{ V & \to & Y \\ \downarrow && \downarrow\\ X & \to & Z } \end{displaymath} there is a cover $U\to V$ and a map $U\to P$ such that the induced composites $U\to X$ and $U\to Y$ are equal. Now we can define a \textbf{unary congruence} in $C$ to consist of: \begin{itemize}% \item An object $X\in C$ \item A parallel pair $s,t:R\toto X$, such that \item There exists a cover $p:Y\to X$ and a map $i:Y\to R$ with $s i = t i = p$, \item There exists a cover $q:S\to R$ and a map $v:S\to R$ with $s v = t q$ and $t v = s q$, and \item There exists a local unary pre-pullback $T$ of the cospan $R \xrightarrow{t} X \xleftarrow{s} R$ and an arrow $c:T\to R$ such that $s c = s \pi_1$ and $t c = t \pi_2$, where $\pi_1$ and $\pi_2$ are the projections of $T$ to $R$. \end{itemize} If $C$ has a trivial topology, then local unary prelimits are simply weak limits, and this reduces to the definition of pseudo-equivalence relation. On the other hand, if $C$ is regular with its regular topology, then these conditions ensure exactly that the [[image]] of $R\to X\times X$ is an internal equivalence relation on $X$. Now we can define morphisms between unary congruences using a suitable kind of either entire and functional relations or anafunctors, and obtain the exact completion of the unary site $C$. This construction exhibits the 2-category of exact categories as a reflective sub-2-category of the 2-category of unary sites, and restricts to the ex/wlex and ex/reg completions on the sub-2-categories of categories with weak finite limits and trivial topologies and of regular categories with regular topologies, respectively. It can also be modified to construct regular completions. See (\hyperlink{Shulman}{Shulman}) for details. \hypertarget{generalizations_to_higher_arity}{}\subsection*{{Generalizations to higher arity}}\label{generalizations_to_higher_arity} More generally, any [[∞-ary site]] has a $\kappa$-ary exact completion, which is a [[∞-ary exact category]]. This exhibits the 2-category of $\kappa$-ary exact categories as a reflective sub-2-category of that of $\kappa$-ary sites. See (\hyperlink{Shulman}{Shulman}) for details. In particular: \begin{itemize}% \item When $\kappa=\omega$, this is called the [[pretopos completion]], and applies in particular to [[coherent categories]]. \item When $\kappa$ is the size of the [[universe]], this applies to any [[small category|small]] [[site]] and constructs its [[topos of sheaves]]. \end{itemize} \hypertarget{properties_of_regular_and_exact_completions}{}\subsection*{{Properties of regular and exact completions}}\label{properties_of_regular_and_exact_completions} Many categorical properties of interest are preserved by one or more of the regular and exact completions. That is, if $C$ has these properties, then so does the completion, and the inclusion functor preserves them. Note that frequently, for a completion to have some structure, it suffices for $C$ to have a ``weak'' version of that structure. \begin{itemize}% \item Of course, [[finite limits]] are preserved by all three completions. In fact, as we have remarked, for the ex/lex and reg/lex completions, $C$ need only have weak finite limits. \item $C$ is [[extensive category|lextensive]] if and only if $C_{ex/lex}$ is, and if and only if $C_{reg/lex}$ is, and in this case the embeddings preserve [[coproducts]] (Menni 2000). It follows that if $C$ is a [[pretopos]], then so is $C_{ex/lex}$, although the inclusion $C\to C_{ex/lex}$ is not a ``pretopos functor'' as it does not preserve [[regular epis]]. \item If $C$ is lextensive and has [[coequalizers]] (and hence has finite colimits), then so do $C_{ex/lex}$ and $C_{reg/lex}$ (Menni 2000). However, the inclusion functors do not preserve coequalizers. In fact, it suffices for $C$ to be lextensive with \emph{quasi-coequalizers}, meaning that for every $f,g\colon Y\rightrightarrows X$ there exists $q\colon X\to Q$ with $q f = q g$, such that for any $h\colon X\to Z$ with $h f = h g$, $h$ coequalizes the [[kernel pair]] of $q$. \item The categories $C_{reg/lex}$ and $C_{ex/lex}$ always have [[projective object|enough (regular) projectives]]. In fact, the objects of $C$ are precisely the projective objects of these categories. Moreover, an exact category $D$ is of the form $C_{ex/lex}$ for some $C$ (with weak finite limits) if and only if it has enough projectives, in which case of course $C$ can be taken to be the subcategory of projectives (Carboni--Vitale 1998). Note that if $D$ has enough projectives, then its subcategory of projectives always has weak finite limits. Similarly, a regular category $D$ is of the form $C_{reg/lex}$ for some $C$ (with weak finite limits) if and only if it has enough projectives and every object can be embedded in a projective one. \item If $C$ is a regular category satisfying the ``regular'' [[axiom of choice]] (i.e. every regular epi splits), then it is \emph{equivalent} to $C_{reg/lex}$, and hence the latter also satisfies the axiom of choice. Similarly, if $C$ is exact and satisfies choice, then it is equivalent to $C_{ex/lex}$. Conversely, if the inclusion $C\to C_{reg/lex}$ or $C\to C_{ex/lex}$ is an equivalence, then since the objects of $C$ are projective in these completions, $C$ must satisfy the axiom of choice. In fact, if we assume merely that $C_{ex/lex} \to (C_{ex/lex})_{ex/lex}$ is a equivalence, then since the objects of $C_{ex/lex}$ are projective in $(C_{ex/lex})_{ex/lex}$, they must also all be projective in $C_{ex/lex}$, and therefore $C\to C_{ex/lex}$ is also an equivalence. It follows by induction that if the sequence of iterations of $(-)_{ex/lex}$ stabilizes at any finite stage, it must in fact stabilize at the very beginning and $C$ must satisfy the axiom of choice. A similar argument applies to the reg/lex completion. (The ex/reg completion, of course, always stabilizes after one application.) \item [[cartesian closed category|Cartesian closure]] is preserved by the ex/lex completion (Carboni--Rosolini 2000). In fact, $C_{ex/lex}$ is cartesian closed if and only if $C$ has \emph{weak simple products}, meaning [[weak dependent product]]s along [[product]] projections. \item [[locally cartesian closed category|Local cartesian closure]] is also preserved by the ex/lex completion (Carboni--Rosolini 2000). In fact, $C_{ex/lex}$ is locally cartesian closed if and only if $C$ is \emph{weakly locally cartesian closed}, meaning that each [[slice category]] has weak dependent products. It follows in particular that if $C$ is a [[Π-pretopos]], then so is $C_{ex/lex}$. For each $\Pi$-pretopos $C$ we thus obtain a sequence $C$, $C_{ex}$, $(C_{ex})_{ex}$, \ldots{} of $\Pi$-pretopoi, which in general does not stabilize. \item (Local) cartesian closure is seemingly not always preserved by the reg/lex completion, but it is under certain hypotheses. Recalling that $C_{reg/lex}$ is the full subcategory of $C_{ex/lex}$ consisting of the kernel pairs, suppose that $C$ has pullback-stable (epi,regular mono) factorizations and that every [[regular monomorphism|regular]] congruence is a kernel pair. Then $C_{reg/lex}$ is [[reflective subcategory|reflective]] in $C_{ex/lex}$ (BCRS 1998, Menni 2000): the reflection of a pseudo-equivalence relation $R\rightrightarrows X$ is its (epi,regular mono) factorization. Moreover, the reflection preserves products, and also pullbacks along maps in $C_{reg/lex}$, from which it follows that if $C_{ex/lex}$ is cartesian closed or locally cartesian closed, so is $C_{reg/lex}$. Thus, if $C$ is weakly cartesian closed (resp. weakly locally cartesian closed), has pullback-stable (epi,regular mono) factorizations, and every regular congruence is a kernel pair, then $C_{reg/lex}$ is cartesian closed (resp. locally cartesian closed). In particular, the local versions of these hypotheses apply in particular to [[Top]] and to any [[quasitopos]]. Note that $Top_{reg/lex}$ is called the category of [[equilogical space]]s. \item If $C$ is lextensive with coequalizers (or ``quasi-coequalizers'') and a [[strong-subobject classifier]], then so is $C_{reg/lex}$ (Menni 2000). It follows that if $C$ is a lextensive [[quasitopos]], then so is $C_{reg/lex}$. For each lextensive quasitopos $C$ we thus obtain a sequence $C$, $C_{reg}$, $(C_{reg})_{reg}$, \ldots{} of lextensive quasitopoi, which in general does not stabilize. \item If $C$ has a [[natural numbers object]], then so do $C_{reg/lex}$ and $C_{ex/lex}$. (Does $C_{ex/reg}$? What about more general [[W-type]]s?) \item If $C$ is a [[ΠW-pretopos]], then so is $C_{ex/lex}$ (see \hyperlink{vdB}{vandenBerg}, Theorem 1.1). \item $C_{ex/lex}$ is an [[elementary topos]] iff $C$ has weak dependent products and a [[generic proof]] (\hyperlink{Menni}{Menni2000}). Note that if $C$ is a topos satisfying the axiom of choice, then its subobject classifier is a generic proof. It follows that in this case $C_{ex/lex}$ is a topos---but we already knew that, because $C_{ex/lex}$ is equivalent to $C$ for such a $C$. \item Expanding on the last point, for a [[presheaf topos]] $C = Set^{D^{op}}$, the category $C_{ex/lex}$ is a topos iff $D$ is a [[groupoid]] (\hyperlink{Menni}{Menni2000}). \item If $C$ is regular, locally cartesian closed, and has a \emph{generic mono}, i.e. a monomorphism $\tau\colon \Upsilon\to \Lambda$ such that every monomorphism is a pullback of $\tau$ (not necessarily uniquely), then $C_{ex/reg}$ is a topos (\hyperlink{Menni}{Menni2000}). \item If $C$ is an [[additive category]], then $C_{ex/lex}$ is an [[abelian category]]. \end{itemize} On the other hand, some properties are \emph{not} preserved by the completions. \begin{itemize}% \item Of course, all the completions are regular categories, but the inclusions are not [[regular functor]]s, since they do not preserve regular epis. \item We have seen that the existence of a [[subobject classifier]] or [[power objects]] is not, in general, preserved by the completions (although if $C$ is a topos, then of course so is $C_{ex/reg}$, since it is equivalent to $C$). \item Similarly, if $C$ is [[well-powered category|well-powered]], it does not follow that $C_{reg/lex}$ or $C_{ex/lex}$ are. In particular, for $X\in C$, the subobject preorders $Sub_{C_{reg/lex}}(X)$ and $Sub_{C_{ex/lex}}(X)$ are equivalent to the preorder reflection of the slice category $C/X$, and it is easy to construct examples in which this is not essentially small\footnote{For example, let $C = Set^{\bullet \rightrightarrows \bullet}$ be the topos of [[quiver|directed graphs]]. For each ordinal $\alpha$, let $G_\alpha$ be the directed graph whose nodes are elements of $\alpha$ and with a directed edge from $\beta$ to $\gamma$ if $\beta \lt \gamma$ in $\alpha$. Then in the poset reflection $Pos(C)$, we have a class of proper monomorphisms, e.g., $[G_\alpha] \lt [G_{\alpha'}]$ whenever $\alpha \lt \alpha'$. Thus $Pos(C)$ is a large poset. This example also shows that $Pos(C)$ need not be a [[total category]] even if $C$ is.} . \item If $C$ is a [[coherent category]], it does not follow that $C_{ex/lex}$ or $C_{reg/lex}$ is. However, if $C$ is additionally [[extensive category|lextensive]], we have seen above that so are these completions, and hence in particular also coherent (any extensive regular category is coherent). One can also write down the ``free coherent completion'' and the ``free pretopos completion'' of a lex category, and the ``pretopos completion'' of a coherent category; see [[familial regularity and exactness]] for some clues on how to proceed. \item If $C$ is a [[Heyting category]], it does not follow that $C_{ex/lex}$ or $C_{reg/lex}$ is. However, if $C$ is additionally lextensive and locally cartesian closed, we have seen above that so are these completions, and hence Heyting (any lextensive locally cartesian closed regular category is Heyting). \item Unsurprisingly, if $C$ is a [[Boolean category]], it does not follow that $C_{ex/lex}$ or $C_{reg/lex}$ is, even if $C$ is lextensive and LCC so that its completions are Heyting. In fact, a stronger statement is true: if $C$ is lextensive and regular, then $C_{reg/lex}$ and $C_{ex/lex}$ are Boolean if and only if $C$ \emph{satisfies the axiom of choice} (in which case they are of course equivalent to $C$). More precisely, if $X\in C$ is such that every subobject of $X$ in $C_{reg/lex}$ is complemented, then $X$ is projective in $C$. (The same argument applies to $C_{ex/lex}$.) For suppose that $p\colon Y\to X$ is a regular epi in $C$. Recall that $Sub_{C_{reg/lex}}(X)$ is the preorder reflection of $C/X$. Thus $p$, considered as an object of $C/X$, defines a monomorphism in $C_{reg/lex}$. By assumption, this monic is complemented; let its complement be represented by $q\colon Z\to X$. Since complements are disjoint, and meets in $Sub_{C_{reg/lex}}(X)$ are given by pullbacks in $C/X$, the pullback of $p$ and $q$ admits a morphism to the initial object $0$, and hence is itself initial since $C$ is extensive. Now $p$ is regular epi, hence so is its pullback $0\to Z$. But in a lextensive regular category, disjointness of the coproduct $1+1$ implies that $0\to 1$ is the equalizer of of the coprojections $1\rightrightarrows 1+1$, and therefore any epimorphism with domain $0$ is an isomorphism; thus $Z$ is also initial. Now since joins in $Sub_{C_{reg/lex}}(X)$ are given by coproducts in $C/X$, the induced map $Y+Z \to X$ must become an isomorphism in $Sub_{C_{reg/lex}}(X)$, which means that it must admit a section; but since $Z$ is initial this means that $p$ itself has a section. \item If $C$ is [[well-pointed topos|well-pointed]], it does not follow that $C_{ex/lex}$ or $C_{reg/lex}$ are (in the stronger sense appropriate for non-toposes). It is of course always true that $1$ is projective in the completions. And if $C$ is lextensive, so that its completions are coherent, then $1$ is indecomposable in them as soon as it is so in $C$. However, it does not follow that $1$ is a \emph{strong} generator in the completions even if it is so in $C$, since the completions have (in general) many more monomorphisms than $C$ does. If $C$ is a well-pointed topos such that $C_{ex/lex}$ is also a topos, then the latter cannot be well-pointed unless $C$ satisfies AC, because the completion would then be Boolean, and hence AC holds by the proof above. \end{itemize} \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} (to be written\ldots{}) \begin{itemize}% \item [[Realizability toposes]] arise as ex/lex completions of categories of partitioned assemblies based on a [[partial combinatory algebra]] $A$. In fact the reg/lex completion gives, as an interesting intermediate step, the category of assemblies based on $A$ (which turns out to be the [[quasitopos]] of $\neg\neg$-separated objects inside the realizability topos). This is discussed in \hyperlink{Menni}{Menni}. \item The category $TF$ of [[torsion|torsion-free]] [[abelian groups]] is regular, but not exact. For instance, the [[congruence]] $\{ (a,b) | a \equiv b \mod 2 \} \subseteq \mathbb{Z}\times\mathbb{Z}$ is not a kernel in $TF$. Unsurprisingly, the ex/reg completion of $TF$ is equivalent to the category $Ab$ of all abelian groups. Note that although $TF$ is not exact, its inclusion into $Ab$ does have a left adjoint (quotient by torsion), and thus $TF$ is cocomplete. Herein lies a subtle trap for the unwary: since the ex/reg completion monad is idempotent, it is in particular lax-idempotent, which means that any left adjoint to the unit $C \hookrightarrow C_{ex/reg}$ is in fact a (pseudo) algebra structure; but since the monad is actually idempotent, any algebra structure is an equivalence. Of course, the reflection $Ab \to TF$ is \emph{not} an equivalence, which doesn't contract the general facts because this left adjoint is not a regular functor, and hence not an adjunction in the 2-category on which the monad $(-)_{ex/reg}$ lives. In fact, it is not hard to check that $C \hookrightarrow C_{ex/reg}$ has a left adjoint in $Cat$ if and only if $C$ has [[coequalizers]] of [[congruences]] (while if it has a left adjoint in $Reg$ then it must be an equivalence). \item A [[free cocompletion]] of a (possibly large) finitely complete category, i.e., the category of [[small presheaves]] on $C$, is the ex/lex completion of the [[free cartesian category|free coproduct completion]] of $C$. This appears as Lemma 3 \hyperlink{JR}{here}. \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item Carboni and Celia Magno, ``The free exact category on a left exact one'', J. Austral. Math. Soc. (Ser. A), 1982. \item Ji\'i{} Rosick\'y{}, \emph{Cartesian closed exact completions}, JPAA 142 no. 3 (October 1999), 261-270. (\href{http://www.sciencedirect.com/science/journal/00224049/142/3}{web}) \end{itemize} \begin{itemize}% \item Hu and Tholen, ``A note on free regular and exact completions and their infinitary generalizations'', \href{http://www.tac.mta.ca/tac/volumes/1996/n10/2-10abs.html}{TAC} 1996. \item Carboni and Vitale, ``Regular and exact completions'', JPAA 1998. \item Birkedal and Carboni and Rosolini and Scott, ``Type Theory via Exact Categories,'' 1998 \item Stephen Lack, ``A note on the exact completion of a regular category, and its infinitary generalizations'' \href{http://www.tac.mta.ca/tac/volumes/1999/n3/5-03abs.html}{TAC} 1999. \item The [[Elephant]], Sections A1.3 and A3. \item Carboni and Rosolini, ``Locally cartesian closed exact completions'', JPAA 2000 \item Mat\'i{}as Menni, ``Exact completions and toposes,'' Ph.D. Thesis, University of Edinburgh, 2000. (\href{http://www.lfcs.inf.ed.ac.uk/reports/00/ECS-LFCS-00-424/}{web}) \end{itemize} \begin{itemize}% \item [[Michael Shulman]], ``Exact completions and small sheaves''. \emph{Theory and Applications of Categories}, Vol. 27, 2012, No. 7, pp 97-173. \href{http://www.tac.mta.ca/tac/volumes/27/7/27-07abs.html}{Free online} \end{itemize} \begin{itemize}% \item [[Benno van den Berg]], \emph{Inductive types and exact completion}, Ann. Pure Appl. Logic, 134 (2005), 95--121. (\href{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.18.5456&rep=rep1&type=pdf}{online .pdf file}) \end{itemize} [[!redirects regular or exact completion]] [[!redirects regular and exact completion]] [[!redirects exact completion]] [[!redirects lex completion]] [[!redirects free exact completion]] [[!redirects ex/lex completion]] [[!redirects ex/reg completion]] [[!redirects reg/lex completion]] [[!redirects regular or exact completions]] [[!redirects regular and exact completions]] [[!redirects exact completions]] [[!redirects lex completions]] [[!redirects ex/lex completions]] [[!redirects ex/reg completions]] [[!redirects reg/lex completions]] \end{document}