\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*{geometry of physics – basic notions of category theory}

\hypertarget{BasicNotionsOfCategoryTheory}{}\subsection*{{Basic notions of Category theory}}\label{BasicNotionsOfCategoryTheory}

We introduce here the basic notions of [[category theory]], along with examples and motivation from [[geometry]]:

\begin{enumerate}%
\item \emph{\hyperlink{CategoriesAndFunctors}{Categories and functors}}


\item \emph{\hyperlink{NaturalTransformationsAndPresheaves}{Natural transformations and presheaves}}


\item \emph{\hyperlink{Adjunctions}{Adjunctions}}


\item \emph{\hyperlink{Equivalences}{Equivalences}}


\item \emph{\hyperlink{Modalities}{Modalities}}



\end{enumerate}
This constitutes what is sometimes called the \emph{language of categories}. While we state and prove some basic facts here, notably the notorious \emph{[[Yoneda lemma]]} (Prop. \ref{YonedaLemma} below), what makes [[category theory]] be a \emph{mathematical theory} in the sense of a coherent collection of non-trivial [[theorems]] is all concerned with the topic of \emph{[[universal constructions]]}, which may be formulated (only) in this language. This we turn to further \hyperlink{UniversalConstructions}{below}.

$\,$

\hypertarget{CategoriesAndFunctors}{}\subsubsection*{{Categories and Functors}}\label{CategoriesAndFunctors}

The notion of a \emph{[[category]]} (Def. \ref{Categories} below) embodies the idea of [[structuralism]] applied to concepts in [[mathematics]]: it collects, on top of the [[set]] (or generally: [[class]]) of mathematical [[objects]] that belong to it, also all the \emph{[[structure]]-preserving maps} between them, hence the [[homomorphisms]] in the case of [[Bourbaki]]-style [[mathematical structures]].

The first achievement of the notion of a [[category]] is to abstract away from such manifestly \emph{[[concrete categories]]} (Examples \ref{ExamplesOfConcreteCategories}, \ref{StructuredSetsAndFaithfulFunctors} below) to more indirectly defined mathematical objects whose ``structure'' is only defined, after the fact, by which maps, now just called \emph{[[morphisms]]}, there are between them.

This [[structuralism]]-principle bootstraps itself to life by considering [[morphisms]] between [[categories]] themselves to be those ``maps'' that respect their [[structuralism]], namely the connectivity and [[composition]] of the [[morphisms]] between their objects: These are the \emph{[[functors]]} (Def. \ref{Functors} below).

For the purpose of [[geometry]], a key class of examples of [[functors]] are the assignments of \emph{[[algebras of functions]] to [[spaces]]}, this is Example \ref{SpacesViaAlgebrasOfFunctions} below.

$\,$

\begin{defn}
\label{Categories}\hypertarget{Categories}{}
\textbf{([[category]])}

A \emph{[[category]]} $\mathcal{C}$ is

\begin{enumerate}%
\item a [[class]] $Obj_{\mathcal{C}}$, called the \emph{class of [[objects]]};


\item for each [[pair]] $X,Y \in Obj_{\mathcal{C}}$ of [[objects]], a [[set]] $Hom_{\mathcal{C}}(X,Y)$, called the \emph{[[set of morphisms]] from $X$ to $Y$}, or the \emph{[[hom-set]]}, for short.

We denote the elements of this set by arrows like this:

\begin{displaymath}
X \overset{f}{\longrightarrow} Y \;\;\in Hom_{\mathcal{C}}(X,Y)
  \,.
\end{displaymath}

\item for each [[object]] $X \in Obj_{\mathcal{C}}$ a morphism

\begin{displaymath}
X \overset{id_X}{\to} X \;\; \in Hom_{\mathcal{C}}(X,X)
\end{displaymath}
called the \emph{[[identity morphism]]} on $X$;


\item for each [[triple]] $X_1, X_2, X_3 \in Obj$ of [[objects]], a [[function]]

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{C}}(X_1, X_2)
    &\times&
    Hom_{\mathcal{C}}(X_2, X_3)
    &\overset{\circ_{X_1,X_2,X_3}}{\longrightarrow}&
    Hom_{\mathcal{C}}(X_1, X_3)
    \\
    X_1 \overset{f}{\to} X_2
    &,&
    X_2 \overset{f}{\to} X_3
    &\mapsto&
    X_1 \overset{ g \circ f }{\longrightarrow} X_3
  }
\end{displaymath}
called \emph{[[composition]]};



\end{enumerate}
such that:

\begin{enumerate}%
\item for all [[pairs]] of [[objects]] $X,Y \in Obj_{\mathcal{C}}$ [[unitality]] holds: given

\begin{displaymath}
X \overset{f}{\to} Y \;\;\in Hom_{\mathcal{C}}(X,Y)
\end{displaymath}
then

\begin{displaymath}
X \overset{id_Y \circ f}{\longrightarrow} Y
  \;=\;
  X \overset{f}{\longrightarrow} Y
  \;=\;
  X \overset{f \circ id_X }{\longrightarrow} Y
  \,;
\end{displaymath}

\item for all [[quadruples]] of [[objects]] $X_1, X_2, X_3, X_4 \in Obj_{\mathcal{C}}$ [[composition]] satifies \emph{[[associativity]]}: given

\begin{displaymath}
X_1
    \overset{f_{12}}{\to}
  X_2
    \overset{f_{23}}{\to}
  X_3
    \overset{f_{34}}{\to}
  X_4
\end{displaymath}
then

\begin{displaymath}
X_1 \overset{f_{34} \circ (f_{23} \circ f_{12})}{\longrightarrow} X_4
  \;\;=\;\;
  X_1 \overset{(f_{34} \circ f_{23}) \circ f_{12}}{\longrightarrow} X_4
  \,.
\end{displaymath}


\end{enumerate}
\end{defn}
The archetypical example of a [[category]] is the [[category of sets]]:

\begin{example}
\label{CategoryOfSets}\hypertarget{CategoryOfSets}{}
\textbf{([[Set|category of all sets]])}

The [[class]] of all [[sets]] with [[functions]] between them is a [[category]] (Def. \ref{Categories}), to be denoted \emph{[[Set]]}:

\begin{itemize}%
\item $Obj_{Set} = \text{class of all sets}$;


\item $Hom_{Set}(X,Y) = \text{set of functions from set X to set Y}$;


\item $id_X \in Hom_{Set}(X,X) =$ [[identity function]] on set $X$;


\item $\circ_{X_1,X_2,X_3} = \text{ordinary composition of functions}$.



\end{itemize}
\end{example}
More generally all kind of \emph{sets with [[structure]]}, in the sense going back to [[Bourbaki]], form categories, where the [[morphisms]] are the \emph{[[homomorphisms]]} (whence the name ``morphism''!). These are called \emph{[[concrete categories]]} (we characterize them precisely in Example \ref{StructuredSetsAndFaithfulFunctors}, further below):

\begin{example}
\label{ExamplesOfConcreteCategories}\hypertarget{ExamplesOfConcreteCategories}{}
\textbf{(basic examples of [[concrete categories]])}

For $\mathcal{S}$ a kind of [[mathematical structure]], there is the [[category]] (Def. \ref{Categories}) $\mathcal{S}Set$ whose [[objects]] are the corresponding [[structured sets]], and whose [[morphisms]] are the corresponding structure [[homomorphisms]], hence the [[functions]] of underlying sets which respect the given structure.

 Basic examples of [[concrete categories]] include the following:

\begin{tabular}{l|l|l}
$\phantom{A}$[[concrete category]]$\phantom{A}$&$\phantom{A}$[[objects]]$\phantom{A}$&$\phantom{A}$[[morphisms]]$\phantom{A}$\\
\hline 
$\phantom{A}$[[Set]]&$\phantom{A}$[[sets]]&$\phantom{A}$[[functions]]\\
$\phantom{A}$[[Top]]&$\phantom{A}$[[topological spaces]]$\phantom{A}$&$\phantom{A}$[[continuous functions]]$\phantom{A}$\\
$\phantom{A}$[[Mfd]]${}_{k}$&$\phantom{A}$[[differentiable manifolds]]$\phantom{A}$&$\phantom{A}$[[differentiable functions]]$\phantom{A}$\\
$\phantom{A}$[[Vect]]&$\phantom{A}$[[vector spaces]]$\phantom{A}$&$\phantom{A}$[[linear functions]]$\phantom{A}$\\
$\phantom{A}$[[Grp]]&$\phantom{A}$[[groups]]$\phantom{A}$&$\phantom{A}$[[group homomorphisms]]$\phantom{A}$\\
$\phantom{A}$[[Alg]]&$\phantom{A}$[[algebras]]$\phantom{A}$&$\phantom{A}$[[algebra homomorphism]]$\phantom{A}$\\
\end{tabular}

\end{example}
This is the motivation for the terminology ``categories'', as the examples in Example \ref{ExamplesOfConcreteCategories} are literally \emph{categories of mathematical structures}. But not all categories are ``[[concrete category|concrete]]'' in this way.

Some terminology:

\begin{defn}
\label{CommutingDiagram}\hypertarget{CommutingDiagram}{}
\textbf{([[commuting diagram]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}), then a [[directed graph]] with [[edges]] labeled by [[morphisms]] of the category is called a \emph{[[commuting diagram]]} if for any two [[vertices]] any two ways of passing along edges from one to the other yields the same [[composition]] of the corresponding [[morphisms]].

For example, a \emph{commuting triangle} is

\begin{displaymath}
f = h \circ g
  \phantom{AAAAAA}
  \itexarray{
    && X
    \\
    & {}^{\mathllap{ g }}\swarrow && \searrow^{ \mathrlap{ f } }
    \\
    Y && \underset{\phantom{A}h\phantom{A}}{\longrightarrow}  && Z
  }
\end{displaymath}
while a \emph{[[commuting square]]} is

\begin{displaymath}
g_1 \circ f_1
  \;=\;
  g_2 \circ f_2
  \phantom{AAAAAA}
  \itexarray{
    X &\overset{\phantom{A}f_1\phantom{A}}{\longrightarrow}& Y_1
    \\
    {}^{ \mathllap{f_2} }\big\downarrow && \big\downarrow^{\mathrlap{ g_1 }}
    \\
    Y_2 &\underset{\phantom{A}g_2\phantom{A}}{\longrightarrow}&  Z
  }
\end{displaymath}
\end{defn}
\begin{defn}
\label{InitialObject}\hypertarget{InitialObject}{}
\textbf{([[initial object]] and [[terminal object]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}). Then

\begin{enumerate}%
\item an [[object]] $\ast \in \mathcal{C}$ is called a \emph{[[terminal object]]} if for every other [[object]] $c \in \mathcal{C}$, there is a unique [[morphism]] from $c$ to $\ast$

\begin{displaymath}
c \overset{\exists!}{\longrightarrow} \ast
\end{displaymath}
hence if the [[hom-set]] is a [[singleton]] $\ast \in Set$:

\begin{displaymath}
Hom_{\mathcal{C}}(c,\ast) \;\simeq\; \ast
  \,.
\end{displaymath}

\item an [[object]] $\emptyset \in \mathcal{C}$ is called an \emph{[[initial object]]} if for every other [[object]] $c \in \mathcal{C}$, there is a unique [[morphism]] from $\emptyset$ to $c$

\begin{displaymath}
\emptyset \overset{\exists!}{\longrightarrow} c
\end{displaymath}
hence if the [[hom-set]] is a [[singleton]] $\ast \in Set$:

\begin{displaymath}
Hom_{\mathcal{C}}(\emptyset,c) \;\simeq\; \ast
  \,.
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{defn}
\label{SmallCategory}\hypertarget{SmallCategory}{}
\textbf{([[small category]])}

If a [[category]] $\mathcal{C}$ (Def. \ref{Categories}) happens to have as [[class]] $Obj_{\mathcal{C}}$ of [[objects]] an actual [[set]] (i.e. a [[small set]] instead of a [[proper class]]), then $\mathcal{C}$ is called a \emph{[[small category]]}.

\end{defn}
As usual, there are some trivial examples, that are however usefully made explicit for the development of the theory:

\begin{example}
\label{InitialCategoryAndTerminalCategory}\hypertarget{InitialCategoryAndTerminalCategory}{}
\textbf{([[initial category]] and [[terminal category]])}

\begin{enumerate}%
\item The \emph{[[terminal category]]} $\ast$ is [[generalized the|the]] [[category]] (Def. \ref{Categories}) whose [[class]] of [[objects]] is [[generalized the|the]] [[singleton]] [[set]], and which has a single [[morphism]] on this object, necessarily the [[identity morphism]].


\item The \emph{[[initial category]]} or \emph{[[empty category]]} $\emptyset$ is the [[category]] (Def. \ref{Categories}) whose [[class]] of [[objects]] is the [[empty set]], and which, hence, has no morphism whatsoever.



\end{enumerate}
Clearly, these are [[small categories]] (Def. \ref{SmallCategory}).

\end{example}
\begin{example}
\label{PartiallyOrderedSetsAsSmallCategories}\hypertarget{PartiallyOrderedSetsAsSmallCategories}{}
\textbf{([[preordered sets]] as [[thin categories]])}

Let $(S, \leq)$ be a [[preordered set]]. Then this induces a [[small category]] whose [[set]] of [[objects]] is $S$, and which has precisely one morphism $x \to y$ whenever $x \leq y$, and no such morphism otherwise:

\begin{equation}
x \overset{\exists !}{\to} y
  \phantom{AAA}
  \text{precisely if}
  \phantom{AAA}
  x \leq y
\label{RelationsAsMorphismInPartiallyOrderedSet}\end{equation}
Conversely, every [[small category]] with at most one morphism from any object to any other, called a \emph{[[thin category]]}, induces on its set of objects the [[structure]] of a [[partially ordered set]] via \eqref{RelationsAsMorphismInPartiallyOrderedSet}.

Here the [[axioms]] for [[preordered sets]] and for [[categories]] match as follows:

\newline | $\phantom{A}$[[partially ordered sets]]$\phantom{A}$ | $\phantom{A}$ $x \leq x$ $\phantom{A}$ | $\phantom{A}$ $(x \leq y \leq z) \Rightarrow (x \leq z)$ $\phantom{A}$ | | $\phantom{A}$[[thin categories]]$\phantom{A}$ | $\phantom{A}$[[identity morphisms]]$\phantom{A}$ | $\phantom{A}$[[composition]]$\phantom{A}$ |

\end{example}
\begin{defn}
\label{Isomorphism}\hypertarget{Isomorphism}{}
\textbf{([[isomorphism]])}

For $\mathcal{C}$ a [[category]] (Def. \ref{Categories}), a [[morphism]]

\begin{displaymath}
X \overset{f}{\to} Y \;\;\in Hom_{\mathcal{C}}(X,Y)
\end{displaymath}
is called an \emph{[[isomorphism]]} if there exists an [[inverse morphism]]

\begin{displaymath}
Y \overset{f^{-1}}{\longrightarrow} Y \;\; \in Hom_{\mathcal{C}}(Y,X)
\end{displaymath}
namely a morphism such that the [[compositions]] with $f$ are equal to the [[identity morphisms]] on $X$ and $Y$, respectively

\begin{displaymath}
f^{-1} \circ f  \;=\; id_X
  \phantom{AAA}
  f \circ f^{-1} \;=\; id_Y
\end{displaymath}
\end{defn}
\begin{defn}
\label{Groupoid}\hypertarget{Groupoid}{}
\textbf{([[groupoid]])}

If $\mathcal{C}$ is a [[category]] in which \emph{every} [[morphism]] is an [[isomorphism]] (Def. \ref{Isomorphism}), then $\mathcal{C}$ is called a \emph{[[groupoid]]}.

\end{defn}
\begin{example}
\label{DeloopingGroupoid}\hypertarget{DeloopingGroupoid}{}
\textbf{([[delooping]] [[groupoid]])}

For $G$ a [[group]], there is a [[groupoid]] (Def. \ref{Groupoid}) $\mathbf{B}G$ with a single [[object]], whose single [[hom-set]] is $G$, with [[identity morphism]] the [[neutral element]] and [[composition]] the group operation in $G$:

\begin{itemize}%
\item $Obj_{\mathbf{B}G} = \ast$


\item $Hom_{\mathcal{C}}(\ast,\ast) \;=\; G$



\end{itemize}
In fact every [[groupoid]] with precisely one object is of the form.

\end{example}
\begin{remark}
\label{}\hypertarget{}{}
\textbf{([[groupoids]] and [[homotopy theory]])}

Even though [[groupoids]] (Def. \ref{Groupoid}) are special cases of [[categories]] (Def. \ref{Categories}), the theory of groupoids in itself has a rather different flavour than that of category theory: Part of the [[homotopy hypothesis]]-theorem is that the theory of groupoids is really \emph{[[homotopy theory]]} for the special case of [[homotopy 1-types]].

(In applications in [[homotopy theory]], groupoids are considered mostly in the case that the [[class]] $Obj_{\mathcal{C}}$ of [[objects]] is in fact a [[set]]: \emph{[[small groupoids]]}, Def. \ref{SmallCategory}).

For this reason we will not have more to say about [[groupoids]] here, and instead relegate their discussion to the section on homotopy theory, further \hyperlink{BasicNotionsOfHomotopyTheory}{below}.

\end{remark}
There is a range of constructions that provide new categories from given ones:

\begin{example}
\label{OppositeCategory}\hypertarget{OppositeCategory}{}
\textbf{([[opposite category]] and [[formal duality]])}

Let $\mathcal{C}$ be a [[category]]. Then its \emph{[[opposite category]]} $\mathcal{C}^{op}$ has the same [[objects]] as $\mathcal{C}$, but the direction of the [[morphisms]] is reversed. Accordingly, [[composition]] in the [[opposite category]] $\mathcal{C}^{op}$ is that in $\mathcal{C}$, but with the order of the arguments reversed:

\begin{itemize}%
\item $Obj_{\mathcal{C}^{op}} \;\coloneqq\; Obj_{\mathcal{C}}$;


\item $Hom_{\mathcal{C}^{op}}(X,Y) \;\coloneqq\; Hom_{\mathcal{C}}(Y,X)$.



\end{itemize}
Hence for every statementa about some [[category]] $\mathcal{C}$ there is a corresponding ``dual'' statement about its opposite category, which is ``the same but with the direction of all morphisms reversed''. This relation is known as \emph{[[formal duality]].}

\end{example}
\begin{example}
\label{ProductCategory}\hypertarget{ProductCategory}{}
\textbf{([[product category]])}

Let $\mathcal{C}$ and $\mathcal{D}$ be two [[categories]] (Def. \ref{Categories}). Then their \emph{[[product category]]} $\mathcal{C} \times \mathcal{D}$ has as [[objects]] [[pairs]] $(c,d)$ with $c \in Obj_{\mathcal{C}}$ and $d \in Obj_{\mathcal{D}}$, and as morphisms [[pairs]] $(c_1 \overset{f}{\to} c_2) \in Hom_{\mathcal{C}}(c_1,c_2)$, $(d_1 \overset{g}{\to} d_2) \in Hom_{\mathcal{D}}(d_1,d_2)$, and [[composition]] is defined by composition in each entry:

\begin{itemize}%
\item $Obj_{\mathcal{C} \times \mathcal{D}} \coloneqq Obj_{\mathcal{C}} \times Obj_{\mathcal{D}}$;


\item $Hom_{\mathcal{C} \times \mathcal{D}}( (c_1,d_1), (c_2,d_2) ) \coloneqq  Hom_{\mathcal{C}}(c_1,c_2) \times Hom_{\mathcal{D}}( d_1, d_2 )$


\item $(f_2, g_2) \circ (f_1, g_1) \;\coloneqq\; ( f_2 \circ f_1, g_2 \circ g_1 )$



\end{itemize}
\end{example}
\begin{defn}
\label{Functors}\hypertarget{Functors}{}
\textbf{([[functor]])}

Let $\mathcal{C}$ and $\mathcal{D}$ be two [[categories]] (Def. \ref{Categories}). A \emph{[[functor]] from $\mathcal{C}$ to $\mathcal{D}$}, to be denoted

\begin{displaymath}
\mathcal{C} \overset{F}{\longrightarrow} \mathcal{D}
\end{displaymath}
is

\begin{enumerate}%
\item a [[function]] between the classes of [[objects]]:

\begin{displaymath}
F_{Obj} \;\colon\; Obj_{\mathcal{C}} \longrightarrow Obj_{\mathcal{D}}
\end{displaymath}

\item for each [[pair]] $X,Y \in Obj_{\mathcal{C}}$ of objects a [[function]]

\begin{displaymath}
F_{X,Y} 
    \;\colon\;  
  Hom_{\mathcal{C}}(X,Y) 
    \longrightarrow 
  Hom_{\mathcal{D}}(F_{Obj}(X), F_{Obj}(Y))
\end{displaymath}


\end{enumerate}
such that

\begin{enumerate}%
\item For each [[object]] $X \in Obj_{\mathcal{C}}$ the [[identity morphism]] is respected:

\begin{displaymath}
F_{X,X}(id_X) \;=\; id_{F_{Obj}(X)}
  \,;
\end{displaymath}

\item for each [[triple]] $X_1, X_2, X_3 \in Obj_{\mathcal{C}}$ of [[objects]], [[composition]] is respected: given

\begin{displaymath}
X_1 \overset{f}{\longrightarrow} X_2 \overset{g}{\longrightarrow} X_3
\end{displaymath}
we have

\begin{displaymath}
F_{X_1, X_3}(g \circ f ) \;=\;  F_{X_2, X_3}(g) \circ F_{X_1,X_2}(f)
   \,.
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{example}
\label{CategoriesOfSmallCategories}\hypertarget{CategoriesOfSmallCategories}{}
\textbf{([[categories]] of [[small categories]] and of [[small groupoids]])}

It is clear that [[functors]] (Def. \ref{Functors}) have a [[composition]] operation given componentwise by the [[composition]] of their component functions. Accordingly, this composition is [[unitality|unital]] and [[associativity|associative]]. This means that there is

\begin{enumerate}%
\item the [[category]] (Def. \ref{Categories}) \emph{[[Cat]]} whose [[objects]] are [[small categories]] (Def. \ref{SmallCategory}) and whose [[morphisms]] are [[functors]] (Def. \ref{Functors}) between these


\item the [[category]] (Def. \ref{Categories}) \emph{[[Grpd]]} whose [[objects]] are [[small groupoids|small]] [[groupoids]] (Def. \ref{Groupoid}) and whose [[morphisms]] are [[functors]] (Def. \ref{Functors}) between these.



\end{enumerate}
\end{example}
\begin{example}
\label{HomFunctor}\hypertarget{HomFunctor}{}
\textbf{([[hom-functor]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}). Then its \emph{[[hom-functor]]}

\begin{displaymath}
Hom_{\mathcal{C}}
  \;\colon\;
  \mathcal{C}^{op} \times \mathcal{C}
    \longrightarrow
  Set
\end{displaymath}
is the [[functor]] (Def. \ref{Functors}) out of the [[product category]] (Def. \ref{ProductCategory}) of $\mathcal{C}$ with its [[opposite category]] to the [[category of sets]], which sends a [[pair]] $X,Y \in \mathcal{C}$ of [[objects]] to the [[hom-set]] $Hom_{\mathcal{C}}(X,Y)$ between them, and which sends a [[pair]] of [[morphisms]], with one of them into $X$ and the other out of $Y$, to the operation of [[composition]] with these morphisms:

\begin{displaymath}
Hom_{\mathcal{C}}
  \;\;\colon\;\;\;
  \itexarray{
    X_1 & Y_1
    \\
    {}^{\mathllap{g}}\big\uparrow & \big\downarrow^{\mathrlap{h}}
    \\
    X_2 & Y_2
  }
  \;\;\mapsto\;\;
  \itexarray{
    Hom_{\mathcal{C}}(X_1, Y_1)
    \\
    \big\downarrow^{ \mathrlap{ f \mapsto h \circ f \circ g  } }
    \\
    Hom_{\mathcal{C}}(X_2, Y_2)
  }
\end{displaymath}
\end{example}
\begin{defn}
\label{Monomorphism}\hypertarget{Monomorphism}{}
\textbf{([[monomorphism]] and [[epimorphism]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}). Then a [[morphism]] $X \overset{f}{\to } Y$ in $\mathcal{C}$ is called

\begin{itemize}%
\item a \emph{[[monomorphism]]} if for every [[object]] $Z \in \mathcal{C}$ the [[hom-functor]] (Example \ref{HomFunctor}) out of $Z$ takes $f$ to an [[injective function]] of [[hom-sets]]:

\begin{displaymath}
Hom_{\mathcal{C}}(Z,f)
  \;\colon\;
  Hom_{\mathcal{C}}(Z,X)
   \overset{\phantom{AAA}}{\hookrightarrow}
  Hom_{\mathcal{C}}(Z,Y)
  \,;
\end{displaymath}

\item an \emph{[[epimorphism]]} if for every [[object]] $Z \in \mathcal{Z}$ the [[hom-functor]] (Example \ref{HomFunctor}) into $Z$ takes $f$ to an [[injective function]]:

\begin{displaymath}
Hom_{\mathcal{C}}( f,Z )
  \;\colon\;
  Hom_{\mathcal{C}}(Y, Z)
    \overset{\phantom{AAA}}{\hookrightarrow}
  Hom_{\mathcal{C}}(X, Z)
  \,.
\end{displaymath}


\end{itemize}
\end{defn}
\begin{defn}
\label{FullyFaithfulFunctor}\hypertarget{FullyFaithfulFunctor}{}
\textbf{([[full functor|full]], [[faithful functor|faithful]] and [[fully faithful functors]])}

A [[functor]] $F \;\colon\; \mathcal{C} \to \mathcal{D}$ (Def. \ref{Functors}) is called

\begin{itemize}%
\item a \emph{[[full functor]]} if all its hom-functions are [[surjective functions]]

\begin{displaymath}
Hom_{\mathcal{C}}(X,Y)
    \underoverset{surj}{F_{X,Y}}{\longrightarrow}
  Hom_{\mathcal{D}}(F(X), F(Y))
\end{displaymath}

\item a \emph{[[faithful functor]]} if all its hom-functions are [[injective functions]]

\begin{displaymath}
Hom_{\mathcal{C}}(X,Y)
    \underoverset{inj}{F_{X,Y}}{\longrightarrow}
  Hom_{\mathcal{D}}(F(X), F(Y))
\end{displaymath}

\item a \emph{[[fully faithful functor]]} if all its hom-functions are [[bijective functions]]

\begin{displaymath}
Hom_{\mathcal{C}}(X,Y)
    \underoverset{bij}{F_{X,Y}}{\longrightarrow}
  Hom_{\mathcal{D}}(F(X), F(Y))
\end{displaymath}


\end{itemize}
A [[fully faithful functor]] is also called a \emph{[[full subcategory]]-inclusion}. We will denote this situation by

\begin{displaymath}
\mathcal{C} \overset{\phantom{A}F\phantom{A}}{\hookrightarrow} \mathcal{D}
  \,.
\end{displaymath}
\end{defn}
\begin{example}
\label{FullSubcategoryOnClassOfObjects}\hypertarget{FullSubcategoryOnClassOfObjects}{}
\textbf{([[full subcategory]] on a [[subobject|sub]]-[[class]] of [[objects]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}) and let $S \subset Obj_{\mathcal{C}}$ be a [[subobject|sub]]-[[class]] of its [[class]] of [[objects]]. The there is a [[category]] $\mathcal{C}_S$ whose class of [[objects]] is $S$, and whose [[morphisms]] are precisely the morphisms of $\mathcal{C}$, between these given objects:

\begin{displaymath}
Hom_{\mathcal{C}_S}(s_1, s_2)
  \;\coloneqq\;
  Hom_{\mathcal{C}}(s_1, s_2)
\end{displaymath}
with [[identity morphisms]] and [[composition]] defined as in $\mathcal{C}$. Then there is a [[fully faithful functor]] (Def. \ref{FullyFaithfulFunctor})

\begin{displaymath}
\itexarray{
    \mathcal{C}_S &\overset{\phantom{AAAA}}{\hookrightarrow}& \mathcal{C}
  }
\end{displaymath}
which is the evident inclsuion on objects, and the [[identity function]] on all [[hom-sets]].

This is called the \emph{[[full subcategory]] of $\mathcal{C}$ on the objects in $S$}.

Beware that not every [[fully faithful functor]] is, in components, exactly of this form, but, assuming the [[axiom of choice]], every fully faithful functor is so up to \emph{[[equivalence of categories]]} (Def. \ref{EquivalenceOfCategories}).

\end{example}
The concept of \emph{[[faithful functor]]} from Def. \ref{FullyFaithfulFunctor} allows to make precise the idea of \emph{[[concrete category]]} from Example \ref{ExamplesOfConcreteCategories}:

\begin{example}
\label{StructuredSetsAndFaithfulFunctors}\hypertarget{StructuredSetsAndFaithfulFunctors}{}
\textbf{([[structured sets]] and [[faithful functors]])}

Let $\mathcal{S}$ be a kind of [[mathematical structure]] and let $\mathcal{S} Set$ be the [[category]] of $\mathcal{S}$-[[structured sets]]. Then there is the [[forgetful functor]]

\begin{displaymath}
\mathcal{S}Set \longrightarrow Set
\end{displaymath}
which sends each [[structured set]] to the underlying set (``forgetting'' the [[structure]] that it carries), and which sends [[functions]] of sets to themselves. That a [[homomorphism]] of [[structured sets]] is a [[function]] between the underlying sets satisfying a \emph{special condition} implies that this is a \emph{[[faithful functor]]} (Def. \ref{FullyFaithfulFunctor}).

Conversely, it makes sense to \emph{define} [[structured sets]] in general to be the [[objects]] of a [[category]] $\mathcal{C}$ which is equipped with a [[faithful functor]] $\mathcal{C} \overset{faithful}{\longrightarrow} Set$ to the [[category of sets]]. See at \emph{[[structure]]} for more on this.

\end{example}
\begin{example}
\label{SpacesViaAlgebrasOfFunctions}\hypertarget{SpacesViaAlgebrasOfFunctions}{}
\textbf{([[spaces]] seen via their [[algebras of functions]])}

In any given context of [[geometry]], there is typically a [[functor]] which sends any [[space]] of the given kind to its [[algebra of functions]], and which sends a map (i.e. [[homomorphism]]) between the given spaces to the algebra [[homomorphism]] given by precomposition with that map (a [[hom-functor]], Def. \ref{HomFunctor}). Schematically:

\begin{displaymath}
\itexarray{
    \big\{
      \text{geometric spaces}
    \big\}
    &
    \overset{
      \text{algebra of functions}
    }{
      \longrightarrow
    }
    &
    \big\{
      \text{algebras}
    \big\}^{op}
    \\
    \\
    X_1 &\mapsto& FunctionsOn(X_1)
    \\
    {}^{\mathllap{f}}\big\downarrow && \big\uparrow^{ \phi \mapsto \phi \circ f }
    \\
    X_2 &\mapsto& FunctionsOn(X_2)
  }
\end{displaymath}
Since the precomposition operation reverses the direction of [[morphisms]], as shown, these are functors from the given [[category]] of [[spaces]] to the \emph{[[opposite category|opposite]]} (Example \ref{OppositeCategory}) of the relevant category of [[algebras]].

In broad generality, there is a [[duality]] (``[[Isbell duality]]'') between [[geometry]]/[[spaces]] and [[algebra]]/[[algebras of functions]]) (``[[space and quantity]]'', \href{space+and+quantity#Lawvere86}{Lawvere 86}).

We now mention some concrete examples of this general pattern:

$\,$

\textbf{[[topological spaces]] and [[C\emph{-algebras]]*}}

Consider

\begin{enumerate}%
\item the [[category]] [[Top]]${}_{cpt}$ of [[compact topological space|compact]] [[topological spaces|topological]] [[Hausdorff spaces]] with [[continuous functions]] between them;


\item the category [[C\emph{Alg]] of [[unital algebra|unital]] [[C}-algebras]] over the [[complex numbers]]



\end{enumerate}
from Example \ref{ExamplesOfConcreteCategories}.

Then there is a [[functor]] (Def. \ref{Functors})

\begin{displaymath}
C(-)
  \;\colon\;
  Top_{H,cpt}
   \longrightarrow
  C^\ast Alg^{op}
\end{displaymath}
from the former to the [[opposite category]] of the latter (Example \ref{OppositeCategory}) which sends any [[compact topological space|compact]] [[topological space]] $X$ to its [[C\emph{-algebra]] $C(X)$ of [[continuous functions]] $X \overset{\phi}{\to} \mathbb{C}$ with values in the [[complex numbers]], and which sends every [[continuous function]] between compact spaces to the [[C}-algebra]]-[[homomorphism]] that is given by [[precomposition]]:

\begin{displaymath}
C(-)
  \;\;\;\colon\;\;\;
  \itexarray{
    X &\mapsto & C(X)
    \\
    {}^{\mathllap{ f }}\big\downarrow
      &&
    \big\uparrow^{\mathrlap{ f^\ast : \phi \mapsto \phi \circ f }}
    \\
    Y &\mapsto& C(Y)
  }
\end{displaymath}
Part of the statement of \emph{[[Gelfand duality]]} is that this is a [[fully faithful functor]], hence exhibiting a [[full subcategory]]-inclusion (Def. \ref{FullyFaithfulFunctor}), namely that of [[commutative C\emph{-algebras]]:}

\begin{displaymath}
Top_{H,cpt}
   \overset{\phantom{AAA}}{\hookrightarrow}
  C^\ast Alg^{op}
  \,.
\end{displaymath}
$\,$

\textbf{[[affine schemes]] and [[commutative algebras]]}

The starting point of [[algebraic geometry]] is to consider \emph{[[affine schemes]]} as the [[formal duals]] (Example \ref{OppositeCategory}) of [[finitely generated object|finitely generated]] [[commutative algebras]] over some [[algebraically closed field|algebraically closed]] [[ground field]] $\mathbb{K}$:

\begin{equation}
Aff_{\mathbb{K}}
   \;\;\coloneqq\;\;
  CAlg^{fin}_{\mathbb{K}}^{op}
  \,.
\label{FormalDualsOfCommutativeRings}\end{equation}
Beware that the immediate identification \eqref{FormalDualsOfCommutativeRings} is often obscured by the definition of [[affine schemes]] as [[locally ringed spaces]]. While the latter is much more complicated, at face value, in the end it yields an [[equivalence of categories|equivalent]] [[category]] (Def. \ref{EquivalenceOfCategories} below) to the simple [[formal dual|formal dualization]] (Example \ref{OppositeCategory}) in \eqref{FormalDualsOfCommutativeRings}, see \href{affine+scheme#AffineSchemesFullSubcategoryOfOppositeOfRings}{here}. Already in 1973 [[Alexander Grothendieck]] had urged to abandon, as a foundational concept, the more complicated definition in favor of the simpler one in \eqref{FormalDualsOfCommutativeRings}, see \href{functorial+geometry#Lawvere16Quote}{Lawvere 03}.

$\,$

\textbf{[[smooth manifolds]] and [[real numbers|real]] [[associative algebras]]}

Consider

\begin{enumerate}%
\item the [[category]] [[SmthMfd]] of [[smooth manifolds]] with [[smooth functions]] between them;


\item the category [[Alg]]${}_{\mathbb{R}}$ of [[associative algebras]] over the [[real numbers]]



\end{enumerate}
from Example \ref{ExamplesOfConcreteCategories}.

Then there is a [[functor]] (Def. \ref{Functors})

\begin{displaymath}
C^\infty(-)
  \;\colon\;
  SmthMfd
    \longrightarrow
  Alg_{\mathbb{R}}^{op}
\end{displaymath}
from the former to the [[opposite category]] of the latter (Def. \ref{OppositeCategory}), which sends any [[smooth manifold]] $X$ to its [[associative algebra]] $C^\infty(X)$ of [[continuous functions]] $X \overset{\phi}{\to} \mathbb{R}$ to the [[real numbers]], and which sends every [[smooth function]] between smooth manifolds to the [[algebra homomorphism]] that is given by [[precomposition]]:

\begin{displaymath}
C^\infty(-)
  \;\;\;\colon\;\;\;
  \itexarray{
    X &\mapsto & C^\infty(X)
    \\
    {}^{\mathllap{ f }}\big\downarrow
      &&
    \big\uparrow^{\mathrlap{ f^\ast : \phi \mapsto \phi \circ f }}
    \\
    Y &\mapsto& C^\infty(Y)
  }
\end{displaymath}
The statement of \emph{[[Milnor's exercise]]} is that this this is a [[fully faithful functor]], hence exhibiting a [[full subcategory]]-inclusion (Def. \ref{FullyFaithfulFunctor}):

\begin{displaymath}
SmthMfd
   \overset{\phantom{AAAA}}{
     \hookrightarrow
   }
  Alg_{\mathbb{R}}^{op}
  \,.
\end{displaymath}
These two statements, expressing categories of [[spaces]] as [[full subcategories]] of [[opposite categories]] of categories of [[algebras]], are the starting point for many developments in [[geometry]], such as \emph{[[algebraic geometry]]}, \emph{[[supergeometry]]}, \emph{[[noncommutative geometry]]} and \emph{[[noncommutative topology]]}.

$\,$

Since a [[fully faithful functor]]/[[full subcategory]]-embedding $\mathcal{C} \hookrightarrow \mathcal{D}$ exhibits the [[objects]] of $\mathcal{D}$ as a consistent generalization of the objects of $\mathcal{C}$, one may turn these examples around and \emph{define} more general kinds of [[spaces]] as \emph{[[formal duality|formal duals]]} (Example \ref{OppositeCategory}) to certain [[algebras]]:

$\,$

\textbf{[[infinitesimally thickened points]] and [[formal Cartesian spaces]]}

The [[category]] of \emph{[[infinitesimally thickened points]]} is, by definition, the [[full subcategory]] (Example \ref{FullSubcategoryOnClassOfObjects}) of the [[opposite category]] (Example \ref{OppositeCategory}) of that of [[commutative algebras]] (Example \ref{ExamplesOfConcreteCategories}) over the [[real numbers]]

\begin{displaymath}
\itexarray{
    InfThckPoint
    &\overset{\phantom{AAAA}}{\hookrightarrow}&
    Alg_{\mathbb{R}}^{op}
    \\
    \mathbb{D} &\mapsto& C^\infty(\mathbb{D})
    \\
    &&   \coloneqq \mathbb{R} \oplus V
  }
\end{displaymath}
on those with a unique [[maximal ideal]] $V$ which is a finite-[[dimensional]] as an $\mathbb{R}$-[[vector space]] and a [[nilradical]]: for each $a \in V$ there exists $n \in \mathbb{N}$ such that $a^n = 0$.

The [[category]] of \emph{[[formal Cartesian spaces]]} is, by definition, the [[full subcategory]] (Example \ref{FullSubcategoryOnClassOfObjects}) of the [[opposite category]] (Example \ref{OppositeCategory}) of that of [[commutative algebras]] (Example \ref{ExamplesOfConcreteCategories}) over the [[real numbers]]

\begin{displaymath}
\itexarray{
    FormalCartSp
    &\overset{\phantom{AAAA}}{\hookrightarrow}&
    Alg_{\mathbb{R}}^{op}
    \\
    \mathbb{R}^n \times \mathbb{D}
      &\mapsto&
    C^\infty(\mathbb{R}^n \times \mathbb{D})
    \\
    &&  \coloneqq C^\infty(\mathbb{R}^n) \otimes_{\mathbb{R}}(\mathbb{R} \oplus V)
  }
\end{displaymath}
on those which are [[tensor products of algebras]], of an [[algebra of functions|algebra of]] [[smooth functions]] on a [[Cartesian space]] $\mathbb{R}^n$, for some $n \in \mathbb{Z}$, and the algebra of functions on an [[infinitesimally thickened point]].

Notice that the [[formal Cartesian spaces]] $\mathbb{R}^{n\vert q}$ are fully \emph{defined} by this assignment.

$\,$

\textbf{[[super points]] and [[super Cartesian spaces]]}

The [[category]] of \textbf{[[super points]]} is \emph{by definition}, the [[full subcategory]] (Example \ref{FullSubcategoryOnClassOfObjects}) of the [[opposite category]] (Example \ref{OppositeCategory}) of that of [[supercommutative algebras]] (Example \ref{ExamplesOfConcreteCategories}) over the [[real numbers]]

\begin{displaymath}
\itexarray{
    SuperPoint
     &\overset{\phantom{AAAA}}{\hookrightarrow}&
    sCAlg_{\mathbb{R}}^{op}
    \\
    \mathbb{R}^{0\vert q}
    &\mapsto&
    \Lambda_q
  }
\end{displaymath}
on the [[Grassmann algebras]]:

\begin{displaymath}
\Lambda_q \;\coloneqq\; \mathbb{R}[ \theta_1, \cdots, \theta_q ]/( \theta_i \theta_j = - \theta_j \theta_i )
 \phantom{AAAAA}
  q \in \mathbb{N}
  \,.
\end{displaymath}
More generally, the [[category]] of \textbf{[[super Cartesian spaces]]} is \emph{by definition}, the [[full subcategory]]

\begin{displaymath}
\itexarray{
    SuperCartSp
    &\overset{\phantom{AAAA}}{\hookrightarrow}&
    sCAlg_{\mathbb{R}}^{op}
    \\
    \mathbb{R}^{n\vert q}
    &\mapsto&
    C^\infty(\mathbb{R}^n) \otimes_{\mathbb{R}} \Lambda_q
  }
\end{displaymath}
on the [[tensor product of algebras]], over $\mathbb{R}$ of the [[algebra of functions|algebra of]] [[smooth functions]] on a [[Cartesian space]], and a [[Grassmann algebra]], as above.

Notice that the [[super Cartesian spaces]] $\mathbb{R}^{n\vert q}$ are fully \emph{defined} by this assignment. We discuss this in more detail in the chapter [[geometry of physics -- supergeometry|on supergeometry]].

\end{example}
$\,$

\hypertarget{NaturalTransformationsAndPresheaves}{}\subsubsection*{{Natural transformations and presheaves}}\label{NaturalTransformationsAndPresheaves}

Given a system of ([[homomorphism|homo-]])[[morphisms]] (``transformations'') in some [[category]] (Def. \ref{Categories})

\begin{displaymath}
F_X \overset{\phantom{A}\eta_X\phantom{A}}{\longrightarrow} G_X
\end{displaymath}
between [[objects]] that depend on some [[variable]] $X$, hence that are values of [[functors]] of $X$ (Def. \ref{Functors}), one says that this is \emph{natural}, hence a \emph{[[natural transformation]]} (Def. \ref{NaturalTransformations} below) if it is compatible with ([[homomorphism|homo-]])[[morphisms]] of the variable itself.

These [[natural transformations]] are the evident [[homomorphisms]] between [[functors]]

\begin{displaymath}
F \overset{\phantom{A}\eta\phantom{A}}{\longrightarrow} G
  \,,
\end{displaymath}
and hence there is a \emph{[[category of functors]]} between any two [[categories]] (Example \ref{FunctorCategory} below).

A key class of such [[functor categories]] are those between an [[opposite category]] $\mathcal{C}^{op}$ and the base [[category of sets]], these are also called \emph{[[categories of presheaves]]} (Example \ref{CategoryOfPresheaves} below). It makes good sense (Remark \ref{PresaheavesAsGeneralizedSpaces} below) to think of these as categories of ``generalized objects of $\mathcal{C}$'', a perspective which is made precise by the statement of the \emph{[[Yoneda lemma]]} (Prop. \ref{YonedaLemma} below) and the resulting \emph{[[Yoneda embedding]]} (Prop. \ref{YonedaEmbedding} below). This innocent-looking lemma is the heart that makes [[category theory]] tick.

$\,$

\begin{defn}
\label{NaturalTransformations}\hypertarget{NaturalTransformations}{}
\textbf{([[natural transformation]] and [[natural isomorphism]])}

Given two [[categories]] $\mathcal{C}$ and $\mathcal{D}$ (Def. \ref{Categories}) and given two [[functors]] $F$ and $G$ from $\mathcal{C}$ to $\mathcal{D}$ (Def. \ref{Functors}), then a \emph{[[natural transformation]]} from $F$ to $G$

\begin{displaymath}
\mathcal{C}
    \underoverset
      {\underset{G}{\longrightarrow}}
      {\overset{F}{\longrightarrow}}
      {\phantom{AA}\Downarrow \mathrlap{\eta} \phantom{AA}}
  \mathcal{D}
\end{displaymath}
is

\begin{itemize}%
\item for each [[object]] $X \in Obj_{\mathcal{C}}$ a [[morphism]]

\begin{equation}
F(X) \overset{ \eta_X }{\longrightarrow} G(X)
\label{NaturalTransformationComponent}\end{equation}


\end{itemize}
such that

\begin{itemize}%
\item for each [[morphism]] $X \overset{f}{\longrightarrow} Y$ we have a [[commuting square]] (Def. \ref{CommutingDiagram}) of the form

\begin{equation}
\eta_Y\circ F(X)
   \;=\;
  G(Y)\circ \eta_X
  \phantom{AAAAAA}
  \itexarray{
     F(X) &\overset{\eta_X}{\longrightarrow}& G(X)
     \\
     {}^{\mathllap{F(f)}}\downarrow
    &&
     \downarrow^{\mathrlap{G(f)}}
     \\
     F(Y) &\underset{\eta_Y}{\longrightarrow}& G(Y)
  }
\label{Naturality}\end{equation}
(sometimes called the \emph{naturality square} of the natural transformation).



\end{itemize}
If all the component morphisms $\eta_X$ are [[isomorphisms]] (Def. \ref{Isomorphism}), then the natural transformation $\eta$ is called a \emph{[[natural isomorphism]]}.

For

\begin{displaymath}
\mathcal{C}
    \underoverset
      {\underset{G}{\longrightarrow}}
      {\overset{F}{\longrightarrow}}
      {\phantom{AA}\Downarrow \mathrlap{\eta} \phantom{AA}}
  \mathcal{D}
  \phantom{AA}
  \text{and}
  \phantom{AA}
  \mathcal{C}
    \underoverset
      {\underset{H}{\longrightarrow}}
      {\overset{G}{\longrightarrow}}
      {\phantom{AA}\Downarrow \mathrlap{\rho} \phantom{AA}}
  \mathcal{D}
\end{displaymath}
two [[natural transformations]] as shown, their \emph{[[composition]]} is the natural transformation

\begin{displaymath}
\mathcal{C}
    \underoverset
      {\underset{H}{\longrightarrow}}
      {\overset{F}{\longrightarrow}}
      {\phantom{A}\Downarrow \mathrlap{\rho \circ \eta} \phantom{AAAA}}
  \mathcal{D}
\end{displaymath}
whose components \eqref{NaturalTransformationComponent} are the [[compositions]] of the components of $\eta$ and $\rho$:

\begin{equation}
(\rho \circ \eta)_X
  \;\coloneqq\;
  \rho_{X} \circ \eta_X
  \phantom{AAAAA}
  \itexarray{
     F(X) &\overset{\eta_X}{\longrightarrow}& G(X)
      &\overset{\rho_X}{\longrightarrow}& H(X)
     \\
     {}^{\mathllap{F(f)}}\downarrow
       &&
     \downarrow^{\mathrlap{G(f)}}
       &&
     \downarrow^{\mathrlap{H(f)}}
     \\
     F(Y) &\underset{\eta_Y}{\longrightarrow}& G(Y)
       &\underset{\rho_Y}{\longrightarrow}& H(Y)
  }
\label{NaturalTransformationComposition}\end{equation}
\end{defn}
\begin{example}
\label{ReductionOnFormalCartesianSpace}\hypertarget{ReductionOnFormalCartesianSpace}{}
\textbf{([[reduction modality|reduction]] of [[formal Cartesian spaces]])}

On the [[category]] [[FormalCartSp]] of [[formal Cartesian spaces]] Example \ref{SpacesViaAlgebrasOfFunctions}, consider the [[endofunctor]]

\begin{displaymath}
\itexarray{
    FormalCartSp
      &\overset{ \phantom{AA}\Re \phantom{AA} }{\longrightarrow}&
    FormalCartSp
    \\
    \mathbb{R}^n \times \mathbb{D}
    &\mapsto&
    \mathbb{R}^n
  }
\end{displaymath}
which sends each [[formal Cartesian space]] to the underlying ordinary [[Cartesian space]], forgetting the [[infinitesimally thickened point]]-factor. Moreover, on [[morphisms]] this functor is defined via the [[retraction]]

\begin{displaymath}
\itexarray{
    id \colon
    &
    \mathbb{R}^n
    &\overset{i}{\longrightarrow}&
    \mathbb{R}^n \times \mathbb{D}
    &\overset{r}{\longrightarrow}&
    \mathbb{R}^n
    \\
    &
    C^\infty(\mathbb{R}^n)
    &\underoverset{\text{quotient projection}}{i^\ast}{\longleftarrow}&
    C^\infty(\mathbb{R}^n) \otimes_{\mathbb{R}} (R \oplus V)
    &\underoverset{f \mapsto f \otimes 1}{r^\ast}{\longleftarrow}&
    C^\infty(\mathbb{R}^n)
  }
\end{displaymath}
as

\begin{displaymath}
\itexarray{
     C^\infty(\mathbb{R}^n \times \mathbb{D})
       &\phantom{AAA}&&
     C^\infty(\mathbb{R}^n)
       &\overset{i^\ast}{\longleftarrow}&
     C^\infty( \mathbb{R}^n \times \mathbb{D} )
     \\
     {}^{\mathllap{ f^\ast }}\big\uparrow
       && &
     {}^{ \mathllap{\Re( f^\ast ) \coloneqq i^\ast \circ f^\ast \circ r^\ast } }\big\uparrow
       &&
     \big\uparrow^{ \mathrlap{ f^\ast } }
     \\
     C^\infty(\mathbb{R}^{n'} \times {\mathbb{D}}')
       &&&
     C^\infty(\mathbb{R}^{n'})
       &\overset{r^\ast}{\longrightarrow}&
     C^\infty( \mathbb{R}^{n'}  \times {\mathbb{D}}')
  }
\end{displaymath}
This is indeed functorial due to the fact that any algebra [[homomorphism]] $f^\ast$ needs to send nilpotent elements to nilpotent elements, so that the following identity holds:

\begin{equation}
i^\ast \circ f^\ast
  \;=\;
  i^\ast \circ f^\ast \circ r^\ast \circ i^\ast 
  \,.
\label{ProjectingOutNilpotentsLater}\end{equation}
Then there is a [[natural transformation]] (Def. \ref{NaturalTransformations}) from this functor to the [[identity functor]]

\begin{displaymath}
\Re
    \overset{ \phantom{A} \eta^{\Re} \phantom{A} }{\longrightarrow}
  Id
\end{displaymath}
whose components inject the underlying Cartesian space along the unit point inclusion of the [[infinitesimally thickened point]]:

\begin{displaymath}
\itexarray{
    \Re\left( \mathbb{R}^n \times \mathbb{D} \right)
      \coloneqq
    &
    \mathbb{R}^n
    &\overset{ \phantom{A} \eta^\Re_{\mathbb{R}^n \times \mathbb{D}} }{\longrightarrow}&
    \mathbb{R}^n \times \mathbb{D}
    \\
    &
    C^\infty(\mathbb{R}^n)
    &\overset{i^\ast}{\longleftarrow}&
    C^\infty(\mathbb{R}^n \times \mathbb{D})
    \\
    &
    {}^{ \mathllap{ i^\ast \circ f^\ast \circ r^\ast } }\big\uparrow && \big\uparrow^{\mathrlap{ f^\ast }}
    \\
    &
    C^\infty(\mathbb{R}^{n'})
    &\overset{i^\ast}{\longleftarrow}&
    C^\infty(\mathbb{R}^{n'} \times \mathbb{D}')
  }
\end{displaymath}
The commutativity of this naturality square is again the identity \eqref{ProjectingOutNilpotentsLater}.

\end{example}
\begin{example}
\label{FunctorCategory}\hypertarget{FunctorCategory}{}
\textbf{([[functor category]])}

Let $\mathcal{C}$ and $\mathcal{D}$ be [[categories]] (Def. \ref{Categories}). Then the \emph{[[category of functors]]} between them, to be denoted $[\mathcal{C}, \mathcal{D}]$, is the [[category]] whose [[objects]] are the [[functors]] $\mathcal{C} \overset{F}{\to} \mathcal{D}$ (Def. \ref{Functors}) and whose [[morphisms]] are the [[natural transformations]] $F \overset{\eta}{\Rightarrow} G$ between functors (Def. \ref{NaturalTransformations}) and whose [[composition]] operation is the composition of natural transformations \eqref{NaturalTransformationComposition}.

\end{example}
\begin{example}
\label{CategoryOfPresheaves}\hypertarget{CategoryOfPresheaves}{}
\textbf{([[category of presheaves]])}

Given a [[category]] $\mathcal{C}$ (Def. \ref{Categories}), a [[functor]] (Def. \ref{Functors}) of the form

\begin{displaymath}
F \;\colon\; \mathcal{C}^{op} \longrightarrow Set
  \,,
\end{displaymath}
hence out of the [[opposite category]] of $\mathcal{C}$ (Def. \ref{OppositeCategory}), into the [[category of sets]] (Example \ref{CategoryOfSets}) is also called a \emph{[[presheaf]]} (for reasons discussed below) \emph{on $\mathcal{C}$} or \emph{over $\mathcal{C}$}.

The corresponding [[functor category]] (Example \ref{FunctorCategory})

\begin{displaymath}
PSh(\mathcal{C})
  \;\coloneqq\; [\mathcal{C}^{op}, Set]
\end{displaymath}
is hence called the \emph{[[category of presheaves]]} over $\mathcal{C}$.

\end{example}
\begin{example}
\label{RepresentablePresheaves}\hypertarget{RepresentablePresheaves}{}
\textbf{([[representable presheaves]])}

Given a [[category]] $\mathcal{C}$ (Def. \ref{Categories}), the [[hom-functor]] (Example \ref{HomFunctor}) induces the following [[functor]] (Def. \ref{Functors}) from $\mathcal{C}$ to its [[category of presheaves]] (Def. \ref{CategoryOfPresheaves}):

\begin{equation}
\itexarray{
    y & \colon &
    \mathcal{C}
      &\longrightarrow&
    [\mathcal{C}^{op}, Set]
    \\
    \\
    && && && c_1 &\overset{g}{\longrightarrow}& c_2
    \\
    &&
    X
    &\mapsto&
    Hom_{\mathcal{C}}(-,X)
     &\phantom{AA}\colon\phantom{AA}&
    Hom_{\mathcal{C}}(c_1,X)
      &\overset{Hom_{\mathcal{C}}( g, X ) }{\longleftarrow}&
    Hom_{\mathcal{C}}(c_2, X)
    \\
    &&
    {}^{\mathllap{ f }}\big\downarrow
    &&
    \big\downarrow^{ \mathrlap{ Hom_{\mathcal{C}}(-,f) } }
    &&
    \big\downarrow^{ \mathrlap{ Hom_{\mathcal{C}}( c_1, f )  } }
    &&
    \big\downarrow^{ \mathrlap{ Hom_{\mathcal{C}}(c_2,f) } }
    \\
    &&
    Y &\mapsto&
    Hom_{\mathcal{C}}(-,Y)
      &\phantom{AA}\colon\phantom{AA}&
    Hom_{\mathcal{C}}(c_1,Y)
      &\overset{Hom_{\mathcal{C}}( g, Y ) }{\longleftarrow}&
    Hom_{\mathcal{C}}(c_2, Y)
  }
\label{YonedaFunctor}\end{equation}
The [[presheaves]] $y(X) \coloneqq Hom_{\mathcal{C}}(-,X)$ in the [[image]] of this functor are called the \emph{[[representable presheaves]]} and $X \in Obj_{\mathcal{C}}$ is called their [[representing object]].

The functor \eqref{YonedaFunctor} is also called the \emph{[[Yoneda embedding]]}, due to Prop. \ref{YonedaEmbedding} below.

\end{example}
\begin{remark}
\label{PresaheavesAsGeneralizedSpaces}\hypertarget{PresaheavesAsGeneralizedSpaces}{}
\textbf{([[presheaves]] as [[generalized spaces]])}

If a given [[category]] $\mathcal{C}$ (Def. \ref{Categories}) is thought of as a category of \emph{[[spaces]]} of sorts, as those in Example \ref{SpacesViaAlgebrasOfFunctions}, then it will be most useful to think of the corresponding [[category of presheaves]] $[\mathcal{C}^{op}, Set]$ (Def. \ref{CategoryOfPresheaves}) as a category of \emph{[[generalized spaces]] probe-able by} the test spaces in $\mathcal{C}$ (\href{space+and+quantity#Lawvere86}{Lawvere 86, p. 17}).

Namely, imagine a [[generalized space]] $\mathbf{X}$ which is at least probe-able by spaces in $\mathcal{C}$. This should mean that for each [[object]] $c \in \mathcal{C}$ there is some [[set]] of geometric maps ``$c \to \mathbf{X}$''. Here the quotation marks are to warn us that, \emph{at this point}, $\mathbf{X}$ is not defined yet; and even if it were, it is not expected to be an object of $\mathcal{C}$, so that, at this point, an actual morphism from $c$ to $\mathbf{X}$ is not definable. But we may anyway consider some \emph{abstract set}

\begin{equation}
\mathbf{X}(c)  \; \text{"=}  Hom(c,\mathbf{X})"
\label{WouldBeMapsIntoGeneralizedSpace}\end{equation}
whose elements we do want to think of maps (homomorphisms of spaces) from $c$ to $\mathbf{X}$.

That this is indeed consistent, in that we may actually remove the quotation remarks on the right of \eqref{WouldBeMapsIntoGeneralizedSpace}, is the statement of the \emph{[[Yoneda lemma]]}, which we discuss as Prop. \ref{YonedaLemma} below.

A minimum consistency condition for this to make sense (we will consider further conditions later on when we discuss \emph{[[sheaves]]}) is that we may consistently pre-compose the would-be maps from $c$ to $\mathbf{X}$ with actual morphisms $d \overset{f}{\to} c$ in $\mathcal{C}$. This means that for every such morphism there should be a function between these sets of would-be maps

\begin{displaymath}
\itexarray{
     c && \mathbf{X}(d)
     \\
     {}^{\mathllap{ f }}\big\downarrow
       &&
     \big\uparrow{}^{\mathrlap{ \mathbf{X}(f) \, \text{"=}(-)\circ f\text{"}}}
     \\
     d && \mathbf{X}(c)
  }
\end{displaymath}
which respects composition and identity morphisms. But in summary, this says that what we have defined thereby is actually a \emph{[[presheaf]]} on $\mathcal{C}$ (Def. \ref{CategoryOfPresheaves}), namely a functor

\begin{displaymath}
\mathbf{X} \;\colon\; \mathcal{C}^{op} \longrightarrow Set
  \,.
\end{displaymath}
For consistency of regarding this presheaf as a \emph{presheaf of sets of plots of a generalized space}, it ought to be true that every ``ordinary space'', hence every [[object]] $X \in \mathcal{C}$, is also an example of a ``generalized space probe-able by'' object of $\mathcal{C}$, since, after all, these are the spaces which may manifestly be probed by objects $c \in \mathcal{C}$, in that morphisms $c \to X$ are already defined.

Hence the incarnation of $X \in \mathcal{C}$ as a generalized space probe-able by objects of $\mathcal{C}$ should be the presheaf $Hom_{\mathcal{C}}(-,X)$, hence the [[representable presheaf|presheaf represented]] by $X$ (Example \ref{RepresentablePresheaves}), via the Yoneda functor \eqref{YonedaFunctor}.

At this point, however, a serious consistency condition arises: The ``ordinary spaces'' now exist as objects of two different categories: on the one hand there is the original $X \in \mathcal{C}$, on the other hand there is its Yoneda image $y(X) \in [\mathcal{C}^{op}, Set]$ in the category of generalized spaces. Hence we need to know that these two perspectives are compatible, notably that maps $X \to Y$ between ordinary spaces are the same whether viewed in $\mathcal{C}$ or in the more general context of $[\mathcal{C}^{op}, Set]$.

That this, too, holds true, is the statement of the \emph{[[Yoneda embedding]]}, which we discuss as Prop. \ref{YonedaEmbedding} below.

Eventually one will want to impose one more consistency condition, namely that plots are determined by their \emph{local behaviour}. This is the \emph{[[sheaf|sheaf condition]]} (Def. \ref{Sheaf} below) and is what leads over from [[category theory]] to [[topos theory]] \hyperlink{BasicNotionsOfToposTheory}{below}.

\end{remark}
\begin{prop}
\label{YonedaLemma}\hypertarget{YonedaLemma}{}
\textbf{([[Yoneda lemma]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}), $X \in \mathcal{C}$ any object, and $\mathbf{Y} \in [\mathcal{C}^{op}, Set]$ a [[presheaf]] over $\mathcal{C}$ (Def. \ref{CategoryOfPresheaves}).

Then there is a [[bijection]]

\begin{displaymath}
\itexarray{
    Hom_{[\mathcal{C}^{op},Set]}( y(X), \mathbf(Y) )
      &\overset{\simeq}{\longrightarrow}&
    \mathbf{Y}(X)
    \\
    \eta
      &\mapsto&
    \eta_X(id_X)
  }
\end{displaymath}
between the [[hom-set]] of the [[category of presheaves]] from the [[representable presheaf|presheaf represented]] by $X$ \eqref{YonedaFunctor} to $\mathbf{Y}$, and the set which is assigned by $\mathbf{Y}$ to $X$.

\end{prop}
\begin{proof}
By Example \ref{FunctorCategory}, an element in the set on the left is a [[natural transformation]] (Def. \ref{NaturalTransformations}) of the form

\begin{displaymath}
\mathcal{C}^{op}
    \underoverset
      {\underset{\mathbf{Y}}{\longrightarrow}}
      {\overset{y(X)}{\longrightarrow}}
      {\phantom{AA} \Downarrow \mathrlap{\eta}  \phantom{AA}}
  Set
\end{displaymath}
hence given by component functions \eqref{NaturalTransformationComponent}

\begin{displaymath}
Hom_{\mathcal{C}}(c,X)
    \overset{\eta_c}{\longrightarrow}
  \mathbf{Y}(X)
\end{displaymath}
for each $c \in \mathcal{C}$. In particular there is the component at $c = X$

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{C}}(X,X)
      &\overset{\eta_X}{\longrightarrow}&
    \mathbf{Y}(X)
    \\
    id_X &\mapsto& \eta_X(id_X)
  }
\end{displaymath}
and the [[identity morphism]] $id_X$ on $X$ is a canonical element in the set on the left. The statement to be proven is hence equivalently that for every element in $\mathbf{Y}(X)$ there is precisely one $\eta$ such that this element equals $\eta_X(id_X)$.

Now the condition to be satisfied by $\eta$ is that it makes its [[naturality squares]] \eqref{Naturality} commute (Def. \ref{CommutingDiagram}). This includes those of the form

\begin{displaymath}
\itexarray{
    id_X
    \in
    &
    Hom_{\mathcal{C}}(X,X)
      &\overset{\eta_X}{\longrightarrow}&
    \mathbf{Y}(X)
    \\
    &
    {}^{\mathllap{ Hom_{\mathcal{C}}(f,X) }}
    \big\downarrow
      &&
    \big\downarrow{}^{\mathrlap{\mathbf{Y}(f)}}
    \\
    &
    Hom_{\mathcal{C}}(Y,X)
    &\underset{\eta_Y}{\longrightarrow}&
    \mathbf{Y}(Y)
  }
  \phantom{AAAA}
  \itexarray{
     \{id_X\}
     &\longrightarrow&
     \{\eta_X(id_X)\}
     \\
     \big\downarrow
     &&
     \big\downarrow
     \\
     \{f\}
     &\longrightarrow&
     \big\{ \eta_Y(F) = \mathbf{Y}(f)( \eta_X(id_X) ) \big\}
  }
\end{displaymath}
for any [[morphism]]

\begin{displaymath}
(Y \overset{f}{\longrightarrow} X)
    \;\in\;
  Hom_{\mathcal{C}}(Y,X)
  \,.
\end{displaymath}
As the diagram chase of elements on the right shows, this commutativity (Def. \ref{CommutingDiagram}) fixes $\eta_Y(f)$ for all $Y \in \mathcal{C}$ and all $f \in Hom_{\mathcal{C}}(Y,X)$ uniquely in terms of the element $\eta_{X}(id_X)$.

It remains only to see that there is no condition on the element $\eta_X(id_X)$, hence that with $\eta_Y(f)$ defined this way, the commutativity of all the remaining naturality squares is implies: The general naturality square for a morphism $Y_2 \overset{g}{\longrightarrow} Y_1$ is of the form

\begin{displaymath}
\itexarray{
    &
    Hom_{\mathcal{C}}(Y_1,X)
      &\overset{\eta_{Y_1}}{\longrightarrow}&
    \mathbf{Y}(Y_1)
    \\
    &
    {}^{\mathllap{ Hom_{\mathcal{C}}(g,X) }}
    \big\downarrow
      &&
    \big\downarrow{}^{\mathrlap{\mathbf{Y}(g)}}
    \\
    &
    Hom_{\mathcal{C}}(Y_2,X)
    &\underset{\eta_{Y_2}}{\longrightarrow}&
    \mathbf{Y}(Y_2)
  }
  \phantom{AAAA}
  \itexarray{
     \{f_1\}
     &\longrightarrow&
     \{ \mathbf{Y}(f_1)( \eta_X(id_X) )  \}
     \\
     \big\downarrow
     &&
     \big\downarrow
     \\
     \{f_2 = f_1\circ g\}
     &\longrightarrow&
     \{\mathbf{Y}(f_2)( \eta_X(id_X) ) = \mathbf{Y}(g) \circ \mathbf{Y}(f_1) ( \eta_X(id_X) ) \}
  }
\end{displaymath}
As shown on the right, the commutativity of this diagram now follows from the [[functor|functoriality]] $\mathbf{Y}(f_2) = \mathbf{Y}(f_1 \circ g)$ of the [[presheaf]] $\mathbf{Y}$.

\end{proof}
As a direct corollary, we obtain the statement of the [[Yoneda embedding]]:

\begin{prop}
\label{YonedaEmbedding}\hypertarget{YonedaEmbedding}{}
\textbf{([[Yoneda embedding]])}

The assignment \eqref{YonedaFunctor} of [[representable presheaves|represented presheaves]] (Example \ref{RepresentablePresheaves}) is a [[fully faithful functor]] (Def. \ref{FullyFaithfulFunctor}), hence exhibits a [[full subcategory]] inclusion

\begin{displaymath}
y
  \;\;\colon\;\;
  \itexarray{
    \mathcal{C}
      &\overset{\phantom{AAAA}}{\hookrightarrow}&
    [\mathcal{C}^{op}, Set]
    \\
    X
    &\mapsto&
    Hom_{\mathcal{C}}(-,X)
  }
\end{displaymath}
of the given [[category]] $\mathcal{C}$ into its [[category of presheaves]].

\end{prop}
\begin{proof}
We need to show that for all $X_1, X_2 \in Obj_{\mathcal{C}}$ the function

\begin{equation}
\itexarray{
    Hom_{\mathcal{C}}(X_1, X_2)
      &\overset{ }{\longrightarrow}&
    Hom_{[\mathcal{C}^{op}, Set]}
    \big(
      Hom_{\mathcal{C}}(-,X_1)
       \;,\;
      Hom_{\mathcal{C}}(-,X_2)
    \big)
    \\
    f
      &\mapsto&
    Hom_{\mathcal{C}}(-,f)
  }
\label{HomFunctionForYonedaEmbedding}\end{equation}
is a [[bijection]]. But the [[Yoneda lemma]] (Prop. \ref{YonedaLemma}) states a bijection the other way around

\begin{displaymath}
\itexarray{
    Hom_{[\mathcal{C}^{op}, Set]}
    \big(
      Hom_{\mathcal{C}}(-,X_1)
       \;,\;
      Hom_{\mathcal{C}}(-,X_2)
    \big)
      &\overset{\simeq}{\longrightarrow}&
    Hom_{\mathcal{C}}(-,X_2)(X_1)
      &=&
    Hom_{\mathcal{C}}(X_1, X_2)
    \\
    \eta && \mapsto && \eta_{X_1}( id_{X_1} )
    \\
    Hom_{\mathcal{C}}(-,f)
      && \mapsto &&
    Hom_{\mathcal{C}}(X_1,f)(id_{X_1}) = f
   }
\end{displaymath}
and hence it is sufficient to see that this is a [[left inverse]] to \eqref{HomFunctionForYonedaEmbedding}. This follows by inspection, as shown in the third line above.

\end{proof}
As a direct corollary we obtain the following alternative characterization of [[isomorphisms]], to be compared with the definition of [[epimorphisms]]/[[monomorphisms]] in Def. \ref{Monomorphism}:

\begin{example}
\label{YonedaCharacterizationOfIsomorphism}\hypertarget{YonedaCharacterizationOfIsomorphism}{}
\textbf{([[isomorphism]] via [[bijection]] of [[hom-sets]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}), let $X, Y \in Obj_{X}$ be a [[pair]] of [[objects]], and let $X \overset{f}{\to} Y \;\; \in Hom_{\mathcal{C}}(X,Y)$ be a [[morphism]] between them. Then the following are equivalent:

\begin{enumerate}%
\item $X \overset{f}{\to} Y$ is an [[isomorphism]] (Def. \ref{Isomorphism}),


\item the [[hom-functors]] into and out of $f$ take values in [[bijections]] of [[hom-sets]]: i.e. for all [[objects]] $A \in Obj_{\mathcal{C}}$, we have

\begin{displaymath}
Hom_{\mathcal{C}}(A,f)
  \;\colon\;
  Hom_{\mathcal{C}}(A,X) 
    \overset{\simeq}{\longrightarrow}
  Hom_{\mathcal{C}}(A,Y)
\end{displaymath}
and

\begin{displaymath}
Hom_{\mathcal{C}}(f,A)
  \;\colon\;
  Hom_{\mathcal{C}}(Y,A) 
    \overset{\simeq}{\longrightarrow}
  Hom_{\mathcal{C}}(X,A)
\end{displaymath}


\end{enumerate}
\end{example}
$\,$

\hypertarget{Adjunctions}{}\subsubsection*{{Adjunctions}}\label{Adjunctions}

The concepts of [[categories]], [[functors]] and [[natural transformations]] constiture the ``language of categories''. This language now allows to formulate the concept of \emph{[[adjoint functors]]} (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}) and more generally that of \emph{[[adjunctions]]} (Def. \ref{AdjunctionInA2Category} below. This is concept that [[category theory]], as a theory, is all about.

Part of the data involved in an [[adjunction]] is its \emph{[[adjunction unit]]} and \emph{[[adjunction counit]]} (Def. \ref{AdjunctionUnitFromHomIsomorphism} below) and depending on their behaviour special cases of [[adjunctions]] are identified (Prop. \ref{FullyFaithfulAndInvertibleAdjoints} below), which we discuss in detail in following sections:

\newline | | | $\phantom{A}$[[coreflective subcategory|coreflection]]$\phantom{A}$  $\phantom{A}$Def. \ref{ReflectiveSubcategory}$\phantom{A}$ | | $\phantom{A}$[[adjunction counit|counit]] is [[isomorphism|iso]]:$\phantom{A}$ | $\phantom{A}$[[reflective subcategory|reflection]]$\phantom{A}$  $\phantom{A}$Def. \ref{ReflectiveSubcategory} | $\phantom{A}$[[adjoint equivalence of categories|adjoint equivalence]]$\phantom{A}$  $\phantom{A}$Def. \ref{AdjointEquivalenceOfCategories}$\phantom{A}$ |

We now discuss four equivalent definitions of [[adjoint functors]]:

\begin{enumerate}%
\item via hom-isomorphism (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets} below);


\item via [[adjunction unit]] and -[[adjunction counit|counit]] satisfying [[triangle identities]] (Prop. \ref{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat});


\item via [[representing objects]] (Prop. \ref{AdjointFunctorFromObjectwiseRepresentingObject});


\item via [[universal morphisms]] (Prop. \ref{CollectionOfUniversalArrowsEquivalentToAdjointFunctor} below).



\end{enumerate}
Then we discuss some key properties:

\begin{enumerate}%
\item uniqueness of adjoints (Prop. \ref{UniquenessOfAdjoints} below),


\item epi/mono/iso-characterization of adjunction (co-)units (Prop. \ref{FullyFaithfulAndInvertibleAdjoints} below).



\end{enumerate}
$\,$

\begin{defn}
\label{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}\hypertarget{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}{}
\textbf{([[adjoint functors]])}

Let $\mathcal{C}$ and $\mathcal{D}$ be two [[categories]] (Def. \ref{Categories}), and let

\begin{displaymath}
\mathcal{D}
    \underoverset
      {\underset{R}{\longrightarrow}}{\overset{L}{\longleftarrow}}{}
  \mathcal{C}
\end{displaymath}
be a [[pair]] of [[functors]] between them (Def. \ref{Functors}), as shown. Then this is called a \emph{pair of [[adjoint functors]]} (or an \emph{[[adjoint pair]] of [[functors]]}) with $L$ \emph{[[left adjoint]]} and $R$ \emph{[[right adjoint]]}, denoted

\begin{displaymath}
\mathcal{D}
    \underoverset
      {\underset{R}{\longrightarrow}}{\overset{L}{\longleftarrow}}{\bot}
  \mathcal{C}
\end{displaymath}
if there exists a [[natural isomorphism]] (Def. \ref{NaturalTransformations}) between the [[hom-functors]] (Example \ref{HomFunctor}) of the following form:

\begin{equation}
Hom_{\mathcal{D}}(L(-),-) \;\simeq\; Hom_{\mathcal{C}}(-,R(-))
  \,.
\label{HomIsomorphismForAdjointFunctors}\end{equation}
This means that for all [[objects]] $c \in \mathcal{C}$ and $d \in \mathcal{D}$ there is a [[bijection]] of [[hom-sets]]

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{D}}(L(c),d)
      &\overset{\simeq}{\longrightarrow}&
    Hom_{\mathcal{C}}(c,R(d))
    \\
    ( L(c) \overset{f}{\to} d )
    &\mapsto&
    (c \overset{\widetilde f}{\to} R(d))
  }
\end{displaymath}
which is [[natural bijection|natural]] in $c$ and $d$. This isomorphism is called the \emph{adjunction hom-isomorphism} and the [[image]] $\widetilde f$ of amorphism $f$ under this bijections is called the \emph{[[adjunct]]} of $f$. Conversely, $f$ is called the \emph{[[adjunct]]} of $\widetilde f$.

Naturality here means that for every [[morphism]] $g \colon c_2 \to c_1$ in $\mathcal{C}$ and for every [[morphisms]] $h\colon d_1\to d_2$ in $\mathcal{D}$, the resulting square

\begin{equation}
\itexarray{
    Hom_{\mathcal{D}}(L(c_1), d_1)
      &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}(c_1, R(d_1))
    \\
    {}^{\mathllap{Hom_{\mathcal{D}}(L(g), h)}}\big\downarrow
     &&
    \big\downarrow^{\mathrlap{Hom_{\mathcal{C}}(g, R(h))}}
    \\
    Hom_{\mathcal{D}}(L(c_2),d_2)
    &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}(c_2,R(d_2))
  }
\label{NaturalitySquareForAdjointnessOfFunctors}\end{equation}
[[commuting square|commutes]] (Def. \ref{CommutingDiagram}), where the vertical morphisms are given by the [[hom-functor]] (Example \ref{HomFunctor}).

Explicitly, this commutativity, in turn, means that for every morphism $f \;\colon\; L(c_1) \to d_1$ with [[adjunct]] $\widetilde f \;\colon\; c_1 \to R(d_1)$, the adjunct of the [[composition]] is

\begin{displaymath}
\widetilde{
  \itexarray{
    L(c_1) &\overset{f}{\longrightarrow}& d_1
    \\
    {}^{\mathllap{L(g)}}\big\uparrow && \big\downarrow^{\mathrlap{h}}
    \\
    L(c_2) && d_2
  }
  }
  \;\;\;=\;\;\;
  \itexarray{
    c_1 &\overset{\widetilde f}{\longrightarrow}& R(d_1)
    \\
    {}^{\mathllap{g}}\big\uparrow && \big\downarrow^{\mathrlap{R(h)}}
    \\
    c_2 && R(d_2)
  }
\end{displaymath}
\end{defn}
\begin{defn}
\label{AdjunctionUnitFromHomIsomorphism}\hypertarget{AdjunctionUnitFromHomIsomorphism}{}
\textbf{([[adjunction unit]] and [[adjunction counit|counit]])}

Given a pair of [[adjoint functors]]

\begin{displaymath}
\mathcal{C}
    \underoverset
      {\underset{R}{\longrightarrow}}{\overset{L}{\longleftarrow}}{\bot}
  \mathcal{D}
\end{displaymath}
according to Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}, one says that

\begin{enumerate}%
\item for any $c \in \mathcal{C}$ the [[adjunct]] of the [[identity morphism]] on $L(c)$ is the \emph{[[unit of an adjunction|unit morphism]]} of the adjunction at that object, denoted

\begin{displaymath}
\eta_c \coloneqq \widetilde{id_{L(c)}} \;\colon\; c \longrightarrow R(L(c))
\end{displaymath}

\item for any $d \in \mathcal{D}$ the [[adjunct]] of the [[identity morphism]] on $R(d)$ is the \emph{[[counit of an adjunction|counit morphism]]} of the adjunction at that object, denoted

\begin{displaymath}
\epsilon_d \;\colon\; L(R(d)) \longrightarrow d
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{remark}
\label{AdjointTriples}\hypertarget{AdjointTriples}{}
\textbf{([[adjoint triples]])}

It happens that there are subsequence [[adjoint functors]]:

If two functors are [[adjoint functors|adjoint]] to each other as in Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}, we also say that we have an \emph{[[adjoint pair]]}:

\begin{displaymath}
L \;\dashv\; R
  \,.
\end{displaymath}
If one of these has yet another adjoint in the other direction, we speak of an \emph{[[adjoint triple]]}

\begin{equation}
L \;\dashv\; C \;\dashv\; R
  \,.
\label{AdjointTriple}\end{equation}
Below in Example \ref{AdjunctionofAdjunction} we identify adjoint triples as \emph{adjunctions of adjunctions}.

Similarly there are [[adjoint quadruples]], etc.

Notice that in the case of an [[adjoint triple]] \eqref{AdjointTriple}, the [[adjunction unit]] of $C \dashv R$ and the [[adjunction counit]] of $L \dashv R$ (Def. \ref{AdjunctionUnitFromHomIsomorphism}) provide, for each object $X$ in the [[domain]] of $C$, a [[diagram]]

\begin{equation}
L(C(X))
   \overset{ \phantom{AA} \epsilon_X \phantom{AA} }{\longrightarrow}
  X
    \overset{ \phantom{AA} \eta_X \phantom{AA} }{\longrightarrow}
  R(C(X))
\label{OppositeExtremesAdjointTriple}\end{equation}
which is usefully thought of as exhibiting the nature of $X$ as being in between two \emph{opposite extreme aspects} $L(C(X))$ and $R(C(X))$ of $X$. This is illustrated by the following examples, and formalized by the concept of \emph{[[modalities]]} that we turn to in Def. \ref{ModalOperator} below.

\end{remark}
\begin{example}
\label{FloorAndCeilingAsAdjointFunctors}\hypertarget{FloorAndCeilingAsAdjointFunctors}{}
\textbf{([[floor]] and [[ceiling]] as [[adjoint functors]])}

Consider the canonical inclusion

\begin{displaymath}
\mathbb{Z}_{\leq}
    \overset{\phantom{AA}\iota \phantom{AA}}{\hookrightarrow}
  \mathbb{R}_{\leq}
\end{displaymath}
of the [[integers]] into the [[real numbers]], both regarded as [[preorders]] in the standard way (``lower or equal''). Regarded as [[full subcategory]]-inclusion (Def. \ref{FullyFaithfulFunctor}) of the corresponding [[thin categories]], via Example \ref{PartiallyOrderedSetsAsSmallCategories}, this inclusion functor has both a left and right [[adjoint functor]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}):

\begin{itemize}%
\item the [[left adjoint]] to $\iota$ is the [[ceiling function]];


\item the [[right adjoint]] to $\iota$ is the [[floor function]];



\end{itemize}
forming an [[adjoint triple]] (Def. \ref{AdjointTriples})

\begin{equation}
\lceil(-)\rceil \;\;\dashv\;\; \iota \;\;\dashv\;\; \lfloor (-) \rfloor
  \,.
\label{FloorCeilingAdjointTriple}\end{equation}
The [[adjunction unit]] and [[adjunction counit]] express that each real number is in between its ``opposite extreme integer aspects'' \eqref{OppositeExtremesAdjointTriple} given by floor and ceiling

\begin{displaymath}
\iota \lfloor x \rfloor \;\overset{\epsilon_X}{\leq}\; x \;\overset{\eta_x}{\leq}\; \iota \lceil x \rceil
  \,.
\end{displaymath}
\end{example}
\begin{proof}
First of all, observe that we indeed have [[functors]] (Def. \ref{Functors})

\begin{displaymath}
\lfloor(-)\rfloor \;,\;
  \lceil(-)\rceil
  \;\;\colon\;
  \mathbb{R}
    \longrightarrow
  \mathbb{Z}
\end{displaymath}
since floor and ceiling preserve the ordering relation.

Now in view of the identification of [[preorders]] with [[thin categories]] in Example \ref{PartiallyOrderedSetsAsSmallCategories}, the hom-isomorphism \eqref{HomIsomorphismForAdjointFunctors} defining [[adjoint functors]] of the form $\iota \dashv \lfloor(-)\rfloor$ says for all $n \in \mathbb{Z}$ and $x \in \mathbb{R}$, that we have

\begin{displaymath}
\underset{ \in \mathbb{Z}}{\underbrace{n \leq \lfloor x \rfloor}}
  \;\Leftrightarrow\;
  \underset{ \in \mathbb{R}}{\underbrace{n \leq x }}
  \,.
\end{displaymath}
This is clearly already the defining condition on the [[floor]] function $\lfloor x \rfloor$.

Similarly, the hom-isomorphism defining [[adjoint functors]] of the form $\lceil(-)\rceil \dashv \iota$ says that for all $n \in \mathbb{Z}$ and $x \in \mathbb{R}$, we have

\begin{displaymath}
\underset{ \in \mathbb{Z}}{\underbrace{\lceil x \rceil \leq n}}
  \;\Leftrightarrow\;
  \underset{ \in \mathbb{R}}{\underbrace{x \leq n }}
  \,.
\end{displaymath}
This is evidently already the defining condition on the [[floor]] function $\lfloor x \rfloor$.

Notice that in both cases the condition of a \emph{[[natural isomorphism]]} in both variables, as required for an [[adjunction]], is automatically satisfied: For let $x \leq x'$ and $n' \leq n$, then naturality as in \eqref{NaturalitySquareForAdjointnessOfFunctors} means, again in view of the identifications in Example \ref{PartiallyOrderedSetsAsSmallCategories}, that

\begin{displaymath}
\itexarray{
    (n \leq \lfloor x \rfloor) &\Leftrightarrow& (n \leq x)
    \\
    \Downarrow && \Downarrow
    \\
    (n' \leq \lfloor x' \rfloor) &\Leftrightarrow& (n' \leq x')
    \\
    \\
    \in \mathbb{Z} && \in \mathbb{R}
  }
\end{displaymath}
Here the logical implications are equivalently functions between [[sets]] that are either [[empty set|empty]] or [[singletons]]. But Functions between such sets are unique, when they exist.

\end{proof}
\begin{example}
\label{DiscreteTopologicalSpaces}\hypertarget{DiscreteTopologicalSpaces}{}
\textbf{([[discrete topological space|discrete]] and [[codiscrete topological spaces]])}

Consider the ``[[forgetful functor]]'' $Top \overset{U}{\longrightarrow} Set$ from the [[category]] [[Top]] of [[topological spaces]] (Example \ref{ExamplesOfConcreteCategories}) to the [[category of sets]] (Def. \ref{CategoryOfSets}) which sends every [[topological space]] to its underlying [[set]].

This has

\begin{itemize}%
\item a [[left adjoint]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}) $Disc$ which equips a set with its [[discrete topology]],


\item a [[right adjoint]] $coDisc$ which equips a set with the [[codiscrete topology]].



\end{itemize}
These hence form an [[adjoint triple]] (Remark \ref{AdjointTriples})

\begin{displaymath}
Disc
  \;\dashv\;
  U
  \;\dashv\;
  coDisc
  \,.
\end{displaymath}
Hence the [[adjunction unit]] of $Disc \dashv U$ and the [[adjunction counit]] of $U \dashv coDisc$ exhibit every [[topological space|topology]] on a given set as ``in between the opposite extremes'' \eqref{OppositeExtremesAdjointTriple} of the discrete and the co-discrete

\begin{displaymath}
Disc(U(X))
    \overset{\epsilon}{\longrightarrow}
  X
    \overset{\eta}{\longrightarrow}
  coDisc(U(X))
  \,.
\end{displaymath}
\end{example}
\begin{lemma}
\label{ReExpressingMiddleFunctorInAdjointTriple}\hypertarget{ReExpressingMiddleFunctorInAdjointTriple}{}
\textbf{(pre/post-[[composition]] with ([[adjunction counit|co-]])[[adjunction unit|unit]] followed by [[adjunct]] is [[adjoint functor]])}

If a [[functor]] $C$ is a [[right adjoint]]

\begin{displaymath}
L \dashv C
  \;\;\colon\;\;
  \mathcal{C}
    \itexarray{
      \overset{\phantom{AA} L \phantom{AA} }{\longleftarrow}
      \\
      \underset{\phantom{AA} C \phantom{AA} }{\longrightarrow}
    }
  \mathcal{D}
\end{displaymath}
of a [[adjoint pair|pair]] of [[adjoint functors]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}), then application of the [[functor]] $C$ on any [[morphism]] $X \overset{f}{\to} Y \;\;\in \mathcal{C}$ is equal the joint operation of [[composition|pre-composition]] with the $(L \dashv C)$-[[adjunction counit]] $\epsilon^\flat_{X}$ (Def. \ref{AdjunctionUnitFromHomIsomorphism}), followed by passing to the $(L \dashv C)$-[[adjunct]]:

\begin{displaymath}
\widetilde{\eta^\sharp_{Y} \circ (-)}
  \;=\;
  C_{X, Y}
\end{displaymath}
Dually, if $C$ is a [[left adjoint]]

\begin{displaymath}
C \dashv R
  \;\;\colon\;\;
  \mathcal{C}
    \itexarray{
      \overset{\phantom{AA} C \phantom{AA} }{\longrightarrow}
      \\
      \underset{\phantom{AA} R \phantom{AA} }{\longleftarrow}
    }
  \mathcal{D}
\end{displaymath}
then its action on any [[morphism]] $X \overset{f}{\to} Y \;\;\in \mathcal{C}$ equals the joint operation of [[composition|post-composition]] with the $(C \dashv R)$-[[adjunction unit]] $\eta^{ \sharp }_{Y}$ (Def. \ref{AdjunctionUnitFromHomIsomorphism}), followed by passing to the $(C \dashv R)$-[[adjunct]]:

\begin{displaymath}
C_{X, Y}
  \;=\;
  \widetilde{ (-) \circ \epsilon^\flat_{X} }
  \,.
\end{displaymath}
In particular, if $C$ is the middle functor in an [[adjoint triple]] (Remark \ref{AdjointTriples})

\begin{displaymath}
L \dashv C \dashv R
  \;\;\colon\;\;
  \mathcal{C}
    \itexarray{
      \overset{\phantom{AA} L \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AAA} C \phantom{AAA} }{\longrightarrow}
      \\
      \overset{\phantom{AA} R \phantom{AA} }{\longleftarrow}
    }
  \mathcal{D}
\end{displaymath}
then these two operations coincide:

\begin{equation}
\widetilde{\eta^\sharp_{Y} \circ (-)}
  \;=\;
  C_{X, Y}
  \;=\;
  \widetilde{ (-) \circ \epsilon^\flat_{X} }
  \,.
\label{PostcompositionWithEtaAsGamma}\end{equation}
\end{lemma}
\begin{proof}
For the first equality, consider the following [[naturality square]] \eqref{Naturality} for the adjunction hom-isomorphism \eqref{HomIsomorphismForAdjointFunctors}:

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{D}}( C Y , C Y )
    &\overset{\widetilde {(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}( Y, R C Y )
    \\
    {}^{\mathllap{ Hom_{\mathcal{D}}(C(f), C Y) }}
    \big\downarrow
    &&
    \!\!\!\!\!
    \big\downarrow^{\mathrlap{ Hom_{\mathcal{C}}( f, R C Y ) }}
    \\
    Hom_{\mathcal{D}}( C X, C Y )
    &\overset{\widetilde{ (-) }}{\longleftarrow}&
    Hom_{\mathcal{C}}( X, R C Y )
  }
  \phantom{AAAAA}
  \itexarray{
    \{ C Y \overset{id_{C Y}}{\to} C Y\}
    &\longrightarrow&
    \{ Y \overset{\eta^\sharp_{Y}}{\to} R C Y \}
    \\
    \big\downarrow
    &&
    \big\downarrow
    \\
    \{ C X \overset{C(f)}{\to} C Y \}
    &\longleftarrow&
    \{ X \overset{\eta^\sharp_{Y} \circ f}{\longrightarrow} R C Y \}
  }
\end{displaymath}
Chasing the [[identity morphism]] $id_{C Y}$ through this diagram, yields the claimed equality, as shown on the right. Here we use that the right [[adjunct]] of the [[identity morphism]] is the [[adjunction unit]], as shown.

The second equality is [[formal duality|fomally dual]]:

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{D}}( C X, C X)
    &\overset{\widetilde { (-) }}{\longrightarrow}&
    Hom_{\mathcal{C}}( L C X  , X)
    \\
    {}^{\mathllap{ Hom_{\mathcal{D}}( C X, C(f) )  }}
    \big\downarrow
    &&
    \big\downarrow^{ \mathrlap{ Hom_{X}( L C X, f )
} }
    \\
    Hom_{\mathcal{D}}( C X, C Y )
    &\overset{ \widetilde{ (-) } }{\longleftarrow}&
    Hom_{\mathcal{C}    }( L C X, Y )
  }
  \phantom{AAAAA}
  \itexarray{
     \{ C X \overset{id_{C X}}{\to} C X \}
     &\longrightarrow&
     \{ L C X \overset{\epsilon^{\flat}_X}{\to} X \}
     \\
     \big\downarrow
       &&
     \big\downarrow
     \\
     \{ C X \overset{C(f)}{\to} C(Y) \}
     &\longleftarrow& \{ L C X \overset{f\circ \epsilon^\flat_{X}  }{\longrightarrow} Y\}
  }
\end{displaymath}
\end{proof}
$\,$

$\,$

We now consider a \textbf{sequence of equivalent reformulations} of the condition of adjointness.

\begin{prop}
\label{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}\hypertarget{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}{}
\textbf{(general [[adjuncts]] in terms of [[adjunction unit|unit/counit]])}

Consider a pair of [[adjoint functors]]

\begin{displaymath}
\mathcal{C}
    \underoverset
      {\underset{R}{\longrightarrow}}{\overset{L}{\longleftarrow}}{\bot}
  \mathcal{D}
\end{displaymath}
according to Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}, with [[adjunction units]] $\eta_c$ and [[adjunction counits]] $\epsilon_d$ according to Def. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}.

Then

\begin{enumerate}%
\item The [[adjunct]] $\widetilde f$ of any morphism $L(c) \overset{f}{\to} d$ is obtained from $R$ and $\eta_c$ as the [[composition|composite]]

\begin{equation}
\widetilde f
  \;\colon\;
  c
    \overset{\eta_c}{\longrightarrow}
  R(L(c))
    \overset{R(f)}{\longrightarrow}
  R(d)
\label{AdjunctFormula}\end{equation}
Conversely, the [[adjunct]] $f$ of any morphism $c \overset{\widetilde f}{\longrightarrow} R(d)$ is obtained from $L$ and $\epsilon_d$ as

\begin{equation}
f
  \;\colon\;
  L(c)
    \overset{L(\widetilde f)}{\longrightarrow}
  R(L(d))
    \overset{\epsilon_d}{\longrightarrow}
  d
\label{ConverseAdjunctFormula}\end{equation}

\item The [[adjunction units]] $\eta_c$ and [[adjunction counits]] $\epsilon_d$ are components of [[natural transformations]] of the form

\begin{displaymath}
\eta \;\colon\; Id_{\mathcal{C}} \Rightarrow R \circ L
\end{displaymath}
and

\begin{displaymath}
\epsilon \;\colon\; L \circ R \Rightarrow Id_{\mathcal{D}}
\end{displaymath}

\item The [[adjunction unit]] and [[adjunction counit]] satisfy the [[triangle identities]], saying that

\begin{equation}
id_{L(c)}
   \;\colon\;
   L(c)
     \overset{L(\eta_c)}{\longrightarrow}
   L(R(L(c)))
     \overset{\epsilon_{L(c)}}{\longrightarrow}
   L(c)
\label{TriangleIdentities}\end{equation}
and

\begin{displaymath}
id_{R(d)}
  \;\colon\;
  R(d)
    \overset{\eta_{R(d)}}{\longrightarrow}
  R(L(R(d)))
    \overset{R(\epsilon_d)}{\longrightarrow}
  R(d)
\end{displaymath}


\end{enumerate}
\end{prop}
\begin{proof}
For the first statement, consider the [[naturality square]] \eqref{NaturalitySquareForAdjointnessOfFunctors} in the form

\begin{displaymath}
\itexarray{
    id_{L(c)}
     \in
    &
    Hom_{\mathcal{D}}(L(c), L(c))
      &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}(c, R(L(c)))
    \\
    &
    {}^{\mathllap{Hom_{\mathcal{D}}(L(id), f)}}\big\downarrow
     &&
    \big\downarrow^{\mathrlap{Hom_{\mathcal{C}}(id, R(f))}}
    \\
    &
    Hom_{\mathcal{D}}(L(c), d)
    &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}( c, R(d) )
  }
\end{displaymath}
and consider the element $id_{L(c_1)}$ in the top left entry. Its image under going down and then right in the diagram is $\widetilde f$, by Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}. On the other hand, its image under going right and then down is $R(f)\circ \eta_{c}$, by Def. \ref{AdjunctionUnitFromHomIsomorphism}. Commutativity of the diagram means that these two morphisms agree, which is the statement to be shown, for the adjunct of $f$.

The converse formula follows analogously.

The third statement follows directly from this by applying these formulas for the [[adjuncts]] twice and using that the result must be the original morphism:

\begin{displaymath}
\begin{aligned}
    id_{L(c)}
    & =
    \widetilde \widetilde { id_{L(c)} }
    \\
    & = \widetilde{ c \overset{\eta_c}{\to} R(L(c))  }
    \\
    & =
     L(c)
       \overset{L(\eta_c)}{\longrightarrow}
     L(R(L(c)))
       \overset{\epsilon_{L(c)}}{\longrightarrow}
     L(c)
  \end{aligned}
\end{displaymath}
For the second statement, we have to show that for every moprhism $f \colon c_1 \to c_2$ the following [[commuting square|square commutes]]:

\begin{displaymath}
\itexarray{
     c_1 &\overset{f}{\longrightarrow}& c_2
     \\
     {}^{\mathllap{\eta_{c_1}}}\big\downarrow
       &&
     \big\downarrow^{\mathrlap{\eta_{c_2}}}
     \\
     R(L(c_1))
      &\underset{ R(L(f)) }{\longrightarrow}&
     R(L(c_2))
  }
\end{displaymath}
To see this, consider the [[naturality square]] \eqref{NaturalitySquareForAdjointnessOfFunctors} in the form

\begin{displaymath}
\itexarray{
    id_{L(c_2)}
    \in
    & Hom_{\mathcal{D}}(L(c_2), L(c_2))
      &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}(c_2, R(L(c_2)))
    \\
    &
    {}^{\mathllap{Hom_{\mathcal{D}}(L(f),id_{L(c_2)})}}\big\downarrow
     &&
    \big\downarrow^{\mathrlap{Hom_{\mathcal{C}}(f, R(id_{L(c_2)}))}}
    \\
    &
    Hom_{\mathcal{D}}(L(c_1),L(c_2))
      &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}(c_1,R(L(c_1)))
  }
\end{displaymath}
The image of the element $id_{L(c_2)}$ in the top left along the right and down is $f \circ \eta_{c_2}$, by Def. \ref{AdjunctionUnitFromHomIsomorphism}, while its image down and then to the right is $\widetilde {L(f)} = R(L(f)) \circ \eta_{c_1}$, by the previous statement. Commutativity of the diagram means that these two morphisms agree, which is the statement to be shown.

The argument for the naturality of $\epsilon$ is directly analogous.

\end{proof}
\begin{prop}
\label{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat}\hypertarget{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat}{}
\textbf{([[adjoint functors]] equivalent to [[adjunction]] in [[Cat]])}

Two functors

\begin{displaymath}
\mathcal{D}
    \underoverset
      {\underset{R}{\longrightarrow}}{\overset{L}{\longleftarrow}}{}
  \mathcal{C}
\end{displaymath}
are an [[adjoint pair]] in the sense that there is a [[natural isomorphism]] \eqref{HomIsomorphismForAdjointFunctors} according to Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}, precisely if they participate in an \emph{[[adjunction]]} in the [[2-category]] [[Cat]], meaning that

\begin{enumerate}%
\item there exist [[natural transformations]]

\begin{displaymath}
\eta \;\colon\; Id_{\mathcal{C}} \Rightarrow R \circ L
\end{displaymath}
and

\begin{displaymath}
\epsilon \;\colon\; L \circ R \Rightarrow Id_{\mathcal{D}}
\end{displaymath}

\item which satisfy the \emph{[[triangle identities]]}

\begin{displaymath}
id_{L(c)}
   \;\colon\;
   L(c)
     \overset{L(\eta_c)}{\longrightarrow}
   L(R(L(c)))
     \overset{\epsilon_{L(c)}}{\longrightarrow}
   L(c)
\end{displaymath}
and

\begin{displaymath}
id_{R(d)}
  \;\colon\;
  R(d)
    \overset{\eta_{R(d)}}{\longrightarrow}
  R(L(R(d)))
    \overset{R(\epsilon_d)}{\longrightarrow}
  R(d)
\end{displaymath}


\end{enumerate}
\end{prop}
\begin{proof}
That a hom-isomorphism \eqref{HomIsomorphismForAdjointFunctors} implies units/counits satisfying the [[triangle identities]] is the statement of the second two items of Prop. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}.

Hence it remains to show the converse. But the argument is along the same lines as the proof of Prop. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}: We now \emph{define} forming of adjuncts by the formula \eqref{AdjunctFormula}. That the resulting assignment $f \mapsto \widetilde f$ is an [[isomorphism]] follows from the computation

\begin{displaymath}
\begin{aligned}
    \widetilde {\widetilde f}
    & =
    \widetilde{ c \overset{\eta_c}{\to} R(L(c)) \overset{R(f)}{\to} R(d) }
    \\
    & =
    L(c) \overset{L(\eta_c)}{\to} L(R(L(c))) \overset{L(R(f))}{\to} L(R(d)) \overset{\epsilon_d}{\to} d
    \\
    & =
    L(c) \overset{L(\eta_c)}{\to} L(R(L(c)))
         \overset{ \epsilon_{L(c)} }{\to}  L(c)
         \overset{f}{\longrightarrow} d
    \\
    & =  L(c) \overset{f}{\longrightarrow} d
  \end{aligned}
\end{displaymath}
where, after expanding out the definition, we used [[natural transformation|naturality]] of $\epsilon$ and then the [[triangle identity]].

Finally, that this construction satisfies the naturality condition \eqref{NaturalitySquareForAdjointnessOfFunctors} follows from the functoriality of the functors involved, and the naturality of the unit/counit:

\begin{displaymath}
\itexarray{
    c_2 &\overset{ \eta_{c_2} }{\longrightarrow}& R(L(c_2))
    \\
    {}^{\mathllap{g}}\downarrow && \downarrow^{\mathrlap{R(L(g))}}
    & \searrow^{\mathrlap{ R( L(g) \circ f ) }}
    \\
    c_1
      &\overset{\eta_{c_1}}{\longrightarrow}&
    R(L(c_1))
     &\overset{R(f)}{\longrightarrow}&
    R(d_1)
    \\
    && & {}_{R( h\circ f)}\searrow & \downarrow^{\mathrlap{ R(h) }}
    \\
    && && R(d_2)
  }
\end{displaymath}
\end{proof}
The condition \eqref{HomIsomorphismForAdjointFunctors} on adjoint functors $L \dashv R$ in Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets} implies in particular that for every [[object]] $d \in \mathcal{D}$ the functor $Hom_{\mathcal{D}}(L(-),d)$ is a \emph{[[representable functor]]} with \emph{[[representing object]]} $R(d)$. The following Prop. \ref{AdjointFunctorFromObjectwiseRepresentingObject} observes that the existence of such [[representing objects]] for all $d$ is, in fact, already sufficient to imply that there is a right adjoint functor.

This equivalent perspective on adjoint functors makes manifest that adjoint functors are, if they exist, unique up to natural isomorphism, this is Prop. \ref{UniquenessOfAdjoints} below.

\begin{prop}
\label{AdjointFunctorFromObjectwiseRepresentingObject}\hypertarget{AdjointFunctorFromObjectwiseRepresentingObject}{}
\textbf{([[adjoint functor]] from objectwise [[representing objects]])}

A [[functor]] $L \;\colon\; \mathcal{C} \longrightarrow \mathcal{D}$ has a [[right adjoint]] $R \;\colon\; \mathcal{D} \to \mathcal{C}$, according to Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}, already if for all [[objects]] $d \in \mathcal{D}$ there is an object $R(d) \in \mathcal{C}$ such that there is a [[natural isomorphism]]

\begin{displaymath}
Hom_{\mathcal{D}}(L(-),d)
     \underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}
     Hom_{\mathcal{C}}(-,R(d))
     \,,
\end{displaymath}
hence for each [[object]] $c \in \mathcal{C}$ a [[bijection]]

\begin{displaymath}
Hom_{\mathcal{D}}(L(c),d)
     \underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}
     Hom_{\mathcal{C}}(c,R(d))
\end{displaymath}
such that for each [[morphism]] $g \;\colon\; c_2 \to c_1$, the following [[commuting diagram|diagram commutes]]

\begin{equation}
\itexarray{
       Hom_{\mathcal{D}}(L(c_1),d)
         &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
       Hom_{\mathcal{C}}(c_1,R(d))
       \\
       {}^{\mathllap{ Hom_{\mathcal{C}}(L(g),id_d) }}
       \big\downarrow
       &&
       \big\downarrow^{\mathrlap{ Hom_{\mathcal{C}}( f, id_{R(d)}  ) }}
       \\
       Hom_{\mathcal{D}}(L(c_2),d)
         &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
       Hom_{\mathcal{C}}(c_2,R(d))
     }
\label{HalfNaturalitySquareForAdjointnessOfFunctors}\end{equation}
(This is as in \eqref{NaturalitySquareForAdjointnessOfFunctors}, except that only naturality in the first variable is required.)

In this case there is a unique way to extend $R$ from a function on [[objects]] to a function on [[morphisms]] such as to make it a [[functor]] $R \colon \mathcal{D} \to \mathcal{C}$ which is [[right adjoint]] to $L$. , and hence the statement is that with this, naturality in the second variable is already implied.

\end{prop}
\begin{proof}
Notice that

\begin{enumerate}%
\item in the language of [[presheaves]] (Example \ref{CategoryOfPresheaves}) the assumption is that for each $d \in \mathcal{D}$ the presheaf

\begin{displaymath}
Hom_{\mathcal{D}}(L(-),d)
  \;\in\;
  [\mathcal{D}^{op}, Set]
\end{displaymath}
is [[representable functor|represented]] \eqref{YonedaFunctor} by the object $R(d)$, and [[natural transformation|naturally]] so.


\item In terms of the [[Yoneda embedding]] (Prop. \ref{YonedaEmbedding})

\begin{displaymath}
y
    \;\colon\;
  \mathcal{D}
   \hookrightarrow
  [\mathcal{D}^{op}, Set]
\end{displaymath}
we have

\begin{equation}
Hom_{\mathcal{C}}(-,R(d))
  =
  y(R(d))
\label{YonedanotationForRepresentable}\end{equation}


\end{enumerate}
The condition \eqref{NaturalitySquareForAdjointnessOfFunctors} says equivalently that $R$ has to be such that for all [[morphisms]] $h \;\colon\; d_1 \to d_2$ the following diagram in the [[category of presheaves]] $[\mathcal{C}^{op}, Set]$ [[commuting diagram|commutes]]

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{D}}(L(-),d_1)
      &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}(-,R(d_1))
    \\
    {}^{\mathllap{ Hom_{\mathcal{C}}( L(-) , h ) }}
    \big\downarrow
    &&
    \big\downarrow^{\mathrlap{ Hom_{\mathcal{C}}( -, R(h)  ) }}
    \\
    Hom_{\mathcal{D}}(L(-),d_2)
      &\underoverset{\simeq}{\widetilde{(-)}}{\longrightarrow}&
    Hom_{\mathcal{C}}(-, R(d_2))
  }
\end{displaymath}
This manifestly has a unique solution

\begin{displaymath}
y(R(h))
  \;=\;
  Hom_{\mathcal{C}}(-,R(h))
\end{displaymath}
for every morphism $h \colon d_1 \to d_2$ under $y(R(-))$ \eqref{YonedanotationForRepresentable}. But the [[Yoneda embedding]] $y$ is a [[fully faithful functor]] (Prop. \ref{YonedaEmbedding}), which means that thereby also $R(h)$ is uniquely fixed.

\end{proof}
We consider one more equivalent characterization of [[adjunctions]]:

\begin{defn}
\label{UniversalArrow}\hypertarget{UniversalArrow}{}
\textbf{([[universal morphism]])}

Let $\mathcal{C}, \mathcal{D}$ be two [[categories]] (Def. \ref{Categories}) and let $R \;\colon\; \mathcal{D} \to \mathcal{C}$ be a [[functor]] (Def. \ref{Functors})

Then for $c\in \mathcal{C}$ an [[object]], a \emph{[[universal morphism]] from $c$ to $R$} is

\begin{enumerate}%
\item an [[object]] $L(c)\in \mathcal{D}$,


\item a [[morphism]] $\eta_c \;\colon\; c \to R(L(c))$, to be called the \emph{[[adjunction unit|unit]]},



\end{enumerate}
such that for any $d\in \mathcal{D}$, any morphism $f \colon c\to R(d)$ factors through this unit $\eta_c$ as

\begin{equation}
f
  \;=\;
  \eta_c \circ R(\widetilde f)
  \phantom{AAAA}
  \itexarray{
    && c
    \\
    & {}^{\mathllap{\eta_c}}\swarrow && \searrow^{\mathrlap{f}}
    \\
    R(L(c)) &&\underset{R (\widetilde f)}{\longrightarrow}&& R(d)
    \\
    \\
    L(c) &&\underset{ \widetilde f}{\longrightarrow}&& d
  }
\label{UniversalArrowFactorization}\end{equation}
for a \emph{unique} morphism $\widetilde f  \;\colon\; L(c) \longrightarrow d$, to be called the [[adjunct]] of $f$.

\end{defn}
\begin{prop}
\label{CollectionOfUniversalArrowsEquivalentToAdjointFunctor}\hypertarget{CollectionOfUniversalArrowsEquivalentToAdjointFunctor}{}
\textbf{(collection of [[universal morphisms]] equivalent to [[adjoint functor]])}

Let $R \;\colon\; \mathcal{D} \to \mathcal{C}$ be a [[functor]] (Def. \ref{Functors}). Then the following are equivalent:

\begin{enumerate}%
\item $R$ has a [[left adjoint]] functor $L \colon \mathcal{C} \to \mathcal{D}$ according to Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets},


\item For every [[object]] $c \in \mathcal{C}$ there is a [[universal morphism]] $c \overset{\eta_c}{\longrightarrow} R(L(c))$, according to Def. \ref{UniversalArrow}.



\end{enumerate}
\end{prop}
\begin{proof}
In one direction, assume a [[left adjoint]] $L$ is given. Define the would-be universal arrow at $c \in \mathcal{C}$ to be the [[unit of an adjunction|unit of the adjunction]] $\eta_c$ via Def. \ref{AdjunctionUnitFromHomIsomorphism}. Then the statement that this really is a universal arrow is implied by Prop. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}.

In the other direction, assume that universal arrows $\eta_c$ are given. The uniqueness clause in Def. \ref{UniversalArrow} immediately implies [[bijections]]

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{D}}(L(c),d)
      &\overset{\simeq}{\longrightarrow}&
    Hom_{\mathcal{C}}(c,R(d))
    \\
    \left(
      L(c) \overset{\widetilde f}{\to} d
    \right)
      &\mapsto&
    \left(
      c \overset{\eta_c}{\to} R(L(c)) \overset{ R(\widetilde f) }{\to} R(d)
    \right)
  }
\end{displaymath}
Hence to satisfy \eqref{HomIsomorphismForAdjointFunctors} it remains to show that these are [[natural transformation|natural]] in both variables. In fact, by Prop. \ref{AdjointFunctorFromObjectwiseRepresentingObject} it is sufficient to show naturality in the variable $d$. But this is immediate from the functoriality of $R$ applied in \eqref{UniversalArrowFactorization}: For $h \colon d_1 \to d_2$ any [[morphism]], we have

\begin{displaymath}
\itexarray{
    && c
    \\
    & {}^{\mathllap{\eta_c}}\swarrow && \searrow^{\mathrlap{f}}
    \\
    R (L(c)) &&\underset{R (\widetilde f)}{\longrightarrow}&& R(d_1)
    \\
    && {}_{\mathllap{ R( h\circ \widetilde f ) }}\searrow && \downarrow^{\mathrlap{R(h)}}
    \\
    && && R(d_2)
  }
\end{displaymath}
\end{proof}
The following equivalent formulation (Prop. \ref{UniversalMorphismsAreInitialObjectsInCommaCategory}) of [[universal morphisms]] is often useful:

\begin{example}
\label{CommaCategoryWithOneSideConstant}\hypertarget{CommaCategoryWithOneSideConstant}{}
\textbf{([[comma category]])}

Let $\mathcal{C}$ be a [[category]], let $c \in \mathcal{C}$ be any [[object]], and let $F \;\colon\; \mathcal{D} \to \mathcal{C}$ be a [[functor]].

\begin{enumerate}%
\item The \emph{[[comma category]]} $c/F$ is the [[category]] whose [[objects]] are [[pairs]] consisting of an object $d \in \mathcal{D}$ and [[morphisms]] $X \overset{f}{\to} F(d)$ in $\mathcal{C}$, and whose [[morphisms]] $(d_1,X_1,f_1) \to (d_2,X_2,f_2)$ are the [[morphisms]] $X_1 \overset{g}{\longrightarrow} X_2$ in $\mathcal{C}$ that make a commuting triangle (Def. \ref{CommutingDiagram}):

\begin{displaymath}
f_2\circ F(g)
  \;=\;
  f_1
  \phantom{AAAAAA}
  \itexarray{
     X_1 && \overset{\phantom{AA} g \phantom{AA}}{\longrightarrow} && X_2
     \\
     F(X_1)
    &&
    \overset{\phantom{AA} F(g) \phantom{AA}}{\longrightarrow}
    &&
     F(X_2)
     \\
     & {}_{\mathllap{f_1}}\searrow && \swarrow_{\mathrlap{f_2}}
     \\
     && c
  }
\end{displaymath}
There is a canonical [[functor]]

\begin{displaymath}
\itexarray{
    F/c
    &\overset{}{\longrightarrow}&
    \mathcal{D}
  }
  \,.
\end{displaymath}

\item The \emph{[[comma category]]} $F/c$ is the [[category]] whose [[objects]] are [[pairs]] consisting of an [[object]] $d \in \mathcal{D}$ and a [[morphism]] $F(d) \overset{f}{\to} X$ in $\mathcal{C}$, and whose [[morphisms]] $(d_1,X_1,f_1) \to (d_2,X_2,f_2)$ are the [[morphisms]] $X_1 \overset{g}{\longrightarrow} X_2$ in $\mathcal{C}$ that make a commuting triangle (Def. \ref{CommutingDiagram}):

\begin{displaymath}
f_2\circ F(g)
  \;=\;
  f_1
  \phantom{AAAAAA}
  \itexarray{
     && c
     \\
     & {}^{\mathllap{f_1}}\swarrow && \searrow^{\mathrlap{f_2}}
     \\
     F(X_1)
    &&
    \underset{\phantom{AA} F(g) \phantom{AA}}{\longrightarrow}
    &&
     F(X_2)
     \\
     X_1 && \underset{ \phantom{AA} g \phantom{AA} }{\longrightarrow} && X_2
  }
\end{displaymath}
Again, there is a canonical [[functor]]

\begin{equation}
\itexarray{
    c/F
    &\overset{}{\longrightarrow}&
    \mathcal{D}
  }
]
\label{CanonicalFunctorOutOfCommaCategoryOfcOverF}\end{equation}


\end{enumerate}
\end{example}
With this definition, the following is evident:

\begin{prop}
\label{UniversalMorphismsAreInitialObjectsInCommaCategory}\hypertarget{UniversalMorphismsAreInitialObjectsInCommaCategory}{}
\textbf{([[universal morphisms]] are [[initial objects]] in the [[comma category]])}

Let $\mathcal{C} \overset{R}{\longrightarrow} \mathcal{D}$ be a [[functor]] and $d \in \mathcal{D}$ an [[object]]. Then the following are equivalent:

\begin{enumerate}%
\item $d \overset{\eta_d}{\to} R(c)$ is a [[universal morphism]] into $R(c)$ (Def. \ref{UniversalArrow});


\item $(d, \eta_d)$ is the [[initial object]] (Def. \ref{InitialObject}) in the [[comma category]] $d/R$ (Example \ref{CommaCategoryWithOneSideConstant}).



\end{enumerate}
\end{prop}
$\,$

$\,$

After these equivalent characterizations of [[adjoint functors]], we now consider some of their main properties:

\begin{prop}
\label{UniquenessOfAdjoints}\hypertarget{UniquenessOfAdjoints}{}
\textbf{([[adjoint functors]] are unique up to [[natural isomorphism]])}

The [[left adjoint]] or [[right adjoint]] to a [[functor]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}), if it exists, is unique up to [[natural isomorphism]] (Def. \ref{NaturalTransformations}).

\end{prop}
\begin{proof}
Suppose the functor $L \colon \mathcal{D} \to \mathcal{C}$ is given, and we are asking for uniqueness of its right adjoint, if it exists. The other case is directly analogous.

Suppose that $R_1, R_2 \;\colon\; \mathcal{C} \to \mathcal{D}$ are two [[functors]] which both are [[right adjoint]] to $L$. Then for each $d \in \mathcal{D}$ the corresponding two hom-isomorphisms \eqref{HomIsomorphismForAdjointFunctors} combine to say that there is a [[natural isomorphism]]/

\begin{displaymath}
\Phi_d
  \;\colon\;
  Hom_{\mathcal{C}}(-,R_1(d))
  \;\simeq\;
  Hom_{\mathcal{C}}(-,R_2(d))
\end{displaymath}
As in the proof of Prop. \ref{AdjointFunctorFromObjectwiseRepresentingObject}, the [[Yoneda lemma]] implies that

\begin{displaymath}
\Phi_d \;=\; y( \phi_d )
\end{displaymath}
for some [[isomorphism]]

\begin{displaymath}
\phi_d \;\colon\;  R_1(d) \overset{\simeq}{\to} R_2(d)
  \,.
\end{displaymath}
But then the uniqueness statement of Prop. \ref{AdjointFunctorFromObjectwiseRepresentingObject} implies that the collection of these isomorphisms for each object constitues a [[natural isomorphism]] between the functors (Def. \ref{NaturalTransformations}).

\end{proof}
\begin{prop}
\label{FullyFaithfulAndInvertibleAdjoints}\hypertarget{FullyFaithfulAndInvertibleAdjoints}{}
\textbf{(characterization of [[epimorphism|epi]]/[[monomorphism|mono]]/[[isomorphism|iso]] [[adjunction counit|(co-)]][[adjunction unit|unit]] of [[adjunction]])}

Let

\begin{displaymath}
L \dashv R
  \;\colon\;
  \mathcal{D}
    \underoverset
      {\underset{\phantom{A}R\phantom{A}}{\longrightarrow}}
      {\overset{\phantom{A}L\phantom{A}}{\longleftarrow}}
      {\bot}
  \mathcal{C}
\end{displaymath}
be a pair of [[adjoint functors]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}).

Recall the definition of

\begin{enumerate}%
\item [[adjunction unit]]/[[adjunction counit|counit]], from Def. \ref{AdjunctionUnitFromHomIsomorphism})


\item [[faithful functor|faithful]]/[[fully faithful functor]] from Def. \ref{FullyFaithfulFunctor}


\item [[monomorphism|mono]]/[[epimorphism|epi]]/[[isomorphism]] from Def. \ref{Isomorphism} and Def. \ref{Monomorphism}.



\end{enumerate}
The following holds:

\begin{itemize}%
\item $R$ is [[faithful functor|faithful]] precisely if all components of the [[unit of an adjunction|counit]] are [[epimorphisms]] $L R(c) \underoverset{\phantom{A}epi\phantom{A}}{\eta_c}{\to} c$;


\item $L$ is [[faithful functor|faithful]] precisely if all components of the [[adjunction unit|unit]] are [[monomorphisms]] $d \underoverset{mono}{\eta_d}{\to} R L(d)$


\item $R$ is [[full and faithful functor|full and faithful]] (exhibits a \emph{[[reflective subcategory]]}, Def. \ref{ReflectiveSubcategory}) precisely if all components of the [[adjunction counit|counit]] are [[isomorphisms]] $L R(c) \underoverset{\phantom{A}iso\phantom{A}}{\eta_c}{\to} c$


\item $L$ is [[full and faithful functor|full and faithful]] (exhibits a [[coreflective subcategory]], def. \ref{ReflectiveSubcategory}) precisely if all component of the [[adjunction unit|unit]] are [[isomorphisms]] $d \underoverset{\phantom{A}iso\phantom{A}}{\eta_d}{\to} R L(d)$.



\end{itemize}
\end{prop}
\begin{proof}
This follows directly by Lemma \ref{ReExpressingMiddleFunctorInAdjointTriple}, using the definition of epi/monomorphism (Def. \ref{Monomorphism}) and the characterization of [[isomorphism]] from Example \ref{YonedaCharacterizationOfIsomorphism}.

\end{proof}
To complete this pattern, we will see below in Prop. \ref{EveryEquivalenceOfCategoriesComesFromAnAdjointEquivalence} that following are equivalent:

\begin{itemize}%
\item the [[adjunction unit|unit]] and [[adjunction counit|counit]] are both [[natural isomorphism]], hence $L$ and $R$ are both [[full and faithful functor|fully faithful]];


\item $L$ is an [[equivalence of categories|equivalence]] (Def. \ref{EquivalenceOfCategories});


\item $R$ is an [[equivalence of categories|equivalence]] (Def. \ref{EquivalenceOfCategories})


\item $L \dashv R$ is an [[adjoint equivalence]] (Def. \ref{AdjointEquivalenceOfCategories}).



\end{itemize}
\begin{prop}
\label{LeftAdjointFunctorPreservesEpi}\hypertarget{LeftAdjointFunctorPreservesEpi}{}
\textbf{(right/left [[adjoint functors]] preserve [[monomorphism]]/[[epimorphisms]] and [[terminal object|terminal]]/[[initial objects]])}

Every [[right adjoint]] functor (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}) preserves

\begin{enumerate}%
\item [[terminal objects]] (Def. \ref{InitialObject}),


\item [[monomorphisms]] (Def. \ref{Monomorphism})



\end{enumerate}
Every [[left adjoint]] functor (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}) preserves

\begin{enumerate}%
\item [[initial objects]] (Def. \ref{InitialObject}),


\item [[epimorphisms]] (Def. \ref{Monomorphism}).



\end{enumerate}
\end{prop}
\begin{proof}
This is immediate from the adjunction hom-isomorphism \eqref{HomIsomorphismForAdjointFunctors}, but we spell it out:

We consider the first case, the second is [[formal duality|formally dual]] (Example \ref{OppositeCategory}). So let $R \;\colon\; \mathcal{C} \to \mathcal{D}$ be a [[right adjoint functor]] with [[left adjoint]] $L$.

Let $\ast \in \mathcal{C}$ be a [[terminal object]] (Def. \ref{InitialObject}). We need to show that for every [[object]] $d \in \mathcal{D}$ the [[hom-set]] $Hom_{\mathcal{D}}(d,R(\ast)) \simeq \ast$ is a [[singleton]]. But by the hom-isomorphism \eqref{HomIsomorphismForAdjointFunctors} we have a [[bijection]]

\begin{displaymath}
\begin{aligned}
    Hom_{\mathcal{d}}(d,R(\ast))
    & \simeq
    Hom_{\mathcal{C}}(L(d), \ast)
    \\
    & \simeq \ast
    \,,
  \end{aligned}
\end{displaymath}
where in the last step we used that $\ast$ is a terminal object, by assumption.

Next let $c_1 \overset{f}{\hookrightarrow} c_2$ be a [[monomorphism]]. We need to show that for $d \in \mathcal{D}$ any [[object]], the [[hom-functor]] out of $d$ yields a monomorphism

\begin{displaymath}
Hom_{\mathcal{D}}(d, R(f))
  \;\colon\;
  Hom_{\mathcal{D}}(d, R(c_1))
    \hookrightarrow
  Hom_{\mathcal{D}}(d, R(c_2))
  \,.
\end{displaymath}
Now consider the following [[naturality square]] \eqref{NaturalitySquareForAdjointnessOfFunctors} of the adjunction hom-isomorphism \eqref{HomIsomorphismForAdjointFunctors}:

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{D}}(d, R(c_1))
    &\simeq&
    Hom_{\mathcal{C}}(L(d), c_1)
    \\
    {}^{ \mathllap{ Hom_{\mathcal{D}}(d,R(f)) } }\big\downarrow
      &&
    \big\downarrow^{ \mathrlap{ Hom_{\mathcal{C}}( L(d),f ) } }_{\mathrlap{mono}}
    \\
    Hom_{\mathcal{D}}(d, R(c_2))
    &\simeq&
    Hom_{\mathcal{C}}(L(d), c_2)
  }
\end{displaymath}
Here the right vertical [[function]] is an [[injective function]], by assumption on $f$ and the definition of [[monomorphism]]. Since the two horizontal functions are [[bijections]], this implies that also $Hom_{\mathcal{d}}(d,R(f))$ is an injection.

\end{proof}
But the main preservation property of [[adjoint functors]] is that \emph{[[adjoints preserve (co-)limits]]}. This we discuss as Prop. \ref{AdjointsPreserveCoLimits} below, after introducing [[limits]] and [[colimits]] in Def. \ref{Limits} below.

$\,$

Prop. \ref{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat} says that [[adjoint functors]] are equivalenty ``[[adjunctions]] in [[Cat]]'', as defined there. This is a special case of a general more abstract concept of [[adjunction]], that is useful:

\begin{defn}
\label{Strict2Categories}\hypertarget{Strict2Categories}{}
\textbf{([[strict 2-category]])}

A \emph{[[strict category]]} $\mathcal{C}$ is

\begin{enumerate}%
\item a [[class]] $Obj_{\mathcal{C}}$, called the \emph{class of [[objects]]};


\item for each [[pair]] $X,Y \in Obj_{\mathcal{C}}$ of [[objects]], a [[small category]] $Hom_{\mathcal{C}}(X,Y) \in Cat$ (Def. \ref{SmallCategory}), called the \emph{[[hom-category]] from $X$ to $Y$}.

We denote the [[objects]] of this [[hom-category]] by arrows like this:

\begin{displaymath}
X \overset{f}{\longrightarrow} Y \;\;\in Obj_{Hom_{\mathcal{C}}(X,Y)}
\end{displaymath}
and call them the \emph{[[1-morphisms]]} of $\mathcal{C}$,

and we denote the [[morphisms]] in the [[hom-category]] by double arrows, like this:

\begin{displaymath}
X
    \underoverset
      {\underset{g}{\longrightarrow}}
      {\overset{f}{\longrightarrow}}
      {\Downarrow{}^{\mathrlap{\phi}}}
  Y
\end{displaymath}
and call these the \emph{[[2-morphisms]]} of $\mathcal{C}$;


\item for each [[object]] $X \in Obj_{\mathcal{C}}$ a [[1-morphism]]

\begin{displaymath}
X \overset{id_X}{\to} X \;\; \in Hom_{\mathcal{C}}(X,X)
\end{displaymath}
called the \emph{[[identity morphism]]} on $X$;


\item for each [[triple]] $X_1, X_2, X_3 \in Obj$ of [[objects]], a [[functor]] (Def. \ref{Functors})

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{C}}(X_1, X_2)
    &\times&
    Hom_{\mathcal{C}}(X_2, X_3)
    &\overset{\circ_{X_1,X_2,X_3}}{\longrightarrow}&
    Hom_{\mathcal{C}}(X_1, X_3)
    \\
    X_1 \overset{f}{\to} X_2
    &,&
    X_2 \overset{f}{\to} X_3
    &\mapsto&
    X_1 \overset{ g \circ f }{\longrightarrow} X_3
  }
\end{displaymath}
from the [[product category]] (Example \ref{ProductCategory}) of [[hom-categories]], called \emph{[[composition]]};



\end{enumerate}
such that:

\begin{enumerate}%
\item for all [[pairs]] of [[objects]] $X,Y \in Obj_{\mathcal{C}}$ [[unitality]] holds:

the [[functors]] of [[composition]] with [[identity morphisms]] are [[identity functors]]

\begin{displaymath}
(-) \circ id_X
  \;=\;
  id_{ Hom_{\mathcal{C}}(X,Y) }
  \phantom{AAAA}
  id_Y \circ (-)      
  \;=\;
  id_{ Hom_{\mathcal{C}}(X,Y) }
\end{displaymath}

\item for all [[quadruples]] of [[objects]] $X_1, X_2, X_3, X_4 \in Obj_{\mathcal{C}}$ [[composition]] satifies \emph{[[associativity]]}, in that the following two composite [[functors]] are [[equality|equal]]:

\begin{displaymath}
\itexarray{
    Hom_{\mathcal{C}}(X_1, X_2) 
     \times 
    Hom_{\mathcal{C}}(X_2, X_3) 
     \times 
    Hom_{\mathcal{C}}(X_3, X_4) 
    &\overset{((-)\circ (-))\circ (-)}{\longrightarrow}&
    Hom_{\mathcal{C}}(X_1, X_3) \times Hom_{\mathcal{C}}(X_3, X_4)
    \\
    {}^{ \mathllap{ (-) \circ ( (-) \circ (-) ) } }\Big\downarrow 
    && 
    \Big\downarrow{}^{ (-) \circ (-) }
    \\
    Hom_{\mathcal{C}}(X_1, X_2) \times Hom_{\mathcal{C}}(X_2, X_4)
    &\underset{(-)\circ (-)}{\longrightarrow}&
    Hom_{\mathcal{C}}(X_1, X)4)
  }
\end{displaymath}


\end{enumerate}
\end{defn}
The archetypical example of a [[strict 2-category]] is the [[category of categories]]:

\begin{example}
\label{2CategoryOfCategories}\hypertarget{2CategoryOfCategories}{}
\textbf{([[2-category of categories]])}

There is a [[strict 2-category]] (Def. \ref{Strict2Categories}) [[Cat]] whose

\begin{itemize}%
\item [[objects]] are [[small categories]] (Def. \ref{SmallCategory});


\item [[1-morphisms]] are [[functors]] (Def. \ref{Functors});


\item [[2-morphisms]] are [[natural transformations]] (Def. \ref{NaturalTransformations})



\end{itemize}
with the evident [[composition]] operations.

\end{example}
With a concept of [[2-category]] in hand, we may phrase Prop. \ref{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat} more abstractly:

\begin{defn}
\label{AdjunctionInA2Category}\hypertarget{AdjunctionInA2Category}{}
\textbf{([[adjunction]] in a [[2-category]])}

Let $\mathcal{C}$ be a [[strict 2-category]] (Def. \ref{Strict2Categories}). Then an \emph{[[adjunction]]} in $\mathcal{C}$ is

\begin{enumerate}%
\item a [[pair]] of [[objects]] $\mathcal{C}, \mathcal{D} \in Obj_{\mathcal{C}}$;


\item [[1-morphisms]]

\begin{displaymath}
\mathcal{D}
    \underoverset
      {\underset{\phantom{AA}R\phantom{AA}}{\longrightarrow}}
      {\overset{L}{\longleftarrow}}
      {}
  \mathcal{C}
\end{displaymath}
called the \emph{[[left adjoint]]} $L$ and \emph{[[right adjoint]]} $R$;


\item [[2-morphisms]]

$id_{\mathcal{C}} \overset{\eta}{\Rightarrow} R \circ L$, called the [[adjunction unit]]

$L \circ R \overset{\epsilon}{\Rightarrow} id_{\mathcal{D}}$, called the [[adjunction counit]]



\end{enumerate}
such that the following \emph{[[triangle identities]]} hold:

We denote this situation by

\begin{displaymath}
\mathcal{D}
       \underoverset
         {\underset{\phantom{AA}R\phantom{AA}}{\longrightarrow}}
         {\overset{L}{\longleftarrow}}
         {\bot}
     \mathcal{C}
\end{displaymath}
\end{defn}
Hence via Example \ref{2CategoryOfCategories}, Prop. \ref{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat} says that an [[adjoint pair]] of [[functors]] is equivalente an [[adjunction]] in the general sense of Def. \ref{AdjunctionInA2Category}, realized in the [[very large category|very large]] [[strict 2-category]] [[Cat]] of [[categories]].

This more abstract perspecive on [[adjunctions]] allow us now to understand ``duality of dualities'' as [[adjunction]] in a [[2-category]] of [[adjunctions]]:

\begin{example}
\label{2CategoryOfCategoriesWithAdjointFunctorsBetweenThem}\hypertarget{2CategoryOfCategoriesWithAdjointFunctorsBetweenThem}{}
\textbf{([[strict 2-category]] of [[categories]] with [[adjoint functors]] between them)}

Let $Cat_{Adj}$ be the [[strict 2-category]] which is defined just as [[Cat]] (Def. \ref{2CategoryOfCategories}) but with the [[1-morphisms]] being [[functors]] that are required to be [[left adjoints]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}).

Since adjoints are unique up to natural isomorphism (Prop. \ref{UniquenessOfAdjoints}), this may be thought of as a 2-category whose [[1-morphisms]] are [[adjoint pairs]] of [[functors]].

\end{example}
\begin{example}
\label{AdjunctionofAdjunction}\hypertarget{AdjunctionofAdjunction}{}
\textbf{([[adjunctions]] of [[adjoint pairs]] are [[adjoint triples]])}

An [[adjunction]] (Def. \ref{AdjunctionInA2Category}) in the [[2-category]] $Cat_{Adj}$ of [[categories]] with [[adjoint functors]] between them (Example \ref{2CategoryOfCategoriesWithAdjointFunctorsBetweenThem}) is equivalently an [[adjoint triple]] of functors (Remark \ref{AdjointTriples}):

The adjunction says that two [[left adjoint functors]] $L_1$ and $L_2$, which, hence each participate in an [[adjoint pair]]

\begin{displaymath}
L_1 \dashv R_1
  \phantom{AAAA}
  L_2 \dashv R_2
\end{displaymath}
form themselves an [[adjoint pair]]

\begin{displaymath}
L_1 \dashv L_2
  \,.
\end{displaymath}
By essentiall uniqueness of adjoints (Prop. \ref{UniquenessOfAdjoints}) this implies a [[natural isomorphism]] $R_1 \simeq L_2$ and hence an [[adjoint triple]]:

\begin{displaymath}
\mathcal{D}
    \itexarray{
      \underoverset{\bot \phantom{\simeq A_a}}{ L_1 \phantom{\simeq A_a} }{\longleftarrow}
      \\
      \underoverset{\phantom{A_a \simeq}\bot}{R_1 \simeq L_2}{\longrightarrow}
      \\
      \overset{ \phantom{A_a \simeq} R_2 }{\longleftarrow}
    }
  \mathcal{C}
\end{displaymath}
\end{example}
Example \ref{AdjunctionofAdjunction} suggest to consider a slight variant of the concept of [[strict 2-categories]] which allows to make the duality between [[left adjoints]] and [[right adjoints]] explicit:

\begin{defn}
\label{DoubleCategory}\hypertarget{DoubleCategory}{}
\textbf{([[double category]])}

A \emph{[[double category]]} $\mathcal{C}$ is

\begin{enumerate}%
\item a [[pair]] of [[categories]] $\mathcal{C}_h$, $\mathcal{C}_v$ (Def. \ref{Categories}) which share the same class of objects: $Obj_{\mathcal{C}_1} = Obj_{\mathcal{C}_2}$, to be called the class $Obj_{\mathcal{C}}$ of \emph{objects of $\mathcal{C}$}

where the [[morphisms]] of $\mathcal{C}_h$ are to be called the \emph{[[horizontal morphisms]]} of $\mathcal{C}$,

while the [[morphisms]] of $\mathcal{C}_v$ are to be called the \emph{[[vertical morphisms]]} of $\mathcal{C}$,


\item for each [[quadruple]] of [[objects]] $a,b,c,d,e \in Obj_{\mathcal{C}}$ and [[pairs]] of [[pairs]] of horizontal/vertical morphisms of the form

\begin{displaymath}
\itexarray{
    a &\overset{f \in \mathcal{C}_h}{\longrightarrow}& b
    \\
    {}^{\mathllap{h \in \mathcal{C}_v}}\big\downarrow && \big\downarrow{}^{\mathrlap{k \in \mathcal{C}_v}}
    \\
    c &\underset{g \in \mathcal{C}_h}{\longrightarrow}&
  }
\end{displaymath}
a [[set]] $2Hom(f,g,h,k)$, to be called the set of \emph{[[2-morphisms]]} of $\mathcal{C}$ between the given [[1-morphisms]], whose elements we denote by

\begin{displaymath}
\itexarray{
    a &\overset{f \in \mathcal{C}_h}{\longrightarrow}& b
    \\
    {}^{\mathllap{h \in \mathcal{C}_v}}\big\downarrow 
    &\swArrow& \big\downarrow{}^{\mathrlap{k \in \mathcal{C}_v}}
    \\
    c &\underset{g \in \mathcal{C}_h}{\longrightarrow}& d
  }
\end{displaymath}

\item a horizontal and a vertical [[composition operation]] of 2-morphisms which is [[unitality]] and [[associativity|associative]] in both directions in the evident way, which respects composition in $\mathcal{C}_h$ and $\mathcal{C}_v$, and such that horizontal and vertical composition commute over each other in the evident way.



\end{enumerate}
\end{defn}
\begin{example}
\label{DoubleCategoryOfSquares}\hypertarget{DoubleCategoryOfSquares}{}
\textbf{([[double category of squares]] of a [[strict 2-category]])}

Let $\mathcal{C}$ be a [[strict 2-category]] (Def. \ref{Strict2Categories}). Then its \emph{[[double category of squares]]} $Sq(\mathcal{C})$ is the [[double category]] (Def. \ref{DoubleCategory}) whose

\begin{itemize}%
\item [[objects]] are those of $\mathcal{C}$;


\item [[horizontal morphisms]] and [[vertical morphisms]] are both the [[1-morphisms]] of $\mathcal{C}$;


\item [[2-morphisms]]

\begin{displaymath}
\itexarray{
    a &\overset{f \in \mathcal{C}_h}{\longrightarrow}& b
    \\
    {}^{\mathllap{h \in \mathcal{C}_v}}\big\downarrow 
      &{}^{\mathllap{\phi}}\swArrow& 
    \big\downarrow{}^{\mathrlap{k \in \mathcal{C}_v}}
    \\
    c &\underset{g \in \mathcal{C}_h}{\longrightarrow}& d
  }
\end{displaymath}
are the [[2-morphisms]] of $\mathcal{C}$ between the evident composites of 1-morphisms:

\begin{displaymath}
k \circ f \overset{\phi}{\Rightarrow} g\circ h
\end{displaymath}


\end{itemize}
and composition is given by the evident compositions in $\mathcal{C}$.

\end{example}
\begin{remark}
\label{StrictAndWeak2Functors}\hypertarget{StrictAndWeak2Functors}{}
\textbf{([[strict 2-functor|strict]] and [[weak 2-functor|weak]] [[2-functors]])}

Given two [[strict 2-categories]] (Def. \ref{Strict2Categories}) or [[double categories]] (Def. \ref{DoubleCategory}), $\mathcal{C}, \mathcal{D}$, there is an evident notion of \emph{[[2-functor]]} or \emph{[[double functor]]}

\begin{displaymath}
\mathcal{C} \overset{F}{\longrightarrow} \mathcal{D}
\end{displaymath}
between them, namely [[functions]] on [[objects]], [[1-morphisms]] and [[2-morphisms]] which respect all the [[composition]] operations and [[identity morphisms]].

These are also called \emph{[[strict 2-functors]]}.

This is in contrast to a more flexible concept of \emph{[[weak 2-functors]]}, often called \emph{[[pseudofunctors]]}, which respect [[composition]] of [[1-morphisms]] only up to invertible [[2-morphisms]] (which themselves are required to satisfy some [[coherence]] condition):

\begin{displaymath}
\itexarray{
    && Y
    \\
    & {}^{\mathllap{ F(f) }}\nearrow 
      &\Downarrow{}^{\rho}_{}\simeq& 
    \searrow^{\mathrlap{F(G)}}
    \\
    X && \underset{F(g \circ f)}{\longrightarrow} && Z
  }
\end{displaymath}
\end{remark}
We will see an important example of a weak double functor in the construction of [[derived functors]] of [[Quillen functors]], below in Prop. \ref{HomotopyDoublePseudofunctor}.

$\,$

\hypertarget{Equivalences}{}\subsubsection*{{Equivalences}}\label{Equivalences}

We have seen [[functors]] (Def. \ref{Functors}) as the [[homomorphisms]] between [[categories]] (Def. \ref{Categories}). But functors themselves are identified only up to [[natural isomorphism]] (Def. \ref{NaturalTransformations}), reflective the fact that they are the [[1-morphisms]] in a [[2-category]] of categories (Example \ref{2CategoryOfCategories}). This means that in identifying two categories, we should not just ask for \emph{[[isomorphisms]]} between them, hence for a [[functor]] between them that has a strict [[inverse morphism]], but just for an inverse up to [[natural isomorphism]].

This is called an \emph{[[equivalence of categories]]} (Def. \ref{EquivalenceOfCategories} below). A particularly well-behaved equivalence of categories is an equivalence exhibited by an [[adjoint pair]] of functors, called an \emph{[[adjoint equivalence of categories]]} (Def. \ref{AdjointEquivalenceOfCategories} below). In fact every [[equivalence of categories]] may be improved to an [[adjoint equivalence]] (Prop. \ref{EveryEquivalenceOfCategoriesComesFromAnAdjointEquivalence}).

$\,$

\begin{defn}
\label{AdjointEquivalenceOfCategories}\hypertarget{AdjointEquivalenceOfCategories}{}
\textbf{([[adjoint equivalence of categories]])}

Let $\mathcal{C}$, $\mathcal{D}$ be two [[categories]] (Def. \ref{Categories}). Then an \emph{[[adjoint equivalence of categories]]} between them is a [[pair]] [[adjoint functors]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets})

\begin{displaymath}
\itexarray{
    \mathcal{C}
      \underoverset
        {\underset{R}{\longrightarrow}}
        {\overset{L}{\longleftarrow}}
        {\phantom{A} \phantom{{}_{\bot}}\simeq_{\bot} \phantom{A}}
    \mathcal{D}
  }
\end{displaymath}
such that their [[unit of an adjunction|unit]] $\eta$ and [[counit of an adjunction|counit]] $\epsilon$ (Def. \ref{AdjunctionUnitFromHomIsomorphism}) are [[natural isomorphisms]] (as opposed to just being [[natural transformations]])

\begin{displaymath}
\eta\;\colon\; id_{\mathcal{D}} \overset{\simeq}{\Rightarrow} R \circ L
  \phantom{AAA}
   \text{and}
  \phantom{AAA}
  \epsilon\;\colon\;
  L \circ R \overset{\simeq}{\Rightarrow} id_{\mathcal{C}}
  \,.
\end{displaymath}
\end{defn}
There is also the following, seemingly weaker, notion:

\begin{defn}
\label{EquivalenceOfCategories}\hypertarget{EquivalenceOfCategories}{}
\textbf{([[equivalence of categories]])}

Let $\mathcal{C}$, $\mathcal{D}$ be two [[categories]] (Def. \ref{Categories}). Then an \emph{[[equivalence of categories]]}

\begin{displaymath}
\itexarray{
    \mathcal{C}
      \underoverset
        {\underset{R}{\longrightarrow}}
        {\overset{L}{\longleftarrow}}
        {\phantom{AA} \simeq \phantom{AA}}
    \mathcal{D}
  }
\end{displaymath}
is a [[pair]] of [[functors]] back and forth, as shown (Def. \ref{Functors}), together with [[natural isomorphisms]] (Def. \ref{NaturalTransformations}) between their [[composition]] and the [[identity functors]]:

\begin{displaymath}
id_{\mathcal{D}} \overset{\simeq}{\Rightarrow} R \circ L
  \phantom{AAA}
   \text{and}
  \phantom{AAA}
  L \circ R \overset{\simeq}{\Rightarrow} id_{\mathcal{C}}
  \,.
\end{displaymath}
\end{defn}
If a functor participates in an equivalence of categories, that functor alone is usually already called an equivalence of categories. If there is any equivalence of categories between two categories, these categories are called \emph{equivalent}.

\begin{prop}
\label{EveryEquivalenceOfCategoriesComesFromAnAdjointEquivalence}\hypertarget{EveryEquivalenceOfCategoriesComesFromAnAdjointEquivalence}{}
\textbf{(every [[equivalence of categories]] comes from an [[adjoint equivalence of categories]])}

Let $\mathcal{C}$ and $\mathcal{D}$ be two [[categories]] (Def. \ref{Categories}). Then the they are [[equivalence of categories|equivalent]] (Def. \ref{EquivalenceOfCategories}) precisely if there exists an [[adjoint equivalence of categories]] between them (Def. \ref{AdjointEquivalenceOfCategories}).

Moreover, let $R \;\colon\; \mathcal{C} \longrightarrow \mathcal{D}$ be a [[functor]] (Def. \ref{Functors}) which participates in an [[equivalence of categories]] (Def. \ref{EquivalenceOfCategories}). Then for every functor $L \;\colon\; \mathcal{D} \to \mathcal{C}$ equipped with a [[natural isomorphism]]

\begin{displaymath}
\eta
    \;\colon\;
  id_{\mathcal{D}}
    \overset{\simeq}{\Rightarrow}
  R \circ L
\end{displaymath}
there exists a [[natural isomorphism]]

\begin{displaymath}
\epsilon
  \;\colon\;
  L \circ R \overset{\simeq}{\Rightarrow} id_{\mathcal{C}}
\end{displaymath}
which completes this to an [[adjoint equivalence of categories]] (Def. \ref{AdjointEquivalenceOfCategories}).

\end{prop}
Inside every [[adjunction]] sits its maximal [[adjoint equivalence]]:

\begin{prop}
\label{FixedPointEquivalenceOfAnAdjunction}\hypertarget{FixedPointEquivalenceOfAnAdjunction}{}
\textbf{([[fixed point equivalence of an adjunction]])}

Let

\begin{displaymath}
\mathcal{D}
    \underoverset
      {\underset{ R }{\longrightarrow}}
      {\overset{ L }{\longleftarrow}}
      {\phantom{AA}\bot\phantom{AA}}
  \mathcal{C}
\end{displaymath}
be a pair of [[adjoint functors]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}). Say that

\begin{enumerate}%
\item an [[object]] $c \in \mathcal{C}$ is a \emph{[[fixed point of an adjunction|fixed point of the adjunction]]} if its [[adjunction unit]] (Def. \ref{AdjunctionUnitFromHomIsomorphism}) is an [[isomorphism]] (Def. \ref{Isomorphism})

\begin{displaymath}
c \underoverset{\simeq}{\eta_c}{\longrightarrow} R L (c)
\end{displaymath}
and write

\begin{displaymath}
\mathcal{C}_{fix} \hookrightarrow \mathcal{C}
\end{displaymath}
for the [[full subcategory]] on these fixed objects (Example \ref{FullSubcategoryOnClassOfObjects})


\item an [[object]] $d \in \mathcal{D}$ is a \emph{[[fixed point of an adjunction|fixed point of the adjunction]]} if its [[adjunction counit]] (Def. \ref{AdjunctionUnitFromHomIsomorphism}) is an [[isomorphism]] (Def. \ref{Isomorphism})

\begin{displaymath}
L R(d) \underoverset{\simeq}{\epsilon_d}{\longrightarrow}
\end{displaymath}
and write

\begin{displaymath}
\mathcal{D}_{fix} \hookrightarrow \mathcal{D}
\end{displaymath}
for the [[full subcategory]] on these fixed objects (Example \ref{FullSubcategoryOnClassOfObjects})



\end{enumerate}
Then the [[adjunction]] ([[corestriction|co]]-)[[restriction|restrics]] to an [[adjoint equivalence]] (Def. \ref{AdjointEquivalenceOfCategories}) on these [[full subcategories]] of [[fixed points]]

\begin{displaymath}
\mathcal{D}_{fix}
    \underoverset
      {\underset{ R }{\longrightarrow}}
      {\overset{ L }{\longleftarrow}}
      {\phantom{A}\phantom{{}_{\bot}}\simeq_{\bot}\phantom{A}}
  \mathcal{C}_{fix}
\end{displaymath}
\end{prop}
\begin{proof}
It is sufficient to see that the functors ([[corestriction|co-]])[[restriction|restrict]] as claimed, for then the restricted adjunction unit/counit are [[isomorphisms]] by definition, and hence exhibit an [[adjoint equivalence]].

Hence we need to show that

\begin{enumerate}%
\item for $c \in \mathcal{C}_{fix} \hookrightarrow \mathcal{C}$ we have that $\eta_{R(d)}$ is an [[isomorphism]];


\item for $d \in \mathcal{D}_{fix} \hookrightarrow \mathcal{D}$ we have that $\epsilon_{L(c)}$ is an [[isomorphism]].



\end{enumerate}
For the first case we claim that $R(\eta_{d})$ provides an [[inverse morphism|inverse]]: by the [[triangle identity]] \eqref{TriangleIdentities} it is a [[right inverse]], but by assumption it is itself an [[invertible morphism]], which implies that $\eta_{R(d)}$ is an isomorphism.

The second claim is [[formal duality|formally dual]].

\end{proof}
$\,$

\hypertarget{Modalities}{}\subsubsection*{{Modalities}}\label{Modalities}

Generally, a [[full subcategory]]-inclusion (Def. \ref{FullyFaithfulFunctor}) may be thought of as a consistent [[proposition]] about [[objects]] in a [[category]]: The objects in the full subcategory are those that have the given property.

This basic situation becomes particularly interesting when the inclusion functor has a [[left adjoint]] or a [[right adjoint]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}), in which case one speaks of a \emph{[[reflective subcategory]]}, or a \emph{[[coreflective subcategory]]}, respectively (Def. \ref{ReflectiveSubcategory} below). The [[adjunction]] now implies that each [[object]] is \emph{[[reflector|reflected]]} or \emph{[[coreflector|coreflected]]} into the subcategory, and equipped with a comparison morphism to or from its (co-)reflection (the adjunction (co-)unit, Def. \ref{AdjunctionUnitFromHomIsomorphism}). This comparison morphism turns out to always be an idempotent (co-)projection, in a sense made precise by Prop. \ref{ModalOpIdempotent} below.

This means that, while any object may not fully enjoy the property that defines the subcategory, one may ask for the ``aspect'' of it that does, which is what is (co-)projected out. Regarding objects only via these aspects of them hence means to regard them only \emph{locally} (where they exhibit that aspect) or only in the \emph{mode} of focus on this aspect. Therefore one also calls the (co-)reflection operation into the given subcategory a \emph{([[colocalization|co]]-)[[localization]]} or \emph{([[comodal operator|co-]])[[modal operator]]}, or \emph{[[modality]]}, for short (Def. \ref{ModalOperator} below).

One finds that (co-)modalities are a fully equivalent perspective on the (co-)reflective subcategories of their fully \emph{([[comodal object|co-]])[[modal objects]]} (Def. \ref{ModalObjects} below), this is the statement of Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories} below.

Another alternative perspective on this situation is given by the concept of \emph{[[localization of categories]]} (Def. \ref{LocalizationOfACategory} below), which is about [[universal property|universally]] forcing a given collection of [[morphisms]] (``[[weak equivalences]]'', Def. \ref{CategoryWithWeakEquivalences} below) to become [[inverse morphism|invertible]]. A \emph{[[reflective localization]]} is equivalently a [[reflective subcategory]]-inclusion (Prop. \ref{ReflectiveSubcategoriesAreLocalizations} below), and this exhibits the [[modal objects]] (Def. \ref{ModalObjects} below) as equivalently forming the [[full subcategory]] of \emph{[[local objects]]} (Def. \ref{LocalObjects} below).

Conversely, every [[reflective subcategory|reflection]] onto [[full subcategories]] of $S$-[[local objects]] (Def. \ref{LocalizationAtACollectionOfMorphisms} below) satisfies the [[universal property]] of a [[localization]] at $S$ with respect to [[left adjoint]] [[functors]] (Prop. \ref{ReflectionOntoLocalObjectsIsLocalizationWithRespectToLeftAdjoints} below).

In conclusion, we have the following three equivalent perspectives on [[modalities]].

\newline $\,$

\begin{defn}
\label{ReflectiveSubcategory}\hypertarget{ReflectiveSubcategory}{}
\textbf{([[reflective subcategory]] and [[coreflective subcategory]])}

Let $\mathcal{D}$ be a [[category]] (Def. \ref{Categories}) and

\begin{displaymath}
\mathcal{C}
  \overset{\phantom{AA}\iota \phantom{AA}}{\hookrightarrow}
  \mathcal{D}
\end{displaymath}
a [[full subcategory]]-inclusion (hence a [[fully faithful functor]] Def. \ref{FullyFaithfulFunctor}). This is called:

\begin{enumerate}%
\item a \emph{[[reflective subcategory]] inclusion} if the inclusion functor $\iota$ has a [[left adjoint]] $L$ def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets})

\begin{displaymath}
\mathcal{C}
    \underoverset
      {\underset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow}}
      {\overset{L}{\longleftarrow}}
      {\bot}
  \mathcal{D}
  \,,
\end{displaymath}
then called the \emph{[[reflector]]};


\item a \emph{[[coreflective subcategory]]}-inclusion if the inclusion functor $\iota$ has a [[right adjoint]] $R$ (def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets})

\begin{displaymath}
\mathcal{C}
    \underoverset
      \underset{R}{\longleftarrow}
      {\overset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow}}
      {\bot}
  \mathcal{D}
  \,,
\end{displaymath}
then called the \emph{[[coreflector]]}.



\end{enumerate}
\end{defn}
\begin{example}
\label{ReflectiveSubcategoryInclusionOfSetsIntoGroupoids}\hypertarget{ReflectiveSubcategoryInclusionOfSetsIntoGroupoids}{}
\textbf{([[reflective subcategory]] inclusion of [[sets]] into [[small groupoid|small]] [[groupoids]])}

There is a [[reflective subcategory]]-inclusion (Def. \ref{ReflectiveSubcategory})

\begin{displaymath}
Set
    \underoverset
     {\underset{\phantom{AAAA}}{\hookrightarrow}}
     {\overset{\pi_0}{\longleftarrow}}
     {\bot}
  Grp
\end{displaymath}
of the [[category of sets]] (Example \ref{CategoryOfSets}) into the [[category]] [[Grpd]] (Example \ref{CategoriesOfSmallCategories}) of [[small groupoids|small]] [[groupoids]] (Example \ref{Groupoid}) where

\begin{itemize}%
\item the [[right adjoint]] [[full subcategory]] inclusion (Def. \ref{FullyFaithfulFunctor}) sends a [[set]] $S$ to the [[groupoid]] with set of objects being $S$, and the only [[morphisms]] being the [[identity morphisms]] on these objects (also called the \emph{[[discrete groupoid]]} on $S$, but this terminology is ambiguous)


\item the [[left adjoint]] [[reflector]] sends a [[small groupoid|small]] [[groupoid]] $\mathcal{G}$ to its set of [[connected components]], namely to the set of [[equivalence classes]] under the [[equivalence relation]] on the set of [[objects]], which regards two objects as equivalent, if there is any [[morphism]] between them.



\end{itemize}
\end{example}
$\,$

We now re-consider the concept of [[reflective subcategories]] from the point of view of [[modalities]]:

\begin{defn}
\label{ModalOperator}\hypertarget{ModalOperator}{}
\textbf{([[modality]])}

Let $\mathcal{D}$ be a [[category]] (Def. \ref{Categories}). Then

\begin{enumerate}%
\item a \emph{[[modal operator]] on $\mathcal{D}$} is

\begin{enumerate}%
\item an [[endofunctor]]

\begin{displaymath}
\bigcirc \;\colon\; \mathcal{D} \to \mathcal{D}
\end{displaymath}
whose [[full subcategory|full]] [[essential image]] we denote by

\begin{displaymath}
Im(\bigcirc)
 \overset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow}
  \mathcal{D}
  \,,
\end{displaymath}

\item a [[natural transformation]] (Def. \ref{NaturalTransformations})

\begin{equation}
X \overset{\eta_X}{\longrightarrow} \bigcirc X
\label{UnitOfAModalOperator}\end{equation}
for all [[objects]] $X \in \mathcal{D}$, to be called the \emph{unit morphism};



\end{enumerate}
such that:

\begin{itemize}%
\item for every [[object]] $Y \in Im(\bigcirc) \hookrightarrow \mathcal{D}$ in the [[essential image]] of $\bigcirc$, every [[morphism]] $f$ into $Y$ factors \emph{uniquely} through the unit \eqref{UnitOfAModalOperator}

\begin{displaymath}
\itexarray{
    && X
    \\
    & {}^{\mathllap{ \eta_X }}\swarrow && \searrow^{\mathrlap{f}}
    \\
    \mathrlap{\bigcirc X\;\;\;\;} && \underset{\exists !}{\longrightarrow} &&  Y & \in Im(\bigcirc)
  }
\end{displaymath}
which equivalently means that if $Y \in Im(\bigcirc)$ the operation of [[composition|precomposition]] with the unit $\eta_X$ yields a [[bijection]] of [[hom-sets]]

\begin{equation}
(-)\circ \eta_X
  \;\colon\;
  Hom_{\mathcal{D}}(\bigcirc X, Y)
  \overset{\phantom{AA}\simeq\phantom{AA}}{\longrightarrow}
  Hom_{\mathcal{D}}(X, Y)
  \,,
\label{ModalityUnitPrecomposition}\end{equation}


\end{itemize}

\item a \emph{[[comodal operator]] on $\mathcal{D}$} is

\begin{enumerate}%
\item an [[endofunctor]]

\begin{displaymath}
\Box \;\colon\; \mathcal{D} \to \mathcal{D}
\end{displaymath}
whose [[full subcategory|full]] [[essential image]] we denote by

\begin{displaymath}
Im( \Box )
 \overset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow}
  \mathcal{D}
\end{displaymath}

\item a [[natural transformation]] (Def. \ref{NaturalTransformations})

\begin{equation}
\Box X \overset{ \epsilon_X }{\longrightarrow} X
\label{CounitOfModalOperator}\end{equation}
for all [[objects]] $X \in \mathcal{D}$, to be called the \emph{counit morphism};



\end{enumerate}
such that:

\begin{itemize}%
\item for every [[object]] $Y \in Im( \Box ) \hookrightarrow \mathcal{D}$ in the [[essential image]] of $\Box$, every [[morphism]] $f$ out of $Y$ factors \emph{uniquely} through the counit \eqref{UnitOfAModalOperator}

\begin{displaymath}
\itexarray{
  && X
  \\
  & {}^{\mathllap{\epsilon_X}}\nearrow && \nwarrow^{\mathrlap{f}}
  \\
  \mathrlap{\Box X\;\;\;} && \underset{\exists !}{\longleftarrow} && Y \in Im( \Box )
  }
\end{displaymath}
which equivalently means that if $Y \in Im(\bigcirc)$ the operation of [[composition|postcomposition]] with the counit $\epsilon_X$ yields a [[bijection]] of [[hom-sets]]

\begin{equation}
\epsilon_X \circ (-)
  \;\colon\;
  Hom_{\mathcal{D}}(Y, \Box X)
  \overset{\phantom{AA}\simeq\phantom{AA}}{\longrightarrow}
  Hom_{\mathcal{D}}(Y , X)
  \,,
\label{CoModalityCoUnitPostcomposition}\end{equation}


\end{itemize}


\end{enumerate}
\end{defn}
\begin{prop}
\label{ModalOperatorsEquivalentToReflectiveSubcategories}\hypertarget{ModalOperatorsEquivalentToReflectiveSubcategories}{}
\textbf{([[modal operators]] equivalent to [[reflective subcategories]])}

If

\begin{displaymath}
\mathcal{C}
    \underoverset
      {\underset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow}}
      {\overset{L}{\longleftarrow}}
      {\bot}
  \mathcal{D}
\end{displaymath}
is a [[reflective subcategory]]-inclusion (Def. \ref{ReflectiveSubcategory}). Then the [[composition|composite]]

\begin{displaymath}
\bigcirc
  \;\coloneqq\;
  \iota \circ L
  \;\colon\;
  \mathcal{D} \longrightarrow \mathcal{D}
\end{displaymath}
equipped with the [[adjunction unit]] [[natural transformation]] (Def. \ref{AdjunctionUnitFromHomIsomorphism})

\begin{displaymath}
X \overset{\eta_X}{\longrightarrow} \bigcirc X
\end{displaymath}
is a [[modal operator]] on $\mathcal{D}$ (Def. \ref{ModalOperator}).

Dually, if

\begin{displaymath}
\mathcal{C}
    \underoverset
      {\underset{R}{\longleftarrow}}
      {\overset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow}}
      {\bot}
  \mathcal{D}
\end{displaymath}
is a [[coreflective subcategory]]-inclusion (Def. \ref{ReflectiveSubcategory}). Then the [[composition|composite]]

\begin{displaymath}
\Box
  \;\coloneqq\;
  \iota \circ R
  \;\colon\;
  \mathcal{D} \longrightarrow \mathcal{D}
\end{displaymath}
equipped with the [[adjunction counit]] [[natural transformation]] (Def. \ref{AdjunctionUnitFromHomIsomorphism})

\begin{displaymath}
\Box X \overset{ \epsilon_X }{\longrightarrow} X
\end{displaymath}
is a [[comodal operator]] on $\mathcal{D}$ (Def. \ref{ModalOperator}).

Conversely:

If an [[endofunctor]] $\bigcirc \;\colon\; \mathcal{D} \to \mathcal{D}$ with [[natural transformation]] $X \overset{\eta_X}{\to} \bigcirc X$ is a [[modal operator]] on a [[category]] $\mathcal{D}$ (Def. \ref{ModalOperator}), then the inclusion of its [[full subcategory|full]] [[essential image]] is a [[reflective subcategory]] inclusion (Def. \ref{ReflectiveSubcategory}) with [[reflector]] given by the [[corestriction]] of $\bigcirc$ to its image:

\begin{displaymath}
Im( \bigcirc )
    \underoverset
      {\underset{ \phantom{AA} \iota \phantom{AA} }{\hookrightarrow}}
      {\overset{ \bigcirc }{\longleftarrow}}
      {}
  \mathcal{D}
  \,.
\end{displaymath}
Dually, if an [[endofunctor]] $\Box \;\colon\; \mathcal{D} \to \mathcal{D}$ with [[natural transformation]] $\Box X \overset{\epsilon_X}{\longrightarrow} X$ is a [[comodal operator]] (Def. \ref{ModalOperator}), then the inclusion of its [[full subcategory|full]] [[essential image]] is a [[coreflective subcategory]] inclusion (Def. \ref{ReflectiveSubcategory}) with [[coreflector]] given by the [[corestriction]] of $\Box$ to its image

\begin{displaymath}
Im( \Box )
    \underoverset
      {\underset{ \Box }{\longleftarrow}}
      {\overset{ \phantom{AA} \iota \phantom{AA} }{\hookrightarrow}}
      {}
  \mathcal{D}
  \,.
\end{displaymath}
\end{prop}
\begin{proof}
The first two statements are immedialy a special case of the characterization of [[adjunctions]] via [[universal morphisms]] in Prop. \ref{CollectionOfUniversalArrowsEquivalentToAdjointFunctor}: Using that $R = \iota$ is here assumed to be [[fully faithful functor|fully faithful]], the uniqueness of $\tilde f$ in the [[universal morphism]]-factorization condition \eqref{UniversalArrowFactorization}

\begin{displaymath}
\itexarray{
    && c
    \\
    & {}^{\mathllap{\eta_c}}\swarrow && \searrow^{\mathrlap{f}}
    \\
    R(L(c)) &&\underset{R (\widetilde f)}{\longrightarrow}&& R(d)
    \\
    \\
    L(c) &&\underset{ \exists ! \, \widetilde f}{\longrightarrow}&& d
  }
\end{displaymath}
implies that also $R(\widetilde f) = \iota(\widetilde f)$ is the unique morphism making that triangle commute.

Similarly for the converse: The assumption on a [[modal operator]] $\bigcirc$ is just so as to make its unit $\eta$ be a [[universal morphism]] (Def. \ref{UniversalArrow}) into the inclusion functor $\iota$ of its [[essential image]].

\end{proof}
\begin{prop}
\label{ModalOpIdempotent}\hypertarget{ModalOpIdempotent}{}
\textbf{([[modal operator]] is [[idempotent]])}

Let $\mathcal{D}$ be a [[category]] (Def. \ref{Categories}).

For $\bigcirc$ a [[modal operator]] on $\mathcal{D}$, with unit $\eta$ (Def. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}), it is \emph{[[idempotent monad|idempotent]]}, in that it is [[natural isomorphism|naturally isomorphic]] (Def. \ref{NaturalTransformations}) to the [[composition]] with itself:

\begin{displaymath}
\bigcirc \;\simeq\; \bigcirc \bigcirc
  \,.
\end{displaymath}
In fact, the image under $\bigcirc$ of its unit is such an isomorphism

\begin{displaymath}
\bigcirc\left( X \overset{\eta_X}{\to} \bigcirc X \right)
  \;\;\colon\;\;
  \bigcirc X
    \overset{\simeq}{\longrightarrow}
  \bigcirc ( \bigcirc X )
\end{displaymath}
as is its unit on its image

\begin{displaymath}
\eta_{\bigcirc X}
  \;\;\colon\;\;
  \bigcirc X
    \overset{\simeq}{\longrightarrow}
  \bigcirc ( \bigcirc X )
  \,.
\end{displaymath}
[[formal dual|Formally dually]], for $\Box$ a [[comodal operator]] on $\mathcal{D}$, with counit $\epsilon$ (Def. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}), it is \emph{[[idempotent monad|idempotent]]}, in that it is [[natural isomorphism|naturally isomorphic]] (Def. \ref{NaturalTransformations}) to the [[composition]] with itsef:

\begin{displaymath}
\Box \circ \Box
  \;\simeq\;
  \Box
  \,.
\end{displaymath}
In fact, the image under $\Box$ of its counit is such an isomorphism

\begin{displaymath}
\Box\left(  \Box X \overset{\epsilon_X}{\to} X \right)
  \;\;\colon\;\;
  \Box (\Box X)
    \overset{\simeq}{\longrightarrow}
  \Box X
\end{displaymath}
as is its counit on its image

\begin{displaymath}
\epsilon_{\Box X}
  \;\;\colon\;\;
  \Box ( \Box X )
    \overset{\simeq}{\longrightarrow}
  \Box X
  \,.
\end{displaymath}
\end{prop}
\begin{proof}
We discuss the first case, the second is [[formal dual|formally dual]] (Example \ref{OppositeCategory}).

By Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}, the modal operator is equivalent to the composite $\iota \circ L$ obtained from the [[reflective subcategory]]-inclusion (Def. \ref{ReflectiveSubcategory}) of its [[essential image]] of [[modal objects]]:

\begin{displaymath}
Im(\bigcirc)
    \underoverset
      {\underset{\phantom{AA}\iota \phantom{AA}}{\hookrightarrow}}
      {\overset{\phantom{AA}L \phantom{AA} }{\longleftarrow}}
      {\bot}
  \mathcal{D}
  \,.
\end{displaymath}
and its unit is the corresponding [[adjunction unit]] (Def. \ref{AdjunctionUnitFromHomIsomorphism})

\begin{displaymath}
X \overset{\eta_X}{\longrightarrow} \iota \circ L
  \,.
\end{displaymath}
Hence it is sufficient to show that the morphisms and $L( \eta_X )$ and $\eta_{\iota Y}$ are isomorphisms.

Now, the [[triangle identities]] \eqref{TriangleIdentities} for the [[adjunction]] $L \dashv \iota$, which hold by Prop. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}, say that their [[composition]] with the [[adjunction counit]] is the [[identity morphism]]

\begin{displaymath}
\epsilon_{L(\eta_X)} \circ L(\eta_X)
  \;=\;
  id_{L(X)}
  \phantom{AA} \text{and} \phantom{AA}
  \iota( \epsilon_Y )\circ \eta_{\iota(Y)}
  \;=\;
  id_{\iota(Y)}
  \,.
\end{displaymath}
But by Prop. \ref{FullyFaithfulAndInvertibleAdjoints}, the counit $\epsilon$ is a [[natural isomorphism]], since $\iota$ is [[fully faithful functor|fully faithful]]. Hence we may cancel it on both sides of the [[triangle identities]] and find that $L(\eta_X)$ and $\eta_{\iota(Y)}$ are indeed isomorphisms.

\end{proof}
\begin{defn}
\label{ModalObjects}\hypertarget{ModalObjects}{}
\textbf{([[modal objects]])}

Let $\mathcal{D}$ be a [[category]] (Def. \ref{Categories}).

For $\bigcirc$ a [[modal operator]] on $\mathcal{D}$ (Def. \ref{ModalOperator}), we say:

\begin{enumerate}%
\item a \emph{$\bigcirc$-[[modal object]]} is an [[object]] $X \in \mathcal{D}$ such that the following conditions hold (which are all equivalent, by Prop. \ref{ModalOpIdempotent}):

\begin{itemize}%
\item it is in the $\bigcirc$-[[essential image]]: $X \in Im( \bigcirc ) \hookrightarrow \mathcal{D}$,


\item it is isomorphic to its own $\bigcirc$-[[image]]: $X \simeq \bigcirc X$,


\item specifically its $\bigcirc$-unit is an [[isomorphism]] $\eta_X \;\colon\; X \overset{\simeq}{\to} \bigcirc X$.



\end{itemize}

\item a \emph{$\bigcirc$-[[modal object|submodal object]]} is an [[object]] $X \in \mathcal{D}$, such that

\begin{itemize}%
\item its $\bigcirc$-unit is a [[monomorphism]] (Def. \ref{Monomorphism}): $\eta_X \;\colon\; X \hookrightarrow \bigcirc X$.

\end{itemize}


\end{enumerate}
[[formal duality|Dually]] (Example \ref{OppositeCategory}):

For $\Box$ a [[comodal operator]] on $\mathcal{D}$ (Def. \ref{ModalOperator}), we say:

\begin{enumerate}%
\item a \emph{$\Box$-[[comodal object]]} is an [[object]] $X \in \mathcal{D}$ such that the following conditions hold (which are all equivalent, by Prop. \ref{ModalOpIdempotent}):

\begin{itemize}%
\item it is in the $\Box$-[[essential image]]: $X \in Im( \Box ) \hookrightarrow \mathcal{D}$,


\item it is isomorphic to its own $\Box$-[[image]]: $\Box X \simeq X$,


\item specifically its $\Box$-counit is an [[isomorphism]] $\epsilon_X \;\colon\; \Box X \overset{\simeq}{\longrightarrow} X$



\end{itemize}

\item a \emph{$\Box$-[[comodal object|supcomodal object]]} is an [[object]] $X \in \mathcal{D}$, such that

\begin{itemize}%
\item its $\Box$-counit is an [[epimorphism]] (Def. \ref{Monomorphism}): $\epsilon_X \;\colon\; \Box X \overset{epi}{\longrightarrow} X$.

\end{itemize}


\end{enumerate}
\end{defn}
\begin{defn}
\label{AdjointModality}\hypertarget{AdjointModality}{}
\textbf{([[adjoint modality]])}

Let

\begin{displaymath}
L \;\dashv\; C \;\dashv\; R
  \;\colon\;
  \mathcal{C}
    \itexarray{
      \overset{\phantom{A} L \phantom{A}}{\hookleftarrow}
      \\
      \overset{\phantom{A} C \phantom{A}}{\longrightarrow}
      \\
      \overset{\phantom{A} R \phantom{A}}{\hookleftarrow}
    }
  \mathcal{D}
\end{displaymath}
be an [[adjoint triple]] (Remark \ref{AdjointTriples}) such that $L$ and $R$ are [[fully faithful functors]] (necessarily both, by Prop. \ref{FullyFaithfulAdjointTriple}). By Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}, there are induced [[modal operators]]

\begin{displaymath}
\Box \;\coloneqq\; L \circ C
  \phantom{AA}
  \bigcirc \;\coloneqq\; R \circ C
\end{displaymath}
which themselves form am [[adjoint pair]]

\begin{displaymath}
\Box \;\dashv\; \bigcirc
  \,,
\end{displaymath}
hence called an \emph{[[adjoint modality]]}. The [[adjunction unit]] and [[adjunction counit]] as in \eqref{OppositeExtremesAdjointTriple} may now be read as exhibiting each object $X$ in the [[domain]] of $C$ as ``in between the opposite extremes of its $\bigcirc$-modal aspect and its $\Box$-modal aspect''

\begin{displaymath}
\Box X
    \overset{\phantom{AA}\epsilon^\Box_X \phantom{AA}}{\longrightarrow}
  X
    \overset{\phantom{AA}\eta^{\bigcirc}_X\phantom{AA}}{\longrightarrow}
  \bigcirc X
  \,.
\end{displaymath}
A [[formal duality|formally dual]] situation (Example \ref{OppositeCategory}) arises when $C$ is [[fully faithful functor|fully faithful]].

\begin{displaymath}
L \;\dashv\; C \;\dashv\; R
  \;\colon\;
  \mathcal{C}
    \itexarray{
      \overset{\phantom{A} L \phantom{A}}{\longrightarrow}
      \\
      \overset{\phantom{A} C \phantom{A}}{\hookleftarrow}
      \\
      \overset{\phantom{A} R \phantom{A}}{\longrightarrow}
    }
  \mathcal{D}
\end{displaymath}
with

\begin{displaymath}
\left(
    \bigcirc \;\coloneqq\; C \circ L
  \right)
  \;\dashv\;
  \left(
    \Box \;\coloneqq\; C \circ R
  \right)
\end{displaymath}
and canonical [[natural transformation]] between opposite extreme aspects given by

\begin{equation}
\Box X 
     \overset{ \phantom{AA} \epsilon^{\Box}_X \phantom{AA} }{\longrightarrow}
   X
    \overset{ \phantom{AA} \eta^{\bigcirc}_X \phantom{AA} }{\longrightarrow}
   \bigcirc X
\label{OppositeExtrmeComparison}\end{equation}
\end{defn}
\begin{prop}
\label{FullyFaithfulAdjointTriple}\hypertarget{FullyFaithfulAdjointTriple}{}
\textbf{([[fully faithful functor|fully faithful]] [[adjoint triple]])}

Let $L \dashv C \dashv R$ be an [[adjoint triple]] (Remark \ref{AdjointTriples}). Then the following are equivalent:

\begin{enumerate}%
\item $L$ is a [[fully faithful functor]];


\item $R$ is a [[fully faithful functor]],


\item $(\Box \;\coloneqq\; L \circ C) \dashv (\bigcirc \;\coloneqq\; R \circ C)$ is an [[adjoint modality]] (Def. \ref{FullyFaithfulAdjointTriple}).



\end{enumerate}
\end{prop}
For \textbf{proof} see \href{adjoint+triple#FullyFaithful}{this prop.}.

In order to analyze (in Prop. \ref{ComparisonMorphismBetweenOppositeExtremes} below) the comparison morphism of opposite extreme aspects \eqref{OppositeExtrmeComparison} induced by an [[adjoint modality]] (Def. \ref{AdjointModality}), we need the following technical Lemma:

\begin{lemma}
\label{CoincidenceOfTransformsForAdjointTriple}\hypertarget{CoincidenceOfTransformsForAdjointTriple}{}
Let

\begin{displaymath}
\mathcal{C}
    \itexarray{
      \overset{ \phantom{A} L \phantom{A} }{\longrightarrow}
      \\
      \overset{ \phantom{A} C \phantom{A} }{\hookleftarrow}
      \\
      \overset{ \phantom{A} R \phantom{A} }{ \longrightarrow }
    }
  \mathcal{D}
\end{displaymath}
be an [[adjoint triple]] with induced [[adjoint modality]] (Def. \ref{AdjointModality}) to be denoted

\begin{displaymath}
\left( \Box \;\coloneqq\; C \circ R\right)
  \;\dashv\;
  \left(
    \bigcirc \;\coloneqq\; C \circ L
  \right)
\end{displaymath}
Denoting the [[adjunction units]]/[[adjunction counit|counits]] (Def. \ref{AdjunctionUnitFromHomIsomorphism}) as

\newline | $\phantom{A}$ $(L \dashv C)$ $\phantom{A}$ | $\phantom{A}$ $\eta^{\bigcirc}$ $\phantom{A}$ | $\phantom{A}$ $\epsilon^{\bigcirc}$ $\phantom{A}$ | | $\phantom{A}$ $(C \dashv R)$ $\phantom{A}$ | $\phantom{A}$ $\eta^\Box$ $\phantom{A}$ | $\phantom{A}$ $\epsilon^\Box$ $\phantom{A}$ |

we have that the following [[composition|composites]] of unit/counit components are equal:

\begin{equation}
\left(
    \eta^{\Box}_{L X}
  \right)
  \circ
  \left(
    L \epsilon^\Box_X
  \right)
  \;\;=\;\;
  \left(
    R \eta^{\bigcirc}_{X}
  \right)
  \circ
  \left(
    \epsilon^{\bigcirc}_{R X}
  \right)
  \phantom{AAAAAA}
  \itexarray{
    L C R X
    &\overset{\epsilon^{\bigcirc}_{R X}}{\longrightarrow}&
    R X
    \\
    {}^{ \mathllap{ L \epsilon^\Box_X } }\big\downarrow
    &&
       \big\downarrow^{\mathrlap { R \eta^{\bigcirc}_{X} } }
    \\
    L X
    &\underset{ \eta^\Box_{L X} }{\longrightarrow}&
    R C L X
  }
\label{CoincidenceOfNaturalTransformationsForAdjointTriple}\end{equation}
\end{lemma}
(\href{adjoint+quadruple#Johnstone11}{Johnstone 11, lemma 2.1})

\begin{proof}
We claim that the following [[commuting diagram|diagram commutes]] (Def. \ref{CommutingDiagram}):

\begin{displaymath}
\itexarray{
    && && R X
    \\
    && & {}^{ \epsilon^\bigcirc_{R X} }\nearrow
    && \searrow^{\mathrlap{ R \eta^{\bigcirc}_X }}
    \\
    && L C R X
    && && R C L X
    \\
    & {}^{ L \epsilon^\Box_X }\swarrow
    && \searrow^{ \mathrlap{ L C R \eta^{\bigcirc}_X } }
    && {}^{\mathllap{ \eta^{\bigcirc}_{R C L X} }}\nearrow
    && \nwarrow^{ \mathrlap{ \eta^{\Box}_{L X} } }
    \\
    L X
    && && L C R C L X
    && && L X
    \\
    & {}_{\mathllap{ L \eta^{\bigcirc}_X }}\searrow
    && {}^{\mathllap{iso}}\swarrow_{\mathrlap{ L \epsilon^{\Box}_{C L X} }}
    && {}_{\mathllap{ L C \eta^\Box_{L X} }}\nwarrow^{\mathrlap{iso}}
    && \nearrow_{\mathrlap{ \epsilon^{\bigcirc}_{L X} }}
    \\
    && L C L X
    && \underset{id_{L C L X}}{\longleftarrow}  &&
    L C L X
  }
\end{displaymath}
This commutes, because:

\begin{enumerate}%
\item the left square is the image under $L$ of [[naturality square|naturality]] \eqref{Naturality} for $\epsilon^\Box$ on $\eta^{\bigcirc}_X$;


\item the top square is [[naturality square|naturality]] \eqref{Naturality} for $\epsilon^{\bigcirc}$ on $R \eta^{\bigcirc}_X$;


\item the right square is [[naturality square|naturality]] \eqref{Naturality} for $\epsilon^{\bigcirc}$ on $\eta^{\Box}_{L X}$;


\item the bottom commuting triangle is the image under $L$ of the [[triangle identity]] \eqref{TriangleIdentities} for $(C \dashv R)$ on $L X$.



\end{enumerate}
Moreover, notice that

\begin{enumerate}%
\item the total bottom composite is the [[identity morphism]] $id_{L X}$, due to the [[triangle identity]] \eqref{TriangleIdentities} for $(C \dashv R)$;


\item also the other two morphisms in the bottom triangle are [[isomorphisms]], as shown, due to the [[idempotent monad|idempoency]] of the $(C-R)$-adjunction (Prop. \ref{ModalOpIdempotent}.)



\end{enumerate}
Therefore the total composite from $L C R X \to R/ C L X$ along the bottom part of the diagram equals the left hand side of \eqref{CoincidenceOfNaturalTransformationsForAdjointTriple}, while the composite along the top part of the diagram clearly equals the right hand side of \eqref{CoincidenceOfNaturalTransformationsForAdjointTriple}.

\end{proof}
\begin{prop}
\label{ComparisonMorphismBetweenOppositeExtremes}\hypertarget{ComparisonMorphismBetweenOppositeExtremes}{}
\textbf{(comparison transformation between opposite extremes of [[adjoint modality]])}

Consider an [[adjoint triple]] of the form

\begin{displaymath}
L \dashv C \dashv R 
  \;\;\colon\;\;
  \mathcal{C}
    \itexarray{
      \overset{\phantom{AA} L \phantom{AA} }{\longrightarrow}
      \\
      \overset{\phantom{AA} C \phantom{AA} }{\hookleftarrow}
      \\
      \overset{\phantom{AAA} R \phantom{AAA} }{\longrightarrow}
    }
  \mathcal{B}
\end{displaymath}
with induced [[adjoint modality]] (Def. \ref{AdjointModality}) to be denoted

\begin{displaymath}
\left( 
    \Box \;\coloneqq\; C \circ R 
  \right)
  \;\dashv\;
  \left(
    \bigcirc \;\coloneqq\; C \circ L 
  \right)
\end{displaymath}
Denoting the [[adjunction units]]/[[adjunction counit|counits]] (Def. \ref{AdjunctionUnitFromHomIsomorphism}) as

\newline | $\phantom{A}$ $(L \dashv C)$ $\phantom{A}$ | $\phantom{A}$ $\eta^{\bigcirc}$ $\phantom{A}$ | $\phantom{A}$ $\epsilon^{\bigcirc}$ $\phantom{A}$ | | $\phantom{A}$ $(C \dashv E)$ $\phantom{A}$ | $\phantom{A}$ $\eta^\Box$ $\phantom{A}$ | $\phantom{A}$ $\epsilon^\Box$ $\phantom{A}$ |

Then for all $X \in \mathcal{C}$ the following two [[natural transformations]], constructed from the [[adjunction units]]/[[adjunction counit|counits]] (Def. \ref{AdjunctionUnitFromHomIsomorphism}) and their [[inverse morphisms]] (using [[idempotent monad|idempotency]], Prop. \ref{ModalOpIdempotent}), are equal:

\begin{equation}
comp_{\mathcal{B}}
  \;\;\coloneqq\;\;
  \left(
    L \epsilon^\Box_X
  \right)
  \circ
  \left(
    \eta^{\bigcirc}_{R X}
  \right)^{-1}
  \;\;=\;\;
  \left(
    \eta^\Box_{L X}
  \right)^{-1}
  \circ
  \left(
    \Gamma \eta^{\bigcirc}_X
  \right)
  \phantom{AAAAAAA}
  \itexarray{
    \Gamma X 
    & \overset{
       \Gamma \eta^{\bigcirc}_X
   }{\longrightarrow} & 
   R C L X
   \\
   {}^{ \mathllap{
      \left(
       \eta^{\bigcirc}_{R X}
     \right)^{-1}    
   } }\big\downarrow 
     & \searrow^{ { comp_{\mathcal{B}} }  } & 
   \big\downarrow^{ \mathrlap{  
     \left(
       \eta^\Box_{L X}
     \right)^{-1}
   } }
   \\ 
   L C R X
   &\underset{ 
    L \epsilon^\Box_X
    }{\longrightarrow}&
   L X
  }
\label{PointsToPiecesInTheBase}\end{equation}
Moreover, the image of these morphisms under $C$ equals the following composite:

\begin{equation}
comp_{\mathcal{C}}
  \;\colon\;
  \Box X 
    \overset{ \phantom{A} \epsilon^{\Box}_X \phantom{A} }{\longrightarrow}
  X
    \overset{ \phantom{A} \eta^{\bigcirc}_X \phantom{A} }{\longrightarrow}
  \bigcirc X
  \,,
\label{PointsToPieces}\end{equation}
hence

\begin{equation}
comp_{\mathcal{C}} \;=\; C(comp_{\mathcal{B}})
  \,.
\label{PiecesToPointsFromBase}\end{equation}
\end{prop}
\begin{proof}
The first statement follows directly from Lemma \ref{CoincidenceOfTransformsForAdjointTriple}.

For the second statement, notice that the $(C \dashv R)$-[[adjunct]] (Prop. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}) of

\begin{displaymath}
comp_{\mathcal{C}}
    \;\colon\;
  C R X 
    \overset{ \phantom{A} \epsilon^{\Box}_X \phantom{A} }{\longrightarrow}
  X
    \overset{ \phantom{A} \eta^{\bigcirc}_X \phantom{A} }{\longrightarrow}
  C L X
\end{displaymath}
is

\begin{equation}
\widetilde{ comp_{\mathcal{C}} }
  \;\;=\;\;
  \underset{
    = id_{R X}
  }{
  \underbrace{
    \Gamma X
      \underoverset{iso}{ \phantom{A} \eta^{\Box}_{R X} \phantom{A} }{ \longrightarrow }
    R C R X 
      \underoverset{iso}{ \phantom{A} \Gamma \epsilon^{\Box}_X \phantom{A} }{\longrightarrow}
    R X
  }}
      \overset{ \phantom{A} R \eta^{\bigcirc}_X \phantom{A}  }{\longrightarrow}
    R C L X
  \,,
\label{AdjunctOfptpH}\end{equation}
where under the braces we uses the [[triangle identity]] (Prop. \ref{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat}).

(As a side remark, for later usage, we observe that the morphisms on the left in \eqref{AdjunctOfptpH} are [[isomorphisms]], as shown, by [[idempotent monad|idempotency]] of the adjunctions.)

From this we obtain the following [[commuting diagram]]:

\begin{displaymath}
\itexarray{
    C R X
      &\overset{ \phantom{A} C R \eta^{\bigcirc}_X \phantom{A} }{\longrightarrow}&
    C R C L X
      &\underoverset{iso}{ \phantom{A} C \left(\eta^{ \Box }_{L X}\right)^{-1} \phantom{A} }{ \longrightarrow }&
    C L X
    \\
    &{}_{\mathllap{ comp_{\mathcal{C}} }}\searrow&
    {}^{ \mathllap{ \epsilon^{\Box}_{C L X} } }
    \big\downarrow^{\mathrlap{\simeq}}
     & 
    \nearrow_{\mathrlap{id_{L X}}}
    \\
    && C L X
  }
\end{displaymath}
Here:

\begin{enumerate}%
\item on the left we identified $\widetilde {\widetilde {comp_{\mathcal{C}}}} \;=\;  comp_{\mathcal{C}}$ by applying the formula (Prop. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}) for $(C \dashv R)$-[[adjuncts]] to $\widetilde {comp_{\mathcal{C}}} = R \eta^{\bigcirc}_X$ \eqref{AdjunctOfptpH};


\item on the right we used the [[triangle identity]] (Prop. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}) for $(C \dashv R)$.



\end{enumerate}
This proves the second statement.

\end{proof}
\begin{defn}
\label{PreorderOnModalities}\hypertarget{PreorderOnModalities}{}
\textbf{([[preorder]] on [[modalities]])}

Let $\bigcirc_1$ and $\bigcirc_2$ be two [[modal operators]] on a [[category]] $\mathcal{C}$. By Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories} these are equivalently characterized by their [[reflective subcategory|reflective]] [[full subcategories]] $\mathcal{C}_{\bigcirc_1}, \mathcal{C}_{\bigcirc}_2 \hookrightarrow \mathcal{C}$ of [[modal objects]].

There is an evident [[preorder]] on [[full subcategories]] of $\mathcal{C}$, given by full inclusions of full subcategories into each other. We write $\mathcal{C}_{\bigcirc_1} \subset \mathcal{C}_{\bigcirc_2}$ if the full subcategory on the left is contained, as a full subcategory of $\mathcal{C}$, in that on the right. Via prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories} there is the induced [[preorder]] on [[modal operators]], and we write

\begin{displaymath}
\bigcirc_1
  \;\lt\;
  \bigcirc_2
  \phantom{AA}
  iff
  \phantom{AA}
  \mathcal{C}_{\bigcirc_1}
  \;\subset\;
  \mathcal{C}_{\bigcirc_2}
  \,.
\end{displaymath}
There is an analogous [[preorder]] on [[comodal operators]] (Def. \ref{ModalOperator}).

If we have two [[adjoint modalities]] (Def. \ref{AdjointModality}) of the same type (both modal left adjoint or both comodal left adjoint) such that both the modalities and the comodalities are compatibly ordered in this way, we denote this situation as follows:

\begin{displaymath}
\itexarray{
    \bigcirc_2 &\dashv& \Box_2
    \\
    \vee && \vee
    \\
    \bigcirc_1 &\dashv& \Box_1
  }
  \phantom{AAAA} \text{or} \phantom{AAAA}
  \itexarray{
    \Box_2 &\dashv& \bigcirc_2
    \\
    \vee && \vee
    \\
    \Box_1 &\dashv& \bigcirc_1
  }
\end{displaymath}
etc.

\end{defn}
\begin{example}
\label{InitialAndFinalAdjointModality}\hypertarget{InitialAndFinalAdjointModality}{}
\textbf{([[bottom]] and [[top]] [[adjoint modality]])}

Let $\mathcal{C}$ be a [[category]] with both an [[initial object]] $\emptyset$ and a [[terminal object]] $\ast$ (Def. \ref{InitialObject}). Then, by Example \ref{InitialAndTerminalObjectInTermsOfAdjunction} there is an [[adjoint triple]] between $\mathcal{C}$ and the [[terminal category]] $\ast$ (Example \ref{InitialCategoryAndTerminalCategory}) of the form

\begin{displaymath}
\mathcal{C}
    \itexarray{
      \overset{ \phantom{A} const_\emptyset \phantom{A} }{\hookleftarrow}
      \\
      \overset{\phantom{AAAA}}{\longrightarrow}
      \\
      \overset{ \phantom{A} const_\ast \phantom{A} }{\hookleftarrow}
    }
  \ast
  \,.
\end{displaymath}
The induced [[adjoint modality]] (Def. \ref{AdjointModality}) is

\begin{displaymath}
const_{\emptyset}
  \;\dashv\;
  const_\ast
  \;\;\colon\;\;
  \mathcal{C} \to \mathcal{C}
  \,.
\end{displaymath}
By slight abuse of notation, we will also write this as

\begin{equation}
\emptyset
    \;\dashv\;
  \ast
  \;\;\colon\;\;
  \mathcal{C} \to \mathcal{C}
  \,.
\label{BottomAdjointModality}\end{equation}
On the other extreme, for $\mathcal{C}$ any [[category]] whatsoever, the [[identity]] functor on it is [[adjoint functor]] to itself, and constitutes an [[adjoint modality]] (Def. \ref{AdjointModality})

\begin{equation}
id_{\mathcal{C}}
  \;\dashv\;
  id_{\mathcal{C}}
  \;\;\colon\;\;
  \mathcal{C} \to \mathcal{C}
  \,.
\label{AdjointModalityTop}\end{equation}
Here

\begin{enumerate}%
\item \eqref{BottomAdjointModality} is the \emph{[[bottom]]} (or \emph{ground})


\item \eqref{AdjointModalityTop} is the \emph{[[top]]}



\end{enumerate}
in the [[preorder]] on [[adjoint modalities]] according to Def. \ref{PreorderOnModalities}, in that for every [[adjoint modality]] of the form $\bigcirc \dashv \Box$ we have the following:

\begin{displaymath}
\itexarray{
    id &\dashv& id
    \\
    \vee && \vee
    \\
    \Box &\dashv& \bigcirc
    \\
    \vee && \vee
    \\
    \emptyset &\dashv& \ast
  }
\end{displaymath}
\end{example}
\begin{defn}
\label{Aufhebung}\hypertarget{Aufhebung}{}
\textbf{([[Aufhebung]])}

On some [[category]] $\mathcal{C}$, consider an inclusion of [[adjoint modalities]], according to Def. \ref{PreorderOnModalities}:

\begin{displaymath}
\itexarray{
    \Box_1 &\dashv& \bigcirc_2
    \\
    \vee && \vee
    \\
    \Box_1 &\dashv& \bigcirc_1
  }
\end{displaymath}
We say:

\begin{enumerate}%
\item This provides \emph{right [[Aufhebung]] of the opposition} exhibited by $\box_1 \dashv \bigcirc_1$ if there is also the diagonal inclusion

\begin{displaymath}
\box_1 \lt \bigcirc_2
  \phantom{AAA}
  equivalently
  \phantom{AAA}
  \mathcal{C}_{\Box_1}
  \subset
  \mathcal{C}_{\bigcirc_2}
\end{displaymath}
We indicate this situation by

\begin{displaymath}
\itexarray{
    \Box_2 &\dashv& \bigcirc_2
    \\
    \vee &/& \vee
    \\
    \Box_1 &\dashv& \bigcirc_1
  }
\end{displaymath}

\item This provides \emph{left [[Aufhebung]] of the opposition} exhibited by $\box_1 \dashv \bigcirc_1$ if there is also the diagonal inclusion

\begin{displaymath}
\bigcirc_1 \lt \Box_2
  \phantom{AAA}
  equivalently
  \phantom{AAA}
  \mathcal{C}_{\bigcirc_1}
  \subset
  \mathcal{C}_{\Box_2}
\end{displaymath}
We indicate this situation by

\begin{displaymath}
\itexarray{
    \Box_2 &\dashv& \bigcirc_2
    \\
    \vee &\backslash& \vee
    \\
    \Box_1 &\dashv& \bigcirc_1
  }
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{remark}
\label{TrivialAufhebung}\hypertarget{TrivialAufhebung}{}
For a progression of [[adjoint modalities]] of the form

\begin{displaymath}
\itexarray{
     \bigcirc_2 &\dashv& \Box_2
     \\
     \vee && \vee
     \\
     \bigcirc_1 &\dashv& \Box_1
   }
\end{displaymath}
the analog of [[Aufhebung]] (Def. \ref{Aufhebung}) is automatic, since, by Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}, in this situation the [[full subcategories]] [[modal objects]] at each stage coincide already.

For emphasis we may denote this situation by

\begin{displaymath}
\itexarray{
     \bigcirc_2 &\dashv& \Box_2
     \\
     \vee &\vert& \vee
     \\
     \bigcirc_1 &\dashv& \Box_1
   }
  \,.
\end{displaymath}
\end{remark}
\begin{example}
\label{}\hypertarget{}{}
\textbf{([[top]] [[adjoint modality]] provides [[Aufhebung]] of all oppositions)}

For $\mathcal{C}$ any [[category]], the [[top]] [[adjoint modality]] $id \dashv id$ (Def. \ref{InitialAndFinalAdjointModality}) provides [[Aufhebung]] (Def. \ref{Aufhebung}) of every other [[adjoint modality]].

\end{example}
But already [[Aufhebung]] of the [[bottom]] [[adjoint modality]] is a non-trivial and interesting condition. We consider this below in Prop. \ref{PiecesHavePoints}.

$\,$

We now re-consider the concept of [[reflective subcategories]] from the point of view of [[localization of categories]]:

\begin{defn}
\label{CategoryWithWeakEquivalences}\hypertarget{CategoryWithWeakEquivalences}{}
\textbf{([[category with weak equivalences]])}

A \emph{[[category with weak equivalences]]} is

\begin{enumerate}%
\item a [[category]] $\mathcal{C}$ (Def. \ref{Categories})


\item a [[subcategory]] $W \subset \mathcal{C}$ (i.e. sub-class of objects and morphisms that inherits the structure of a [[category]])



\end{enumerate}
such that the [[morphisms]] in $W$

\begin{enumerate}%
\item include all the [[isomorphisms]] of $\mathcal{C}$,


\item satisfy \emph{[[two-out-of-three]]}:

If for $g$, $f$ any two [[composition|composable]] [[morphisms]] in $\mathcal{C}$, two out of the set $\{g,\, f,\, g \circ f \}$ are in $W$, then so is the third.

\begin{displaymath}
\itexarray{
    & {}^{\mathllap{f}}\nearrow && \searrow^{\mathrlap{g}}
    \\
    && \underset{ g \circ f }{\longrightarrow}
  }
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{defn}
\label{LocalizationOfACategory}\hypertarget{LocalizationOfACategory}{}
\textbf{([[localization of a category]])}

Let $W \subset \mathcal{C}$ be a [[category with weak equivalences]] (Def. \ref{CategoryWithWeakEquivalences}). Then the \emph{[[localization of a category|localization]]} of $\mathcal{C}$ at $W$ is, if it exsists

\begin{enumerate}%
\item a [[category]] $\mathcal{C}[W^{-1}]$,


\item a [[functor]] $\gamma \;\colon\; \mathcal{C} \longrightarrow \mathcal{C}[W^{-1}]$ (Def. \ref{Functors})



\end{enumerate}
such that

\begin{enumerate}%
\item $\gamma$ sends all morphisms in $W \subset \mathcal{C}$ to [[isomorphisms]] (Def. \ref{Isomorphism}),


\item $\gamma$ is [[universal property|universal with this property]]: If $F \;\colon\; \mathcal{C} \longrightarrow \mathcal{D}$ is any functor with this property, then it factors through $\gamma$, up to [[natural isomorphism]] (Def. \ref{NaturalTransformations}):

\begin{displaymath}
F \;\simeq\;
  D F \circ \gamma
  \phantom{AAAAAAA}
  \itexarray{
    \mathcal{C}
      && \overset{F}{\longrightarrow} &&
    \mathcal{D}
    \\
    & {}_{\mathllap{\gamma}}\searrow
      &{}^{\rho}\Downarrow_{\simeq}&
    \nearrow_{\mathrlap{D F}}
    \\
    && \mathcal{C}[W^{-1}]
  }
\end{displaymath}
and any two such factorizations $D F$ and $D^' F$ are related by a unique [[natural isomorphism]] $\kappa$ compatible with $\rho$ and $\rho^'$:



\end{enumerate}
\begin{equation}
\itexarray{
       \mathcal{C}
         && \overset{F}{\longrightarrow} &&
       \mathcal{D}
       \\
       &
       {}_{\mathllap{\gamma}}\searrow
         &{}^{\rho}\Downarrow_{\simeq}&
       \nearrow_{\mathrlap{D F}}
       && \searrow^{\mathrlap{id}}
       \\
       && \mathcal{C}[W^{-1}]
       && {}_{\simeq}\seArrow^{\kappa} && \mathcal{D}
       \\
       && &  {}_{\mathllap{id}}\searrow && \swarrow_{\mathrlap{D^' F}}
       \\
       && && \mathcal{C}[W^{-1}]
     }
     \phantom{AAAA}
     =
     \phantom{AAAA}
     \itexarray{
       \mathcal{C}
         && \overset{F}{\longrightarrow} &&
       \mathcal{D}
       \\
       & {}_{\mathllap{\gamma}}\searrow
         &{}^{\rho^'}\Downarrow_{\simeq}&
       \nearrow_{\mathrlap{D^' F}}
       \\
       && \mathcal{C}[W^{-1}]
     }
\label{CompatibleNaturalIsoForLocalization}\end{equation}
Such a localization is called a \emph{[[reflective localization]]} if the localization functor has a [[fully faithful functor|fully faithful]] [[right adjoint]], exhibiting it as the reflection functor of a [[reflective subcategory]]-inclusion (Def. \ref{ReflectiveSubcategory})

\begin{displaymath}
\mathcal{C}[W^{-1}]
  \underoverset
    {\underset{\phantom{AAAA}}{\hookrightarrow}}
    {\overset{ \phantom{AA} \gamma \phantom{AA} }{\longleftarrow}}
    {\bot}
  \mathcal{C}
  \,.
\end{displaymath}
\end{defn}
\begin{prop}
\label{ReflectiveSubcategoriesAreLocalizations}\hypertarget{ReflectiveSubcategoriesAreLocalizations}{}
\textbf{([[reflective subcategories]] are [[localizations]])}

Every [[reflective subcategory]]-inclusion (Def. \ref{ReflectiveSubcategory})

\begin{displaymath}
\mathcal{C}_{L}
  \underoverset
    {\underset{\phantom{AA}\iota \phantom{AA}}{\hookrightarrow}}
    {\overset{ \phantom{AA} L \phantom{AA} }{\longleftarrow}}
    {\bot}
  \mathcal{C}
\end{displaymath}
is [[generalized the|the]] [[reflective localization]] (Def. \ref{LocalizationOfACategory}) at the class $W \coloneqq L^{-1}(Isos)$ of morphisms that are sent to isomorphisms by the reflector $L$.

\end{prop}
\begin{proof}
Let $F \;\colon\; \mathcal{C} \to \mathcal{D}$ be a [[functor]] which inverts morphisms that are inverted by $L$.

First we need to show that it factors through $L$, up to natural isomorphism. But consider the following [[whiskering]] of the [[adjunction unit]] $\eta$ (Def. \ref{AdjunctionUnitFromHomIsomorphism}) with $F$:

\begin{displaymath}
\itexarray{
    \mathcal{C}
    && \overset{F}{\longrightarrow} &&
    \mathcal{D}
    \\
    & {}_{\mathllap{L}}\searrow &\Downarrow& \nearrow_{\mathrlap{D F}}
    \\
    && \mathcal{C}_L
  }
  \phantom{AA} \coloneqq \phantom{AA}
  \itexarray{
    \mathcal{C}
      && \overset{id}{\longrightarrow} &&
    \mathcal{C}
      & \overset{F}{\longrightarrow}&
    \mathcal{D}
    \\
    & {}_{\mathllap{L}}\searrow &\Downarrow^{\eta}& \nearrow_{\mathrlap{\iota}}
    \\
    && \mathcal{C}_L
  }
\end{displaymath}
By [[idempotent monad|idempotency]] (Prop. \ref{ModalOpIdempotent}), the components of the [[adjunction unit]] $\eta$ are inverted by $L$, and hence by assumption they are also inverted by $F$, so that on the right the [[natural transformation]] $F(\eta)$ is indeed a [[natural isomorphism]].

It remains to show that this factorization is unique up to unique natural isomorphism. So consider any other factorization $D^' F$ via a natural isomorphism $\rho$. [[pasting|Pasting]] this now with the [[adjunction counit]]

\begin{displaymath}
\itexarray{
    &&
    \mathcal{C} && \overset{F}{\longrightarrow} &&  \mathcal{D}
    \\
    &
    {}^{\mathllap{\iota}}\nearrow
    &
    {}^{\epsilon}\Downarrow
    & {}_{\mathllap{L}}\searrow
    &\Downarrow^{\rho}& \nearrow_{\mathrlap{D^' F}}
    \\
    \mathcal{C}_L
    &&
      \underset{ id }{\longrightarrow}
    &&
    \mathcal{C}_L
  }
\end{displaymath}
exhibits a natural isomorphism $\epsilon \cdot \rho$ between $D F \simeq D^' F$. Moreover, this is compatible with $F(\eta)$ according to \eqref{CompatibleNaturalIsoForLocalization}, due to the [[triangle identity]] (Prop. \ref{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat}):

\begin{displaymath}
\itexarray{
    \mathcal{C}
    &&
     \overset{id}{\longrightarrow}
    &&
    \mathcal{C} && \overset{F}{\longrightarrow} &&  \mathcal{D}
    \\
    &
      {}_{\mathllap{id}}\searrow
    &
    {}^{\mathllap{\eta}}\Downarrow
    &
    {}^{\mathllap{\iota}}\nearrow
    &
    {}^{\epsilon}\Downarrow
    & {}_{\mathllap{L}}\searrow
    &\Downarrow^{\rho}& \nearrow_{\mathrlap{D^' F}}
    \\
    &&
    \mathcal{C}_L
    &&
      \underset{ id }{\longrightarrow}
    &&
    \mathcal{C}_L
  }
  \phantom{AAAA}
  =
  \phantom{AAAA}
  \itexarray{
    \mathcal{C} && \overset{F}{\longrightarrow} &&  \mathcal{D}
    \\
    & \searrow &\Downarrow^\rho& \swarrow
    \\
    && \mathcal{C}_L
  }
\end{displaymath}
Finally, since $L$ is [[essentially surjective functor]], by [[idempotent monad|idempotency]] (Prop. \ref{AdjointnessInTermsOfHomIsomorphismEquivalentToAdjunctionInCat}), it is clear that this is the unique such natural isomorphism.

\end{proof}
\begin{defn}
\label{LocalObjects}\hypertarget{LocalObjects}{}
\textbf{([[local object]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}) and let $S \subset Mor_{\mathcal{C}}$ be a set of [[morphisms]]. Then an [[object]] $X \in \mathcal{C}$ is called an \emph{$S$-[[local object]]} if for all $A \overset{s}{\to} B \; \in S$ the [[hom-functor]] (Def. \ref{HomFunctor}) from $s$ into $X$ yields a [[bijection]]

\begin{displaymath}
Hom_{\mathcal{C}}(s,X)
  \;\colon\;
  Hom_{\mathcal{C}}(B,X)
   \overset{ \phantom{AA} \simeq \phantom{AA} }{\longrightarrow}
  Hom_{\mathcal{C}}(A,X)
  \,,
\end{displaymath}
hence if every morphism $A \overset{f}{\longrightarrow} X$ [[extension|extends]] uniquely along $w$ to $B$:

\begin{displaymath}
\itexarray{
    A &\overset{\phantom{A}f\phantom{A}}{\longrightarrow}& X
    \\
    {}^{\mathllap{w}}\big\downarrow & \nearrow_{\mathrlap{ \exists! }}
    \\
    B
  }
\end{displaymath}
We write

\begin{equation}
\mathcal{C}_S
  \overset{\phantom{AA}\iota\phantom{AA}}{\hookrightarrow}
  \mathcal{C}
\label{FullSubcategoryOfSLocalObjects}\end{equation}
for the [[full subcategory]] (Example \ref{FullSubcategoryOnClassOfObjects}) of $S$-local objects.

\end{defn}
\begin{defn}
\label{LocalizationAtACollectionOfMorphisms}\hypertarget{LocalizationAtACollectionOfMorphisms}{}
\textbf{([[reflective subcategory|reflection]] onto [[full subcategory]] of [[local objects]])}

Let $\mathcal{C}$ be a [[category]] and set $S \subset Mor_{\mathcal{C}}$ be a sub-[[class]] of its [[morphisms]]. Then the \emph{reflection onto local $S$-objects} (often just called ``localization at the collection $S$'' is, if it exists, a [[left adjoint]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}) $L$ to the [[full subcategory]]-inclusion of the $S$-[[local objects]] \eqref{FullSubcategoryOfSLocalObjects}:

\begin{displaymath}
\mathcal{C}_S
    \underoverset
      {\underset{\iota}{\hookrightarrow}}
      {\overset{\phantom{AA}L\phantom{AA}}{\longleftarrow}}
      {\bot}
  \mathcal{C}
  \,.
\end{displaymath}
\end{defn}
A class of examples is the following, which comes to its full nature (only) after passage to [[homotopy theory]] (Example \ref{HomotopyLocalizationOfCombinatorialModelCategories} below):

\begin{defn}
\label{HomotopyLocalizationOn1Categories}\hypertarget{HomotopyLocalizationOn1Categories}{}
\textbf{([[homotopy localization]] of [[1-categories]])}

Let $\mathcal{C}$ be a [[category]], let $\mathbb{A} \in \mathcal{C}$ be an [[object]], and consider the class of [[morphisms]] given by [[projection]] out of the [[Cartesian product]] with $\mathbb{A}$, of all objects $X \in \mathcal{C}$:

\begin{displaymath}
X \times \mathbb{A} 
    \overset{p_1}{\longrightarrow}
  X
  \,.
\end{displaymath}
If the corresponding [[reflective subcategory|reflection]] onto the [[full subcategory]] of [[local objects]] (Def. \ref{LocalizationAtACollectionOfMorphisms}) exists, we say this is \emph{[[homotopy localization]]} at that object , and denote the [[modal operator]] corresponding to this (via Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}) by

\begin{displaymath}
\bigcirc\!\!\!\!\!\!\!\!\mathbb{A}
  \;\colon\;
  \mathcal{C}
  \longrightarrow 
  \mathcal{C}
  \,.
\end{displaymath}
\end{defn}
\begin{prop}
\label{ReflectiveLocalizationGivenByLocalObjects}\hypertarget{ReflectiveLocalizationGivenByLocalObjects}{}
\textbf{([[reflective localization]] [[reflective subcategory|reflects]] onto [[full subcategory]] of [[local objects]])}

Let $W \subset \mathcal{C}$ be a [[category with weak equivalences]] (Def. \ref{CategoryWithWeakEquivalences}). If its [[reflective localization]] (Def. \ref{LocalizationOfACategory}) exists

\begin{displaymath}
\mathcal{C}[W^{-1}]
    \underoverset
      {\underset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow}}
      {\overset{ \phantom{AA} L \phantom{AA} }{\longleftarrow}}
      {\bot}
  \mathcal{C}
\end{displaymath}
then $\mathcal{C}[W^{-1}] \overset{\iota}{\hookrightarrow} \mathcal{C}$ is [[equivalence of categories|equivalently]] the inclusion of the [[full subcategory]] (Example \ref{FullSubcategoryOnClassOfObjects}) on the $W$-[[local objects]] (Def. \ref{LocalObjects}), and hence $L$ is equivalently reflection onto the $W$-local objects, according to Def. \ref{LocalizationAtACollectionOfMorphisms}.

\end{prop}
\begin{proof}
We need to show that

\begin{enumerate}%
\item every $X \in \mathcal{C}[W^{-1}] \overset{\iota}{\hookrightarrow} \mathcal{C}$ is $W$-[[local object|local]],


\item every $Y \in \mathcal{C}$ is $W$-[[local object|local]] precisely if it is [[isomorphism|isomorphic]] to an object in $\mathcal{C}[W^{-1}] \overset{\iota}{\hookrightarrow} \mathcal{C}$.



\end{enumerate}
The first statement follows directly with the [[adjoint functor|adjunction isomorphism]] \eqref{HomIsomorphismForAdjointFunctors}:

\begin{displaymath}
Hom_{\mathcal{C}}(w, \iota(X))
    \simeq
  Hom_{\mathcal{C}[W^{-1}]}(L(w), X)
\end{displaymath}
and the fact that the [[hom-functor]] takes [[isomorphisms]] to [[bijections]] (Example \ref{YonedaCharacterizationOfIsomorphism}).

For the second statement, consider the case that $Y$ is $W$-local. Observe that then $Y$ is also local with respect to the class

\begin{displaymath}
W_{sat} \;\coloneqq\; L^{-1}(Isos)
\end{displaymath}
of \emph{all} morphisms that are inverted by $L$ (the ``[[saturated class of morphisms]]''): For consider the [[hom-functor]] $\mathcal{C} \overset{Hom_{\mathcal{C}}(-,Y)}{\longrightarrow} Set^{op}$ to the [[opposite category|opposite]] of the [[category of sets]]. By assumption on $Y$ this takes elements in $W$ to isomorphisms. Hence, by the defining [[universal property]] of the [[localization]]-functor $L$, it factors through $L$, up to [[natural isomorphism]].

Since, by [[idempotent monad|idempotency]] (Prop. \ref{ModalOpIdempotent}), the [[adjunction unit]] $\eta_Y$ is in $W_{sat}$, this implies that we have a [[bijection]] of the form

\begin{displaymath}
Hom_{\mathcal{C}}( \eta_Y, Y )
  \;\colon\;
  Hom_{\mathcal{C}}( \iota L(Y), Y )
    \overset{\simeq}{\longrightarrow}
  Hom_{\mathcal{C}}(Y, Y)
  \,.
\end{displaymath}
In particular the [[identity morphism]] $id_Y$ has a [[preimage]] $\eta_Y^{-1}$ under this function, hence a [[left inverse]] to $\eta$:

\begin{displaymath}
\eta_Y^{-1} \circ \eta_Y \;=\; id_Y
  \,.
\end{displaymath}
But by [[2-out-of-3]] this implies that $\eta_Y^{-1} \in W_{sat}$. Since the first item above shows that $\iota L(Y)$ is $W_{sat}$-local, this allows to apply this same kind of argument again,

\begin{displaymath}
Hom_{\mathcal{C}}( \eta^{-1}_Y, \iota L(Y) )
    \;\colon\;
  Hom_{\mathcal{C}}( Y, \iota L(Y) )
    \overset{\simeq}{\longrightarrow}
  Hom_{\mathcal{C}}( \iota L(Y) , \iota L(Y))
  \,,
\end{displaymath}
to deduce that also $\eta_Y^{-1}$ has a [[left inverse]] $(\eta_Y^{-1})^{-1} \circ \eta_Y^{-1}$. But since a [[left inverse]] that itself has a [[left inverse]] is in fact an [[inverse morphisms]] (\href{retract#LeftInverseWithLeftInverseIsLeftInverse}{this Lemma}), this means that $\eta^{-1}_Y$ is an [[inverse morphism]] to $\eta_Y$, hence that $\eta_Y \;\colon\; Y \to \iota L (Y)$ is an [[isomorphism]] and hence that $Y$ is isomorphic to an object in $\mathcal{C}[W^{-1}] \overset{\iota}{\hookrightarrow} \mathcal{C}$.

Conversely, if there is an [[isomorphism]] from $Y$ to a morphism in the image of $\iota$ hence, by the first item, to a $W$-local object, it follows immediatly that also $Y$ is $W$-local, since the [[hom-functor]] takes [[isomorphisms]] to [[bijections]] and since bijections satisfy [[2-out-of-3]].

\end{proof}
\begin{prop}
\label{ReflectionOntoLocalObjectsIsLocalizationWithRespectToLeftAdjoints}\hypertarget{ReflectionOntoLocalObjectsIsLocalizationWithRespectToLeftAdjoints}{}
\textbf{([[reflective subcategory|reflection]] onto [[local objects]] is [[localization]] with respect to [[left adjoints]])}

Let $\mathcal{C}$ be a [[category]] (Def. \ref{Categories}) and let $S \subset Mor_{\mathcal{C}}$ be a [[class]] of [[morphisms]] in $\mathcal{C}$. Then the [[reflective subcategory|reflection]] onto the $S$-[[local objects]] (Def. \ref{LocalizationAtACollectionOfMorphisms}) satisfies, if it exists, the [[universal property]] of a [[localization of categories]] (Def. \ref{LocalizationOfACategory}) with respect to \emph{[[left adjoint]]} functors inverting $S$.

\end{prop}
\begin{proof}
Write

\begin{displaymath}
\mathcal{C}_S 
    \underoverset
      {\underset{ \phantom{AA}\iota\phantom{AA} }{\hookrightarrow}}
      {\overset{\phantom{AA}L\phantom{AA}}{\longleftarrow}}
      {\bot}
  \mathcal{C}
\end{displaymath}
for the [[reflective subcategory]]-inclusion of the $S$-[[local objects]].

Say that a [[morphism]] $f$ in $\mathcal{C}$ is an \emph{$S$-[[local morphism]]} if for every $S$-[[local object]] $A \in \mathcal{C}$ the [[hom-functor]] (Example \ref{HomFunctor}) from $f$ to $A$ yields a [[bijection]] $Hom_{\mathcal{C}}(f,A)$. Notice that, by the [[Yoneda embedding]] for $\mathcal{C}_S$ (Prop. \ref{YonedaEmbedding}), the $S$-[[local morphisms]] are precisely the morphisms that are taken to isomorphisms by the reflector $L$ (via Example \ref{YonedaCharacterizationOfIsomorphism}).

Now let

\begin{displaymath}
(F \dashv G)
  \;\colon\;
  \mathcal{C} 
    \underoverset
      {\underset{G}{\longleftarrow}}
      {\overset{ \phantom{AA} F \phantom{AA} }{\longrightarrow}}
      {\bot}
   \mathcal{D}
\end{displaymath}
be a pair of [[adjoint functors]], such that the [[left adjoint]] $F$ inverts the morphisms in $S$. By the adjunction hom-isomorphism \eqref{HomIsomorphismForAdjointFunctors} it follows that $G$ takes values in $S$-[[local objects]]. This in turn implies, now via the [[Yoneda embedding]] for $\mathcal{D}$, that $F$ inverts all $S$-[[local morphisms]], and hence all morphisms that are inverted by $L$.

Thus the essentially unique factorization of $F$ through $L$ now follows by Prop. \ref{ReflectiveSubcategoriesAreLocalizations}.

\end{proof}


\end{document}