\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*{sheafification}

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

\hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory}

[[!include topos theory - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{existence}{Existence}\dotfill \pageref*{existence} \linebreak
\noindent\hyperlink{construction}{Construction}\dotfill \pageref*{construction} \linebreak
\noindent\hyperlink{for_sheaves_with_values_in_categories_other_than_}{For sheaves with values in categories other than $Set$}\dotfill \pageref*{for_sheaves_with_values_in_categories_other_than_} \linebreak
\noindent\hyperlink{with_values_in_models_for_finitelimit_theories}{With values in models for finite-limit theories}\dotfill \pageref*{with_values_in_models_for_finitelimit_theories} \linebreak
\noindent\hyperlink{using_the_ipcproperty}{Using the IPC-property}\dotfill \pageref*{using_the_ipcproperty} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

Given a [[site]] $C$, the \emph{sheafification} [[functor]] universally turns [[presheaves]] on $C$ into [[sheaves]].

It is characterized as being the [[left adjoint|left]] [[adjoint functor]] $L : PSh(C) \to Sh(C)$ to the inclusion $Sh(C) \hookrightarrow PSh(C)$ of sheaves into all presheaves, exhibiting this as a [[reflective subcategory]].

Therefore sheafification is a special case of a very general phenonemon of [[localization]]s of categories. See [[category of sheaves]] for more.

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

Let $(C,J)$ be a [[site]] in the sense of: [[small category]] equipped with a [[coverage]]. Write $PSh(C)$ for the [[category of presheaves]] on $C$ and

\begin{displaymath}
j : C \to PSh(C)
\end{displaymath}
for the [[Yoneda embedding]]. Write

\begin{displaymath}
i :  Sh_J(C) \hookrightarrow PSh(C)
\end{displaymath}
for the [[category of sheaves]]: the [[full subcategory]] on those presheaves that are $J$-[[sheaves]].

\hypertarget{existence}{}\subsubsection*{{Existence}}\label{existence}

\begin{prop}
\label{ExistenceOfLeftAdjoint}\hypertarget{ExistenceOfLeftAdjoint}{}
The inclusion of sheaves into presheaves admits a [[left adjoint|left]] [[adjoint functor]], which hence exhibits $Sh(C)$ as a [[reflective subcategory]] or reflective [[localization]] of $PSh(C)$:

\begin{displaymath}
(L \dashv i) : Sh_J(C) \stackrel{\overset{L}{\leftarrow}}{\hookrightarrow}
   PSh(C)
  \,.
\end{displaymath}
\end{prop}
\begin{proof}
This follows by general properties discussed at [[reflective subcategory]]. We spell out the argument using the theory of [[localization]] at a set of morphisms satisfying a [[calculus of fractions]].

Recall from the discussion at [[sheaf]] that $Sh_J(C)$ is by definition the [[full subcategory]] of $PSh(C)$ on the [[local object]]s with respect to the morphisms

\begin{displaymath}
W = 
  \left\{
  S(\{U_i\}) := \lim_\to\left( 
    \coprod_{i,j} j(U_i) \times_{j(U)} j(U_j) \stackrel{\to}{\to} \coprod_i j(U_i) \right) \to j(U)
   |
   \;\;
  \{U_i \to U\}_{i \in I} \in J
  \right\}
\end{displaymath}
of [[sieve]] inclusions for all [[covering]] families of the [[coverage]] $J$. (Here the [[colimit]] $\lim_\to$ is the [[coequalizer]] of the two injection maps, as indicated. This is spelled out in more detail at [[sheaf]] and at [[sieve]].)

Now we invoke the following results:

\begin{enumerate}%
\item The  says that every [[full subcategory]] of a [[locally presentable category]] on the $W$-[[local object]]s for a [[small set]] $W$ of morphisms is a [[reflective subcategory]], given by the [[localization]] at these morphisms;


\item By  every reflective subcategory is the [[localization]] at the collection of morphisms inverted by the left adjoint (which by the localization proposition is the saturation of the original set of morphisms).


\item If $W$ satisfies the axioms of a [[calculus of fractions]] then, by the discussion there, this localization is equivalently given by the category $PSh(C)[W^{-1}]$ whose objects are those of $PSh(C)$ and whose morphisms are given by $PSh(C)[W^{-1}](X,A) \simeq {\lim_{\to}}_{\hat X  \stackrel{w \in W}{\to} X} PSh_C(\hat X,A)$.



\end{enumerate}
Notice that an object is a [[local object]] with respect to the above set of morphisms $W$ precisely if it is local with respect to the set of all [[small set|small]] [[colimit]]s (in the [[arrow category]] $Arr(PSh(C))$ ) of such morphims (since the [[hom-functor]] $PSh_C(-,A)$ sends colimits in the first argument to [[limit]]s, and a limit of [[isomorphism]]s is an isomorphism).

Let hence $\bar W$ be the completion of $A$ under forming small colimits in $Arr(PSh(C))$.

We claim that the morphisms in $\bar W$ form a [[calculus of fractions]]. The first condition to check is that for all morphisms of presheaves $X \to j(U)$ and every covering family $\{U_i \to U\}$ there is a morphism $Y \to X$ in $\bar W$ and a [[commuting diagram]]

\begin{displaymath}
\itexarray{
    Y &\to& S(\{U_i\})
    \\
    \downarrow && \downarrow^{\mathrlap{s}}
    \\
    X &\to& j(U)
  }
\end{displaymath}
in $PSh(C)$. (It is sufficient to demand this for $s \in W \subset \bar W$ to deduce the stability conditions for all morphisms in $\bar W$, since by [[universal colimits]] in the [[presheaf topos]] $PSh(C)$ the pullback of a colimit is a colimit of pullbacks.)

Similarly, to see that we can find $Y \to X$ we use the [[co-Yoneda lemma]] to decompose $X$ as a [[colimit]] of [[representable functor|representables]] $X \simeq {\lim_{\to}_j} K_j$ and then use [[universal colimits]] to deduce that we are looking at a diagram of the form

\begin{displaymath}
\itexarray{
    {\lim_{\to}}_r s^* K_r &\to& S(\{U_i\})
    \\
    \downarrow && \downarrow^{\mathrlap{s}}
    \\
    {\lim_\to}_r j(K_r) &\to& j(U)
  }
  \,.
\end{displaymath}
Since $\bar W$ is closed under colimits, it is hence sufficient that we show the stability condition for $X$ any representable. So we need to fill diagrams of the form

\begin{displaymath}
\itexarray{
    Y &\to& S(\{U_i\})
    \\
    \downarrow && \downarrow^{\mathrlap{s}}
    \\
    j(K) &\to& j(U)
  }
  \,.
\end{displaymath}
For this now use the single condition on a [[coverage]]: that for $\{U_i \to U\}$ a covering family in the [[site]] $(C,J)$ we can find a covering family $\{K_j \to K\}$ such that every $K_j \to K$ factors through one of the $U_i \to U$. But this means that also the [[sieve]]s factor, and we have a commuting diagram

\begin{displaymath}
\itexarray{
    S(\{K_j\}) &\to& S(\{U_i\})
    \\
    \downarrow && \downarrow
    \\
    j(K) &\to& j(U)
  }
  \,.
\end{displaymath}
This shows that $\bar W$ satisfies the first condition at [[factorization system]].

The second condition at [[calculus of fractions]] demands that if two composites of the form

\begin{displaymath}
X \stackrel{\to}{\to} S(\{U_i\}) \to j(U)
\end{displaymath}
are equal in $PSh(C)$, then there is a morphism $Y \to X$ in $PSh(C)$ such that the two composites

\begin{displaymath}
Y \to X \stackrel{\to}{\to} S(\{U_i\})
\end{displaymath}
are equal. But the [[sieve]] inclusions are [[monomorphism]]s, hence this condition is trivially satisyfied (choose $Y \to X$ to be the [[identity]] on $X$). Again by decomposing into colimits by the [[co-Yoneda lemma]] and using [[universal colimits]] and the pasting law for [[pullback]]s, the same follows for general morphisms in $\bar W$

\begin{displaymath}
\itexarray{
    {\lim_\to}_k X_k &\stackrel{\simeq}{\to}& X
    \\
    \downarrow \downarrow && \downarrow \downarrow
    \\
    {\lim_\to}_k S(U_{k,i}) &\to& Y
    \\
    \downarrow && \downarrow 
    \\
    {\lim_\to}_k j(U_k) &\stackrel{\simeq}{\to}& j(U)
  }
  \,.
\end{displaymath}
by applying the above on each component $k$ of the colimit.

This gives us the [[localization]] $L : PSh(C) \to Sh_J(C)$ as described at [[calculus of fractions]]. By the discussion there we have that $Sh_J(C)$ is equivalently given by the category $PSh(C)[W^{-1}]$ with the same objects as $PSh(C)$ and [[hom-set]]s given by

\begin{displaymath}
PSh(C)[W^{-1}](X,A) 
   \simeq
 {\lim_\to}_{\{\hat X \stackrel{w \in \hat W}{\to} X\}}
  PSh_C(\hat X,A)
  \,.
\end{displaymath}
So we have that for $X \in PSh(C)$ a presheaf and $A \in Sh_J(C)$ the [[hom-set]] $Sh_C(L(X),A)$ is given by

\begin{displaymath}
Sh_C(L(X), A) \simeq
  {\lim_{\to}}_{\hat X \stackrel{w \in \bar W}{\to} X} PSh_C(\hat X,A)
  \,.
\end{displaymath}
But if $A$ is a sheaf, it is a $\bar W$-[[local object]] and hence $PSh_C(\hat X \stackrel{w}{\to} X, A)$ is an [[isomorphism]] for all $w \in \bar W$. Hence the above colimit is over a diagram constant on its value at $w = Id : X \to X$ therefore we have a [[natural isomorphism]]

\begin{displaymath}
\cdots \simeq
  PSh_C(X,A)
  \,.
\end{displaymath}
This demonstrates the [[adjunction]] $(L \dashv i)$.

\end{proof}
\hypertarget{construction}{}\subsubsection*{{Construction}}\label{construction}

\begin{cor}
\label{}\hypertarget{}{}
For $X \in PSh(C)$ a [[presheaf]] on the [[site]] $(C,J)$, its \textbf{sheafification} $L(X)$ is the presheaf given on any $U \in C$ by

\begin{displaymath}
L(X) : U \mapsto {\lim_\to}_{\{\hat U \stackrel{w}{\to} j(U)\}} PSh_C(\hat U, X)
  \,,
\end{displaymath}
where the [[colimit]] on the right is over all $w \in \bar W$.

\end{cor}
\begin{proof}
By the [[Yoneda lemma]] we have

\begin{displaymath}
L(X)(U) \simeq PSh_C(j(U), L(X))
  \,.
\end{displaymath}
By the \hyperlink{ExistenceOfLeftAdjoint}{above proposition} this is

\begin{displaymath}
\cdots \simeq Sh_C(L(j(U)), L(X))
  \,.
\end{displaymath}
By the proof of the above proposition, using the formulas discussed at [[calculus of fractions]], this hom-set is given by

\begin{displaymath}
\cdots \simeq {\lim_\to}_{\{ \hat U \stackrel{w \in \bar W}{\to} j(U)\}} PSh_C(\hat U, X)
  \,.
\end{displaymath}
\end{proof}
\begin{observation}
\label{}\hypertarget{}{}
By the definition of $\bar W$, the morphisms $\hat U \to j(U)$ in $\bar W$ are colimits of diagrams of [[covering]] [[sieve]]s

\begin{displaymath}
\hat U \simeq 
    {\lim_\to}_{\{K \to U\}} S(\{K_i\}) \to {\lim_\to}_{\{K \to U\}} j(K)
  \,.
\end{displaymath}
This means (\ldots{}) that the above colimit may be computed as two consecutive colimits of the form

\begin{displaymath}
{\lim_{\to}}_{\{S(\{U_i\}) \to j(U)\}} PSh_C(S(\{U_i\}), X)
  \,.
\end{displaymath}
One such application is called the [[plus construction]].

\end{observation}
\begin{observation}
\label{}\hypertarget{}{}
A morphism $S(\{U_i\}) \to X$ out of a [[sieve]] into any presheaf is in components precisely a [[matching family]] of the presheaf $X$ on the [[covering]] $\{U_i \to U\}$.

\end{observation}
\begin{proof}
Use that the sieve is the [[coequalizer]]

\begin{displaymath}
S(\{U_i\}) \to \coprod_i j(U_i) \stackrel{\to}{\to}
   \coprod_{i,j} j(U_i) \times_{j(U)} j(U_j)
\end{displaymath}
and that the [[hom-functor]] $PSh_C(-,X)$ sends [[colimit]]s to [[limit]]s. More details on this computation are at [[sheaf]].

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
The [[unit of an adjunction|unit]] of the $(L \dashv i)$-[[adjunction]] has as components natural morphisms

\begin{displaymath}
X \to L X
\end{displaymath}
in $PSh(C)$, from any presheaf into its sheafification. By general properties of [[reflective subcategories]] these morphisms are mapped to [[isomorphism]]s by $L : PSh(C) \to Sh(C)$. Therefore these are [[local isomorphism]]s.

So every presheaf is related by a [[local isomorphism]] to its sheafification.

\end{remark}
\hypertarget{for_sheaves_with_values_in_categories_other_than_}{}\subsection*{{For sheaves with values in categories other than $Set$}}\label{for_sheaves_with_values_in_categories_other_than_}

For presheaves with values in categories other than [[Set]], sheafification may be a difficult problem, unless one has some extra assumptions.

\hypertarget{with_values_in_models_for_finitelimit_theories}{}\subsubsection*{{With values in models for finite-limit theories}}\label{with_values_in_models_for_finitelimit_theories}

Consider a type of structure $T$ defined in terms of an [[essentially algebraic theory]] finite limits (such as [[group]]s, [[algebra]]s, [[module]]s, etc.), then [[internal logic|internal]] $T$-[[algebra over an algebraic theory|models]] are preserved by both [[direct image]]s and [[inverse image]]s of [[geometric morphism]]s. Therefore, the [[adjunction]] $(L \dashv i) : Sh_J(C) \to PSh(C)$ directly induces an adjunction between $T$-models in sheaves and presheaves. And since finite limits of sheaves and presheaves are computed pointwise, $T$-models in the category of (pre)sheaves are the same as (pre)sheaves of $T$-models-in-$Set$.

\hypertarget{using_the_ipcproperty}{}\subsubsection*{{Using the IPC-property}}\label{using_the_ipcproperty}

If a [[category]] $A$ satisfies the following assumptions, sheafification of presheaves in $[S^{op}, A]$ exists and is constructed analogously as for [[Set]]-valued sheaves.

\begin{itemize}%
\item $A$ admits small [[limit]]s;
\item $A$ admits small [[colimit]]s;
\item small [[filtered category|filtered colimit]]s in $A$ are exact;
\item $A$ satisfies the [[IPC-property]] .

\end{itemize}
This is true for instance for

\begin{itemize}%
\item the category [[Set]] of sets;


\item the category [[Grp]] of groups;


\item the category $k Alg$ of $k$-algebras;


\item the category $Mod(R)$ of [[module]]s,



\end{itemize}
(but all of these are also $T$-models for finite-limit theories $T$).

One should say more: there are so many applications and fairly difficult theorems there; for example van \newline Osdol's work.

[[Mike Shulman|Mike]]: Another way to think about this is: if you have a type of structure $T$ defined in terms of finite limits (such as groups, algebras, modules, etc.), then [[internal logic|internal]] $T$-models are preserved by both direct and inverse images of geometric morphisms. Therefore, the adjunction between sheaves and presheaves of sets directly induces an adjunction between $T$-models in sheaves and presheaves. And since finite limits of sheaves and presheaves are computed pointwise, $T$-models in the category of (pre)sheaves are the same as (pre)sheaves of $T$-models-in-$Set$.

If $T$ is \emph{not} defined in terms of finite limits, then internal $T$-models in sheaves need not be the same as sheaves of $T$-models-in-$Set$. My intuition would be that the former, rather than the latter, is the more interesting and important notion. For instance, a local ring in a topos of sheaves is a sheaf of rings whose \emph{stalks} are local, rather than a sheaf taking values in the category of local rings, and this is usually what people care about. But since people have studied the other version, there must be important examples of it as well?

[[Urs Schreiber|Urs]]: okay, I have added this to the above now -- so is the IPC-property business really unnecessary for the examples above?

[[Mike Shulman|Mike]]: I'm pretty sure it is not. Does anyone have any examples where the IPC-property business is important?

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item \textbf{sheafification}, [[plus-construction on presheaves]]


\item [[(∞,1)-sheafification]] / [[∞-stackification]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

The description of sheafification in terms of [[local isomorphism]]s is in section 16.3 (for [[Set]]-valued presheaves) and section 17.4 (for more general presheaves) of

\begin{itemize}%
\item Kashiwara--Schapira, \emph{[[Categories and Sheaves]]}

\end{itemize}
The description in terms of [[dense monomorphism]]s using [[Lawvere-Tierney topology]] is in section V.3 of

\begin{itemize}%
\item [[Saunders Mac Lane]] and [[Ieke Moerdijk]], \emph{[[Sheaves in Geometry and Logic]]}

\end{itemize}
Extension of sheafification of presheaves with values in other categories has been advanced in

\begin{itemize}%
\item [[Alex Heller]], K. A. Rowe, \emph{On the category of sheaves}, Amer. J. Math. 84, 1962, 205-216


\item Barr, Grillet, and Van Osdol, \emph{Exact categories and categories of sheaves}, Lecture Notes in Math., Vol. 236, Springer, Berlin, 1971


\item Friedrich Ulmer, \emph{On the existence and exactness of the associated sheaf functor}, J. Pure Appl. Algebra 3, 1971, 295-306


\item [[Alexander Rosenberg]], \emph{Almost quotient categories, sheaves and localizations}, 181 p. Seminar on supermanifolds 25, University of Stockholm, D. Leites editor, 1988 (in Russian; partial remake in English exists)



\end{itemize}
Discussion in [[homotopy type theory]] is in

\begin{itemize}%
\item Kevin Quirin, Nicolas Tabareau, \emph{Lawvere-Tierney sheafification in Homotopy Type Theory}, Journal of Formalized Reasoning, Vol 9, No 2, (2016) (\href{https://jfr.unibo.it/article/view/6232}{web})

\end{itemize}
category: sheaf theory [[!redirects sheafification functor]] [[!redirects associated sheaf]] [[!redirects associated sheaf functor]]



\end{document}