← Notes on advances of LSC
Normalization operator Oldversions__20250418.tex
\documentclass{amsart}
\usepackage[left=2cm, right=2cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{amsfonts, amsthm, amssymb, mathtools,etoolbox}
\usepackage{blindtext}
\usepackage[colorlinks=true, urlcolor=blue, linkcolor=blue, citecolor=blue]{hyperref}
\usepackage{tikz,tikz-cd}
\usepackage{cleveref}
\usepackage{array}
\usepackage[style=alphabetic,sorting=nyt]{biblatex}
\renewbibmacro{in:}{}
% \addbibresource{biblio.bib}
\addbibresource{CommonBiblio20240922.bib}
\tikzset{pullback/.style={minimum size=1.2ex,path picture={
\draw[opacity=1,black,-,#1] (-0.5ex,-0.5ex) -- (0.5ex,-0.5ex) -- (0.5ex,0.5ex);%
}}}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{todo}[theorem]{Todo}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{fact}[theorem]{Fact}
\theoremstyle{definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{question}[theorem]{Question}
\newtheorem{idea}[theorem]{Idea}
\newcommand{\dq}[1]{``#1"}
\newcommand{\memo}[1]{\textcolor{red}{memo: #1}}
\newcommand{\invmemo}[1]{\textcolor{blue}{memo: #1}}
\newcommand{\para}[1]{\paragraph{\textbf{#1}}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Nor}{\mathrm{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\G}{\mathbb{G}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\ob}{\mathrm{ob}}
\newcommand{\true}{\mathrm{true}}
\newcommand{\Image}{\mathrm{Im}}
\newcommand{\Sub}{\mathrm{Sub}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\FinSet}{\mathbf{FinSet}}
\newcommand{\PSh}{\mathbf{PSh}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\sgt}{\{\cdot\}}
\newcommand{\Func}[2]{[#1,#2]}
\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\demph}[1]{\textit{#1}}
\font\maljapanese=dmjhira at 2.5ex
\newcommand{\yo}{\textrm{\!\maljapanese\char"48}}
\newcommand{\Stab}{\mathrm{Stab}}
\newcommand{\mono}{\mathrm{mono}}
\title{Normalization operator in a category and the local state classifier of hyperconnected quotient topoi}
\author{Ryuya Hora}
\thanks{Graduate School of Mathematical Sciences, University of Tokyo. \url{hora@ms.u-tokyo}}
% \date{\today}
\subjclass[2020]{18B25}
\keywords{Topos, normalization, hyperconnected geometric morphism, local state classifier}
\begin{document}
\begin{abstract}
This paper continues the author’s study of the colimit of all monomorphisms in a category, called the local state classifier $\Xi$, and its use in analyzing hyperconnected geometric morphisms from a given topos.
We first define a normalization operator $\Xi \to \Xi$ in any category that admits a local state classifier, in particular, in any Grothendieck topos. In the category of group actions for a group $G$, this operator coincides with the usual normalization operator receiving a subgroup $H\subset G$ and returning its normalizer subgroup $\Nor_G(H)\subset G$.
We then describe how to construct a local state classifier of a given hyperconnected quotient of a given topos.
% that has a local state classifier.
These results serve as preparation for a topos-theoretic study of regular languages, congruences of words, and syntactic monoids.
\end{abstract}
\maketitle
\tableofcontents
\section{Introduction}
Since \cite{johnstone1981factorization} introduced the notion of hyperconnected geometric morphism, topos theory has heavily utilized it. Referring to the terminology in \cite{lawvere2025open}, we call a hyperconnected geometric morphism from a topos $\E$ a \demph{hyperconnected quotient} of $\E$.
Following \cite{rosenthal1982quotient}, which describes hyperconnected quotients of a Grothendieck topos using generators, the author in \cite{hora2024internal} gives a new classification theorem for hyperconnected quotients, which applies to a broader class of topoi.
That paper introduces the notion of a \demph{local state classifier} $\Xi$ defined as the colimit of all monomorphisms \cite[][Definition 3.4]{hora2024internal}. The main theorem of the paper states that if a topos has a local state classifier $\Xi$, then hyperconnected quotients of $\E$ are in one-to-one correspondence with internal semilattice homomorphisms $\Xi \to \Omega$.
This provides a convenient way to classify all hyperconnected quotients of a given Grothendieck topos.
To utilize the classification theorem, we need to describe the local state classifier of a given Grothendieck topos. For a presheaf topos, it is easy to determine its local state classifier \cite[][Example 3.22.]{hora2024internal}.
However, it is not easy to describe a local state classifier of a non-presheaf topos.
The main theorem of the present paper provides a new method for describing the local state classifier of a hyperconnected quotient of a known topos. To prove the main theorem, we introduce the notion of \demph{normalization operator} $\xi_{\Xi}\colon \Xi \to \Xi$ in any category with a local state classifier $\Xi$. This abstractly defined operator coincides with the usual normalization of subgroups in the topos of group actions.
This work is motivated by research on topoi of automata. In automata theory, it is crucial to consider right congruences on the words $\Sigma^{\ast}$. The set of all right congruences provides the local state classifier of the topos $\PSh(\Sigma^*)$, and plays a central role in the ongoing theory of topoi of automata (especially for the theory of congruences and syntactic monoids). Here, since $\PSh(\Sigma^*)$ is a presheaf topos, it is easy to describe its local state classifier.
However, in order to capture finiteness related to algebraic language theory,
we need to consider the topoi of topological (or, in many cases, profinite) monoid actions (see \cite{hora2024topoi}), and its local state classifier.
Here, the main theorem of the present paper is useful, since every topos of topological monoid actions is a hyperconnected quotient of some monoid action topos, as studied in \cite{rogers2023toposes}.
\subsection*{Acknowledgement}
The author would like to thank his supervisor Ryu Hasegawa for helpful discussions and suggestions.
He was supported by JSPS KAKENHI Grant Number JP24KJ0837 and FoPM, WINGS Program, the University of Tokyo.
\section{Preliminaries: Hyperconnected quotients and local state classifier}\label{sec:Preliminaries}
\subsection{Hyperconnected quotients}
This subsection aims to recall the preliminaries
for hyperconnected geometric morphisms. See \cite{johnstone1981factorization} or \cite[][A.4.6]{johnstone2002sketchesv1} for more details. We will also explain the notion of local state classifier from \cite{hora2024internal}.
% \begin{definition}[Hyperconnected geometric morphisms]
% A geometric morphism $f\colon \E \to \F$ is \demph{hyperconnected} if it is connected (i.e. $f^{\ast}$ is fully faithful), and satisfies the following equivalent conditions
% \begin{itemize}
% \item The counit $\epsilon_X\colon f^{\ast}f_{\ast}\to \id_{\E}$ is monic.
% \item The essential image of $f^{\ast}$ is closed under taking subobjects.
% \item The essential image of $f^{\ast}$ is closed under taking subquotients.
% \end{itemize}
% \end{definition}
\begin{definition}[Hyperconnected geometric morphisms]
A geometric morphism $f\colon \E \to \F$ is said to be \demph{hyperconnected} if it is connected (i.e. $f^{\ast}\colon \F \to \E$ is fully faithful) and its counit $\epsilon_X\colon f^{\ast}f_{\ast}\to \id_{\E}$ is monic.
\end{definition}
In this paper, a \demph{hyperconnected quotiet} of a topos $\E$ means (an equivalence class of) a hyperconnected geometric morphism from $\E$.
Since $f^{\ast}$ is fully faithful for a hyperconnected quotient $f\colon \E \to \F$, we can regard $\F$ as a (replete) full subcategory of $\E$.
With this identification, we will write `$X\in \ob(\E)$ belongs to $\F$' for `$X\in \ob(\E)$ belongs to the essential image of $f^{\ast}$' in this paper. This does not cause a problem, since we will not distinguish two mutually equivalent hyperconnected quotients.
\subsection{Local state classifier}
In this subsection, we will briefly explain the notion of local state classifier. For more proofs, informal explanations, and examples, see the original article \cite{hora2024internal}.
\subsubsection{Definition}
\begin{definition}[{\cite[][Definition 3.4]{hora2024internal}}]
The \demph{local state classifier} of a category $\E$ is the colimit of all monomorphisms of $\E$, if it exists. In other words, it is an object $\Xi$ equipped with a family of morphisms $\{\xi_X \colon X \to \Xi\}_{X\in \ob(\E)}$, such that they form a colimit cocone under the faithful embedding functor $\E_{\mono}\rightarrowtail \E$.
\end{definition}
The definition of a local state classifier is quite transcendental, and even a (small) cocomplete category might not admit a local state classifier. However, we can prove the following proposition:
\begin{proposition}[{\cite[][Section 3.16.]{hora2024internal}}]\label{prop:ExistenceForGrothendieck}
Every Grothendieck topos $\E$ has a local state classifier.
\end{proposition}
\subsubsection{Inducing full subcategories}
% But
How is a local state classifier related to the classification of hyperconnected quotients? Since $\Xi$ is just an object of $\E$ and a hyperconnected quotient is a (very nice) subcategory of $\E$, they might seem unrelated.
The answer is, in short, that we can construct a full subcategory of $\E$ from any subobject of $\Xi$.
% Here is an answer:
Let $\E$ be a category with a local state classifier $\Xi$.
For any subobject $\iota_F\colon F \rightarrowtail\Xi$
% of the local state classifier of a category $\E$
, we can define a full subcategory $\E_F \hookrightarrow \E$ by
\begin{equation}\label{eq:FullSubCondition}
X\in \ob(\E_F)
\iff
\begin{tikzcd}
& F\ar[d, rightarrowtail, "\iota_F"]\\
X\ar[r,"\xi_X"']\ar[ru, dashed, "\exists"]&\Xi.
\end{tikzcd}
\end{equation}
% \[
% X\in \ob(\E_F)
% \iff
% \begin{tikzcd}
% & F\ar[d, rightarrowtail]\\
% X\ar[r,"\xi_X"']\ar[ru, dashed, "\exists"]&\Xi.
% \end{tikzcd}
% \]
In other words, we define the full subcategory $\E_F$ of $\E$, specifying objects by
\[
\ob(\E_F) \coloneqq \{X\in \ob(\E)\mid \text{ the morphism $\xi_X$ factors through $F\rightarrowtail \Xi$}\}.
\]
In this note,
% we write $\iota_F \colon F \rightarrowtail\Xi$ for the embedding morphism (for a fixed subobject $F$ of $\Xi$). F
for each object $X\in \ob(\E_F)$, we write $\xi_X^F\colon X \to F$ for the unique lift of $\xi_X$ along $\iota_F$
\[
\begin{tikzcd}
& F\ar[d, rightarrowtail, "\iota_F"]\\
X\ar[r,"\xi_X"']\ar[ru, "\xi_X^F"]&\Xi.
\end{tikzcd}
\]
% Let us summarize the definitions around the main theorem of \cite{hora2024internal} without any proofs.
\subsubsection{The order structure}
Although the definition of a local state classifier makes sense for any categories, it behaves better in a cartesian closed categories. First and foremost, it has a canonical semilattice structure as follows:
\begin{proposition}[{\cite[][Proposition 3.27.]{hora2024internal}}]\label{prop:SemilatticeStructure}
If a cartesian closed category (in particular, an elementary topos) $\E$ admits a local state classifier $\{\xi_X\colon X\to \Xi\}_{X\in \ob (\E)}$, there exists a unique internal $\land$-semilattice structure on $\Xi$ such that the diagram
\[
\begin{tikzcd}[column sep =5pt]
&X_1\times \dots \times X_n \ar[ld, "(\xi_{X_1}) \times \dots \times (\xi_{X_n})"']\ar[rd, "\xi_{(X_1 \times \dots \times X_n)}"]&\\
\Xi^n\ar[rr,"\land"']&&\Xi
\end{tikzcd}
\]
is commutative for any finite sequence of objects $X_1, \dots, X_n \in \ob(\E)$.
\end{proposition}
This internal semilattice structure induces a semilattice structure on each homset $\E(X,\Xi)$ for each object $X\in \ob(\E)$. Therefore, each homset $\E(X, \Xi)$ admits a natural partial order defined by $f\leq g \iff f\land g =f$.
A subobject $\iota_F \colon F \rightarrowtail \Xi$ is said to be an \demph{internal filter}, if each subset $\E(X,F) \rightarrowtail \E(X,\Xi)$ is a filter in the usual sense (i.e., upward closed and closed under finite meets $\top, \land$). (In \cite{hora2024internal}, the author adopts a diagrammatic definition of an internal filter so that it makes sense even for locally large categories.)
\subsubsection{The classification theorem}
The paper \cite{hora2024internal} proves that,
if the category $\E$ is an elementary topos
% with a local state classifier $\Xi$
and the subobject $F\rightarrowtail\Xi$ is
an internal filter,
% an \demph{internal filter} (with respect to the internal $\land$-semilattice structure of $\Xi$ (\Cref{prop:SemilatticeStructure})),
the resulting full subcategory $\E_F$ is also an elementary topos, and the embedding $\E_F \hookrightarrow \E$ is an inverse image functor of a hyperconnected geometric morphism $f_F\colon \E \to \E_F$.
The main theorem of \cite{hora2024internal} (\Cref{thm:OldMainTheorem}) states that
this construction $F \mapsto \E_F$ provides a bijective correspondence between the internal filters of $\Xi$ and the hyperconnected quotients of $\E$.
% \Cref{thm:OldMainTheorem} states that,
% if the category $\E$ is an elementary topos with a local state classifier $\Xi$, the above construction $F \mapsto \E_F$ provides a bijective correspondence between the internal filters of the internal $\land$-semilattice $\Xi$ and the hyperconnected quotients of $\E$. Notice that the embedding $\E_F \hookrightarrow \E$ serves as the inverse image functor of the corresponding hyperconnected geometric morphism $f_F\colon \E \to \E_F$.
% The following theorem is the main theorem of \cite{hora2024internal}.
\begin{theorem}[{\cite[][Theorem 4.1]{hora2024internal}\footnote{In \cite{hora2024internal}, there is another correspondant, internal semilattice homomorphisms $\Xi \to \Omega$.}}]\label{thm:OldMainTheorem}
If an elementary topos $\E$ has a local state classifier $\Xi$,
% then $\Xi$ has an internal semilattice structure,
% and
there exists a bijective correspondence between the following data:
\begin{itemize}
\item Hyperconnected quotients of the topos $\E$.
% \item Internal semilattice homomorphisms $\Xi \to \Omega$.
\item Internal filters of the local state classifier $\Xi$.
\end{itemize}
\end{theorem}
% \begin{remark}[External description of internal filter]
% \end{remark}
% \begin{remark}[Description of the corresponding comonad and its counit map]\label{rmk:NotationOdXiF}
The paper \cite{hora2024internal} also provides the description of the corresponding lex comonad $\G \coloneqq f^{*}f_* \colon \E \to \E$ with its counit $\epsilon \colon \G \to \id_{\E}$
\[
\begin{tikzcd}
{\;}\ar[rr,phantom, ""'{name=F}]& \F \ar[rd,"f^*"]&{\;} \\
\E \ar[ru,"f_*"]\ar[rr, "\G", ""'{name=U}]\ar[rr, bend right =50, "\id_\E"', ""{name=W}]& & \E,
\ar[to=U, from=F, phantom, "\rotatebox{90}{$\coloneqq$}"]
\ar[to=W, from=U, Rightarrow, "\epsilon"]
\end{tikzcd}
\]
which states that the following diagram is a pullback square
\begin{equation}\label{eq:PullbackDescriptionOfTheCounitAndComonad}
\begin{tikzcd}
\G X\ar[r, "\xi^F_{\G X}"]\ar[d, "\epsilon_X", tail]\ar[rd, phantom, "\lrcorner", very near start]& F\ar[d,tail, "\iota_F"]\\
X\ar[r , "\xi_X"']& \Xi
\end{tikzcd}
\end{equation}
for every $X\in \ob(\E)$.
% \end{remark}
\section{The statement of the main theorem}
In order to motivate the following sections, let us state the main theorem first.
\begin{theorem}\label{thm:MainTheorem}
Let $\E$ be an elementary topos with a local state classifier $\Xi$, and $F \rightarrowtail \Xi$ be an internal filter.
% For a hyperconnected geometric morphism $f\colon \E \to \F$ corresponding to an internal filter $F\rightarrowtail \Xi$,
Then,
the family of morphisms
$\{\xi_{Z}^F \colon Z \to F\}_{Z\in \ob(\E_F)}$ is a local state classifier of the induced hyperconnected quotient topos $\E_{\F}$.
\end{theorem}
% There are implicit non-triviality here.
Notice that the above theorem implicitly states that the filter $F$ belongs to the
% induced hyperconnected quotient
full subcategory
$\E_F$.
This \dq{self-referential} phenomenon, $F \in \ob(\E_F)$, is not trivial. In fact, without the assumption that $F$ is a filter, there are a lot of counter-examples.
% exists a subobject $F \rightarrowtail \Xi$ such that $F\notin \ob(\E_{\F})$.
\begin{example}[The topos of graphs: {[Not being a loop] is a loop.} (1/2)] \label{exmp:ToposOfGraphsOne}
Let us consider the topos of directed graphs $\E \coloneqq \PSh(\rightrightarrows)$. As explained in \cite[][Toy Example 5.3.]{hora2024internal}, its local state classifier $\Xi$ looks like
\[
\Xi = \left (
\begin{tikzcd}[scale=3]
\bullet\ar[loop left,"\text{[Being a loop]}"]\ar[loop right,"\text{[Not being a loop]}"]
\end{tikzcd}
\right ).
\]
For a directed graph $X = (s,t\colon E \rightrightarrows V)$ in $\E$, the graph morphism $\xi_X$ sends every vertex to the unique vertex of $\Xi$, and sends each morphism $e\in E$ to either [Being a loop] or [Not being a loop] detecting whether the edge $e$ is a loop or not.
Let us consider a subgraph
\[
F = \left (
\begin{tikzcd}[scale=3]
\bullet\ar[loop right,"\text{[Not being a loop]}"]
\end{tikzcd}
\right ),
\]
which is not an internal filter. Then the induced full subcategory $\E_F$ consists of graphs whose edges are not loops (i.e., $s(e) \neq t(e)$ for any $e\in E$). Obviously, $F$ itself does not belongs to the subcategory, since the edge [Not being a loop] is a loop! Thus we obtain an example of the situation $F\notin \ob(\E_F)$.
\end{example}
% and is the main topic of the next section.
% % non-triv
% In some situations, this theorem helps one to describe a local state classifier of a non-presheaf topos.
% \memo{Can I cite kit?}
% \memo{Can I write Myhill-Nerode Theorem?}
% The main content of the next section, the normalization operator, is a kind of measurement
% This will be proven in \Cref{cor:FilterLivesInHQuotient} in a little bit more general form.
The main concept in the next section, \demph{the normalization operator,} precisely describes such a \dq{self-referential aspect} of the local state classifier (see also \Cref{exmp:ToposOfDirectedGraphTwo}). By using this and the order structure of $\Xi$, \Cref{cor:FilterLivesInHQuotient} shows that for an upward closed $F$, the condition $F \in \ob(\E_F)$ holds.
\section{Normalization operator in a category with a local state classifier}
The aim of this section is to define and study what we call the normalization operator of a category.
\begin{definition}[Normalization operator]\label{def:NormalizationOperator}
For a category $\E$ that admits a local state classifier $\Xi$, \demph{the normalization operator}
\[\xi_{\Xi}\colon \Xi \to \Xi\]
is the component of the colimit cocone $\{\xi_X \colon X \to\Xi\}_{X\in \ob(\E)}$ for the object $\Xi$.
% and write it as $\Nor_{\E} \coloneqq \xi_{\Xi}$.
\end{definition}
This terminology is inspired by the case of group action topos (see \cite[][Example 3.10]{hora2024internal} for details).
In the topos of right $G$-actions $\PSh(G)$ for a group $G$, the local state classifier $\Xi$ is the set of subgroups equipped with the right conjugate actions.
\[
H\cdot g \coloneqq g^{-1}Hg \text{ in }\Xi
\]
Each component of the colimit cocone $\{\xi_X \colon X \to\Xi\}_{X\in \ob(\E)}$
sends an element $x\in X$ of a $G$-set $X$ to its stabilizer subgroup.
\[
\xi_X(x) = \{g\in G\mid x\cdot g = x\}
\]
Therefore, the normalization operator $\xi_{\Xi} \colon \Xi \to \Xi$ sends a subgroup $H\in \Xi$ to its normalizer group $\Nor_{G}(H) \in \Xi$
\[
\xi_{\Xi}\colon H \mapsto \{g\in G \mid g^{-1}Hg= H\} = \Nor_G (H).
\]
\begin{example}[The topos of graphs: {[Not being a loop] is a loop.} (2/2)]\label{exmp:ToposOfDirectedGraphTwo}
The normalization operator $\xi_\Xi \colon \Xi \to \Xi$ in the topos of directed graphs $\E = \PSh(\rightrightarrows)$ sends both of two loops [Being a loop] and [Not being a loop] in $\Xi$
\[
\Xi = \left (
\begin{tikzcd}[scale=3]
\bullet\ar[loop left,"\text{[Being a loop]}"]\ar[loop right,"\text{[Not being a loop]}"]
\end{tikzcd}
\right )
\]
to the edge [Being a loop].
In particular, we have $\xi_{\Xi}(\text{[Not being a loop]}) = \text{[Being a loop]}$, which captures the self-referential statement \dq{[Not being a loop] is a loop.}
\end{example}
% \begin{example}[Monoid actions and Word actions]
% \end{example}
% \begin{example}[Localic topos]
% \end{example}
At first glance, the normalization operator has nothing to do with the order structure ($=$ the semilattice structure) of $\Xi$.
% is NOT a semilattice homomorphism on $\Xi$.
For example, it does not preserve even the order structure: In the topos $\PSh(S_3)$ of the symmetric group $S_3$-actions, the subgroup $H \coloneqq \langle(1,2)\rangle$ is larger than $\{e\} \subset G$, but $\Nor_{S_3}(H)= H \subsetneq S_3 =\Nor_{S_3}(\{e\})$.
% \begin{remark}
% the normalization morphism is NOT a semilattice homomorphism on $\Xi$. It does not preserve even the order structure. For example, in the topos $\PSh(S_3)$ of the symmetric group $S_3$-actions, the subgroup $H \coloneqq \langle(1,2)\rangle$ is larger than $\{e\} \subset G$, but $\Nor_{S_3}(H)= H \subsetneq S_3 =\Nor_{S_3}(\{e\})$.
% \end{remark}
However, there is an obvious inclusion relation
\[H \subset \Nor_G(H)\] for the normalizer of a subgroup $H \subset G$, which can be generalized as follows:
% The next proposition is a generalization of the inclusion relation
\begin{proposition}[Normalization lemma]
\label{prop:NormalizationLemma}
In a cartesian closed category $\E$ with a local state classifier $\Xi$, the morphism $\xi_{\Xi}\colon \Xi\to \Xi$ is equal to or larger than $\id_{\Xi}$
% \[
% \id_{\Xi} \leq \xi_{\Xi}
% \]
\[
\begin{tikzcd}[column sep=50pt]
\Xi\ar[r, bend left, ""'{name=A}, "\id_\Xi"]\ar[r, bend right, "\xi_\Xi"', ""{name=B}] \ar[from=A, to=B, phantom, "\rotatebox{90}{$\geq$}"] &\Xi
\end{tikzcd}
\]
with respect to the $\land$-semilattice structure on $\E(\Xi, \Xi)$.
\end{proposition}
\begin{proof}
To prove $\id_{\Xi}\leq \xi_{\Xi}$, we need to prove that the composite of
\[
\begin{tikzcd}[column sep = 50pt]
\Xi\ar[r,"{\langle\id_{\Xi}, \xi_{\Xi}\rangle}"]&
\Xi\times \Xi\ar[r,"\land"]&\Xi.
\end{tikzcd}
\]
is the identity.
Since $\Xi$ is a colimit, it suffices to prove the following commutativity for each object $X\in \ob(\E)$.
\[
\begin{tikzcd}[column sep = 50pt]
X\ar[d,"\xi_X"']\ar[rr,bend left, "\xi_X"]&&\Xi\ar[d,equal]\\
\Xi\ar[r,"{\langle\id_{\Xi}, \xi_{\Xi}\rangle}"]&
\Xi\times \Xi\ar[r,"\land"]&\Xi
\end{tikzcd}
\]
By the definition of $\land$ operation and the fact that ${\langle\id_X, \xi_X\rangle}$ is a (split) monomorphism, we have the next commutative diagram.
\[
\begin{tikzcd}[column sep = 50pt]
X\ar[d,"\xi_X"']\ar[rr,bend left, "\xi_X"]\ar[r, "{\langle\id_X, \xi_X\rangle}", tail]&X\times \Xi\ar[d,"{\xi_X \times \xi_{\Xi}}"]\ar[r,"\xi_{X\times \Xi}"]&\Xi\ar[d,equal]\\
\Xi\ar[r,"{\langle\id_{\Xi}, \xi_{\Xi}\rangle}"]&
\Xi\times \Xi\ar[r,"\land"]&\Xi
\end{tikzcd}
\]
This completes the proof.
\end{proof}
\begin{corollary}
\label{cor:FilterLivesInHQuotient}
For any cartesian closed category $\E$ with a local state classifier $\Xi$, and any internal filter (or more generally, any upward closed subobject) $F\rightarrowtail \Xi$, we have
\[
F \in \ob(\E_F),
\]
i.e.,
$F$ belongs to the induced full subcategory $\E_F \hookrightarrow \E$.
% is an object of the corresponding hyperconnected quotient $\E \twoheadrightarrow \E_F$.
\end{corollary}
\begin{proof}
% Let $\iota_{F} \colon F \rightarrowtail\Xi$ denote the inclusion map.
Due to the equivalence (\ref{eq:FullSubCondition}), it suffices to prove that $\xi_F \colon F \to \Xi$ lifts along $\iota_{F}\colon F \rightarrowtail \Xi$.
\[
F\in \ob(\E_F)
\iff
\begin{tikzcd}
& F\ar[d, rightarrowtail, "\iota_{F}"]\\
F\ar[r,"\xi_F"']\ar[ru, dashed, "\exists"]&\Xi
\end{tikzcd}
\]
Since $\iota_{F}$ trivially lifts along itself and the internal filter $F$ is upward closed, it is enough to prove the inequality $\iota_{F} \leq \xi_F$. This follows from the following diagram and the inequality of \Cref{prop:NormalizationLemma}.
% $\xi_F$ also lifts along $\iota_{F}$.
% The inequality $\id_\Xi \leq \xi_{\Xi}$ (\Cref{prop:NormalizationLemma}) implies $\iota_{F} \leq \xi_F$ due to the following diagram.
\[
% \begin{tikzcd}[column sep=50pt]
% F\ar[r, bend left, ""'{name=A}, "\iota_{F}"]\ar[r, bend right, "\xi_F"', ""{name=B}] \ar[from=A, to=B, phantom, "\rotatebox{90}{$\geq$}"] &\Xi
% \end{tikzcd}
% =
\begin{tikzcd}[column sep=50pt]
F \ar[r,"\iota_{F}", rightarrowtail]\ar[rr, bend right=50, "\xi_F"',""{name=C}]&\Xi\ar["\rotatebox{90}{$=$}", to={C}, phantom]\ar[r, bend left, ""'{name=A}, "\id_\Xi"]\ar[r, bend right, "\xi_\Xi"', ""{name=B}] \ar[from=A, to=B, phantom, "\rotatebox{90}{$\geq$}"] &\Xi
\end{tikzcd}
\]
\end{proof}
\section{Local state classifier in a hyperconnected quotient}
The goal of this section is to prove \Cref{thm:MainTheorem}.
In this section, we fix the following data:
\begin{itemize}
\item $\E$ is an elementary topos with a local state classifier $\Xi$.
\item $F$ is an internal filter of $\Xi$.
\item $\E_F$ is the corresponding hyperconnected quoteint of $\E$.
\item $\G$ is the corresponding (lex idempotent) comonad on $\E$, with monic counit $\{\epsilon_X \colon \G X \rightarrowtail X\}_{X\in \ob(\E)}$
\end{itemize}
Due to \Cref{thm:OldMainTheorem} and \Cref{prop:ExistenceForGrothendieck}, this situation covers all hyperconnected geometric morphisms between Grothendieck topoi.
% Due to \Cref{cor:FilterLivesInHQuotient}, for any internal filter $F \rightarrowtail \Xi$, all morphisms $\{\xi_X^F\colon X \to F \}_{X\in \ob(\E_F)}$, which are morphisms in $\E$ a priori, belong to the full subcategory $\E_F$.
Due to \Cref{cor:FilterLivesInHQuotient}, we know that all components of the family $\{\xi_{Z}^F \colon Z \to F\}_{Z\in \ob(\E_F)}$ belong to the full subcategory $\E_F$. As next lemma shows, it is not hard to prove that it is a cocone. \memo{Warning: The constructions, like powerset construction, are done in the larger topos $\E$.}
\begin{lemma}[Being a cocone]\label{lem:BeingCocone}
The family $\{\xi_{Z}^F \colon Z \to F\}_{Z\in \ob(\E_F)}$ is a cocone under the functor ${(\E_F)}_{\mono} \to \E_F$.
\end{lemma}
\begin{proof}
Let $m\colon Z\rightarrowtail Z'$ be an arbitrary monomorphism in the category $\E_F$. Since the embedding $\E_F \hookrightarrow \E$ preserves finite limits, $m$ remains to be monic in the ambient topos $\E$. Therefore, we have the commutativity of the outer perimeter of the following diagram:
\[
\begin{tikzcd}
Z\ar[rr,"m", rightarrowtail]\ar[rd, "\xi^F_{Z}"']\ar[rdd, "\xi_Z"', bend right]&&Z'\ar[ld, "\xi^F_{Z'}"] \ar[ldd, "\xi_Z'", bend left]\\
&F\ar[d,rightarrowtail, "\iota_F"]&\\
&\Xi.&
\end{tikzcd}
\]
Since $\iota_F$ is monic, this implies the commutativity of the inner triangle $ \xi_{Z'}^F \circ m = \xi^F_{Z}$, which completes the proof.
\end{proof}
In the rest of this section, we will prove the universality of the family $\{\xi_{Z}^F \colon Z \to F\}_{Z\in \ob(\E_F)}$ as a colimit of $(\E_F)_{\mono} \to \E_F$. What we can use is the fact that the cocone $\{\xi_X \colon X \to \Xi\}_{X\in \ob(\E)}$ is a (large) colimit cocone $\E_{\mono}\to \E$. So we will convert the situations in $\E_F$ to the larger category $\E$ and reduce the required universality of $F \in \ob(\E_F)$ to that of $\Xi \in \ob(\E)$.
First, we will prove the uniqueness part of the universality of $F$. Recall that a (possibly large) family of morphisms $\{f_\lambda \colon X_\lambda \to Y\}_{\lambda \in \Lambda}$ is said to be \demph{jointly epimorphic} if, for any parallel morphisms $g,h\colon Y \rightrightarrows Z$, the implication
$
(\forall \lambda \in \Lambda\; g\circ f_\lambda = h\circ f_\lambda) \implies (g=h)
$ holds.
% holds.
% \[
% (\forall \lambda \in \Lambda\; g\circ f_\lambda = h\circ f_\lambda) \iff (g=h)
% \]
% holds.
% implies $g=h$.
In the following proof, we will not assume that the topos $\E$ is a Grothendieck topos. So we cannot use the complete lattice structure of the subobject lattice of $\Xi$. Instead of it, we use the Heyting algebra structure of it, which makes sense in an arbitrary elementary topos.
\begin{lemma}[Universality (1/2): Uniqueness]
\label{lem:JointlyEpimorphic}
% For a hyperconnected geometric morphism $f\colon \E \to \F$ corresponding to an internal filter $F\rightarrowtail \Xi$,
% % Let $f\colon \E \to \F$ be a hyperconnected geometric morphism, $\G\coloneqq f^{\ast}f_{\ast}\colon \E \to \E$ be the corresponding lex comonad, and $\epsilon\colon \G \to \id_{\E}$ be its counit.
% the (possibly large) family of morphisms $\{\xi_{\G X}^F \colon \G X \to F\}_{X\in \ob(\E)}$ is jointly epimorphic, where $\G$ denotes the corresponding lex comonad.
The cocone $\{\xi_{Z}^F \colon Z \to F\}_{Z\in \ob(\E_F)}$ is jointly epimorphic (in $\E$, and hence in $\E_F$).
\end{lemma}
\begin{proof}
% Let $g, h \colon F \rightrightarrows Z$ be two morphisms such that $g \circ \xi^F_Z = h\circ \xi^{F}_{Z}$ holds for any $Z\in \ob(\E_F)$. We will prove $g=h$ by showing that their equalizer $S \rightarrowtail F \rightrightarrows Z$ coincides with $F$.
% % By the construction of $S$,
% %
Take an arbitrary subobject $S\rightarrowtail F$ such that every arrow in $\{\xi^F_{Z} \colon Z \to F\}_{Z\in \ob(\E_F)}$ lifts along $S\rightarrowtail F$. It suffices to prove $S=F$ (due to \Cref{lem:JointlyEpimorphicFamilyAndSubobject}).
% since for any two morphisms $g, h \colon F \to Z$ that are not distinguished by any morphisms in the family, every morphism $\xi^F_Z$ factors through their equalizer $S \rightarrowtail F \rightrightarrows Z$.
% % which implies $g=h$.
% Notice that each morphism $\xi^F_Z \colon Z \to F$ factors through $S$, i.e.,
By the lifting assumption on $S$,
the inequality
\[
\Image(\xi^F_Z) \leq S \text{ in } \Sub_{\E}(\Xi)
\]
holds for every $Z\in \ob(\E_F)$.
We also have the equality
\[
\Image(\xi_X)\land F = \Image(\xi^F_{\G X}) \text{ in } \Sub_{\E}(\Xi)
\]
for every object $X \in \ob(\E)$, since the epi-mono factorization of $\E$, which is pullback stable, decomposes the pullback square (\ref{eq:PullbackDescriptionOfTheCounitAndComonad})
\[
\begin{tikzcd}
\G X\ar[r, "\xi_{\G X}^F"]\ar[d, "\epsilon_X", tail] \ar[rd, phantom, "\lrcorner", very near start]& F\ar[d,tail, "\iota_F"]\\
X\ar[r , "\xi_X"']& \Xi
\end{tikzcd}
\]
into the following pullback diagram
\[
\begin{tikzcd}
\G X\ar[r, two heads]\ar[rr, bend left, "\xi_{\G X}^F"]\ar[d, "\epsilon_X", tail]\ar[rd, phantom, "\lrcorner", very near start]&
% \Image(\xi_X)\land F
\Image(\xi^F_{\G X})
\ar[r, tail]\ar[d, tail]\ar[rd, phantom, "\lrcorner", very near start]& F\ar[d,tail, "\iota_F"]\\
X\ar[rr, bend right , "\xi_X"']\ar[r, two heads]&\Image(\xi_X)\ar[r, tail]& \Xi.
\end{tikzcd}
\]
Combining the above two (in)equalities in $\Sub_{\E}(\Xi)$,
we obtain an inequality
\[
\Image(\xi_X)\land F \leq S \text{ in } \Sub_{\E}(\Xi)
\]
for each object $X\in \ob(\E)$.
Since the poset $\Sub_{\E}(\Xi)$ is a Heyting algebra,
this is equivalent to the inequality
\[
\Image(\xi_X) \leq (F \mathbin{\rightarrow} S) \text{ in } \Sub_{\E}(\Xi).
\]
This means that the colimit cocone $\{\xi_X\colon X \to \Xi\}_{X\in \ob(\E)}$ factors throgh the subobject $(F\to S) \in \Sub_{\E}(\Xi)$.
Since the colimit cocone $\{\xi_X \colon X \to \Xi\}_{X \in \ob(\E)}$ is jointly epimorphic, we have
\[
\Xi = \top= (F \mathbin{\rightarrow} S) \text{ in } \Sub_{\E}(\Xi).
\] (due to \Cref{lem:JointlyEpimorphicFamilyAndSubobject}), i.e., $F\leq S$. Since $S\leq F$ holds by definition, this completes the proof.
\end{proof}
Lastly, we need to prove the existence part of the universality of $F$, using the universality of $\Xi$. This is the tricky part, since in order to use the universality of $\Xi$, we need to construct a cocone under $\E_{\mono} \to \E$ from a given cocone $\{\phi_Z\colon Z\to L\}_{Z \in \ob(\F)}$ under $(\E_F)_{\mono} \to \E_F$.
The first idea to do it is to use the counit $\epsilon_X \colon \G X \rightarrowtail X$. Since $\G X$ is an object of $\E_F$, we can canonically associate an object $\G X$ of $\E_F$ with each object $X$ of $\E$. But here is another problem. Although we want to construct a family of morphisms \textbf{from} all objects $X$ in $\E$, what the counit provides is morphisms \textbf{to} objects of $\E$. To inverse the direction of the arrow, we need the next idea, to use the powerset object.
Recall that any morphism $f\colon X \to Y$ in a topos induces three morphisms between the powerset objects:
\[
\begin{tikzcd}[column sep = 70pt]
PX \ar[r,"\exists_f ", bend left] \ar[r, "\forall_f"', bend right ] & PY. \ar[l, "f^{-1}"']
\end{tikzcd}
\]
Combining these ideas, we obtain a cocone under $\E_{\mono} \to \E$ as follows:
\begin{lemma}
\label{lem:ExtensionLemma}
% Let $f\colon \E \to \F$ be a hyperconnected geometric morphism, $\G\coloneqq f^{\ast}f_{\ast}\colon \E \to \E$ be the corresponding lex comonad, and $\epsilon\colon \G \to \id_{\E}$ be its counit.
% For any locally determined cocone
Let
$\{\phi_Z\colon Z\to L\}_{Z \in \ob(\F)}$ be a cocone under the diagram $(\E_F)_{\mono}\to \E_F$. Then the family of morphisms
\[
\begin{tikzcd}
\{\psi_X\colon X\ar[r,"\sgt_X"] &PX \ar[r,"{\epsilon_X}^{-1}"]&P\G X\ar[r,"\exists_{\phi_{\G X}}"] & PL\}_{X\in \ob(\E)}
\end{tikzcd}
\]
defines a cocone under the diagram $\E_{\mono} \to \E$.
% a locally determined cocone on $\E$.
Furthermore, $\psi$ is an extension of $\phi$ in the sense of
\[
\begin{tikzcd}
\G X \ar[r, "\phi_{\G X}"]\ar[d, tail, "\epsilon_X"]& L\ar[d, "\sgt_L", tail]\\
X\ar[r, "\psi_X"]& PL
\end{tikzcd}
\]
\end{lemma}
\begin{proof}
For any monomorphism $m\colon X\rightarrowtail Y$ in $\E$, we have a commutative diagram
\[
\begin{tikzcd}[row sep = 10pt]
X\ar[r,"\sgt_X"] \ar[dd, "m", tail]&PX \ar[r,"{\epsilon_X}^{-1}"]\ar[dd, "\exists_m"]&P\G X\ar[rd,"\exists_{\phi_{\G X}}"]\ar[dd,"\exists_{\G m}"]&\\ &&&PL\\
Y\ar[r,"\sgt_X"] &PY \ar[r,"{\epsilon_Y}^{-1}"]&P\G Y\ar[ru,"\exists_{\phi_{\G Y}}"'] &
\end{tikzcd}
\]
since the left square commutes by \Cref{lem:sgtNaturality}, the right triangle commutes by the assumption of $\phi$ being locally determined, and the middle square commutes by the Beck-Chevalley condition for the pullback square
\[
\begin{tikzcd}
\G X \ar[r, "\G m", tail]\ar[d,"\epsilon_X", tail]&\G Y\ar[d,"\epsilon_Y", tail]\\
X\ar[r,"m", tail] & Y.
\end{tikzcd}
\]
This proves that $\psi$ is locally determined.
To prove
\[
\begin{tikzcd}
\G X \ar[rrr, "\phi_{\G X}"]\ar[d, tail, "\epsilon_X"]&&& L\ar[d, "\sgt_L", tail]\\
X\ar[r,"\sgt_X"'] &PX \ar[r,"{\epsilon_X}^{-1}"']&P\G X\ar[r,"\exists_{\phi_{\G X}}"'] & PL
\end{tikzcd}
\]
is commutative, we have
\[
\begin{tikzcd}
\G X \ar[rrr, "\phi_{\G X}"]\ar[rrd, "\sgt_{\G X}", tail]\ar[d, tail, "\epsilon_X"]&&& L\ar[d, "\sgt_L", tail]\\
X\ar[r,"\sgt_X"'] &PX \ar[r,"{\epsilon_X}^{-1}"']&P\G X\ar[r,"\exists_{\phi_{\G X}}"'] & PL.
\end{tikzcd}
\]
\Cref{lem:sgtExtNaturality} and \Cref{lem:sgtNaturality} complete the proof.
\end{proof}
\begin{proof}[Proof of \Cref{thm:MainTheorem}]
By \Cref{cor:FilterLivesInHQuotient}, this family of morphisms is in the category $\F$. Since the embedding $f^{\ast}\colon \F \to \E$ is fully faithful and lex, the family of morphisms is locally determined. So, we need to prove that this family has the universality as a colimit of all monomorphisms in $\F$. Since \Cref{lem:JointlyEpimorphic} ensure the uniqueness part of the desired universality, we will prove the existence part.
Take an arbitrary cocone $\{\phi_Z \colon Z\to L\}_{Z\in \ob(\F)}$ under all monomorphisms in $\F$. Let $\{\psi_X\colon X \to PL\}_{X\in \ob(\E)}$ be the locally determined cocone given in \Cref{lem:ExtensionLemma}. By the universality of the local state classifier $\Xi$, we have a unique morphism $\gamma \colon \Xi \to PL$ such that
\[
\begin{tikzcd}
% [column sep = 10pt]
[row sep = 50pt]
&X\ar[ld,"\xi_X"']\ar[rd,"\psi_X"]&\\
\Xi\ar[rr,"\gamma"]&&PL
\end{tikzcd}
\]
commutes for every $X\in \ob(\E)$. Due to the diagram (\ref{eq:PullbackDescriptionOfTheCounitAndComonad}) and the latter part of \Cref{lem:ExtensionLemma}, the following diagram is also commutative.
\begin{equation}\label{eq:block}
\begin{tikzcd}
% [column sep = 10pt]
[row sep = 50pt]
&\G X\ar[ld, "\xi_{\G X}^F"']\ar[d,"\epsilon_X", tail]\ar[rd, "\phi_{\G X}"]&\\
F\ar[d,tail, "\iota_F"'] &X\ar[ld,"\xi_X"']\ar[rd,"\psi_X"]&L\ar[d,"\sgt_L", tail]\\
\Xi\ar[rr,"\gamma"]&&PL
\end{tikzcd}
\end{equation}
Now that, it remains to prove that $\gamma \circ \iota_F\colon F\rightarrowtail \Xi \to PL$ lifts along $\sgt_L$:
\[
\begin{tikzcd}
% [column sep = 10pt]
[row sep = 50pt]
&\G X\ar[ld, "\xi_{\G X}^F"']\ar[rd, "\phi_{\G X}"]&\\
F\ar[d,tail, "\iota_F"'] \ar[rr, dashed, "?"]&&L\ar[d,"\sgt_L", tail]\\
\Xi\ar[rr,"\gamma"]&&PL.
\end{tikzcd}
\]
Take the characteristic morphism of $\sgt_{L}\colon L \rightarrowtail PL$ as
\[
\begin{tikzcd}
% [column sep = 10pt]
[row sep = 50pt]
&\G X\ar[ld, "\xi_{\G X}^F"']\ar[rd, "\phi_{\G X}"]&&\\
F\ar[d,tail, "\iota_F"'] \ar[rr, dashed, "?"]&&L\ar[d,"\sgt_L", tail]\ar[rr, "!"]\ar[rrd, phantom, "\lrcorner", very near start]&&1\ar[d,"\true", tail]\\
\Xi\ar[rr,"\gamma"]&&PL\ar[rr,"\chi_L"]&&\Omega.
\end{tikzcd}
\]
By the universality of the pullback, it suffices to
% We
prove that the composite $F\rightarrowtail \Xi \to PL \to \Omega$ coincides with the true morphism $\true_{F}\colon F \to \Omega$. \Cref{lem:JointlyEpimorphic} reduces it to proving that the composition $\G X \to F \to \Xi \to PL \to \Omega$ coincides with $\true_{\G X}$ for every $X \in \ob(\E)$. This follows from the commutativity of the perimeter of
\[
% \begin{tikzcd}
% % [column sep = 10pt]
% [row sep = 50pt]
% &\G X\ar[ld, "\xi_{\G X}^F"']\ar[rd, "\phi_{\G X}"]\ar[rrrd, bend left, "!"]\ar[d,"\epsilon_X"]&&\\
% F\ar[d,tail, "\iota_F"'] &X\ar[ld, "\xi_X"']\ar[rd,"\psi_X"]&L\ar[d,"\sgt_L", tail]\ar[rr, "!"]\ar[rrd, phantom, "\lrcorner", very near start]&&1\ar[d,"\true", tail]\\
% \Xi\ar[rr,"\gamma"]&&PL\ar[rr,"\chi_L"]&&\Omega.
% \end{tikzcd}
\begin{tikzcd}
% [column sep = 10pt]
[row sep = 50pt]
&\G X\ar[ld, "\xi_{\G X}^F"']\ar[rd, "\phi_{\G X}"]\ar[rrrd, bend left, "!"]&&\\
F\ar[d,tail, "\iota_F"']
% \ar[rrd, phantom, "(\ref{eq:block})"]
&(\ref{eq:block})&L\ar[d,"\sgt_L", tail]\ar[rr, "!"]\ar[rrd, phantom, "\lrcorner", very near start]&&1\ar[d,"\true", tail]\\
\Xi\ar[rr,"\gamma"]&&PL\ar[rr,"\chi_L"]&&\Omega.
\end{tikzcd}
\]
This completes the proof.
\end{proof}
% \section{A motivating example}
\appendix
\section{Properties of elementary topoi}
This appendix summarizes the properties of elementary topoi that are used in the main part.
\begin{lemma}[Jointly epimorphic families in an elementary topos]\label{lem:JointlyEpimorphicFamilyAndSubobject}
For a (possibly large) family of morphisms $\{f_\lambda \colon X_\lambda \to Y\}_{\lambda \in \Lambda}$ in a category $\E$, we consider the following two conditions:
\begin{enumerate}
\item $\{f_\lambda \colon X_\lambda \to Y\}_{\lambda \in \Lambda}$ is jointly epimorphic.
\item If all morphisms in the family factor through a monomorphism $m\colon S\rightarrowtail Y$, then $m$ is an isomorphism.
\end{enumerate}
If $\E$ is balanced, i.e. every monic and epic morphism is an isomorphism, then $(1)$ implies $(2)$. If $\E$ has equalizers, then $(2)$ implies $(1)$. In particular, if $\E$ is an elementary topos, the two conditions $(1),(2)$ are equivalent.
\end{lemma}
\begin{proof}
First, assuming that the family is jointly epimorphic and $\E$ is balanced, we prove $(2)$. Take an arbitrary monomorphism $m\colon S\rightarrowtail Y$ such that every morphism $f_\lambda$ in the family factors through $m$ as $f_{\lambda} = m\circ f^S_{\lambda}$. For any morphisms $g,h \colon Y \rightrightarrows Z$ such that $g\circ m = h\circ m$, we have $g\circ f_{\lambda} = g\circ m \circ f_{\lambda}^{S} = h\circ m \circ f_{\lambda}^{S} = h\circ f_{\lambda}$, and the $g=h$. This proves that $m$ is also epic, and hence the balancedness assumption implies that $m$ is an isomorphism.
Next, assuming $(2)$ and that $\E$ has equalizers, we prove $(1)$. Take an arbitrary morphisms $g,h \colon Y \rightrightarrows Z$ such that $g\circ f_{\lambda} =h\circ f_{\lambda}$ for any $\lambda$. We prove $g=h$. Let $m\colon S\rightarrowtail Y$ be the equalizet of the two morphisms $g,h$. Then every morphism in the family factors through $m$, and the assumption $(2)$ implies that $m$ is an isomorphism. This proves that $g=h$.
\end{proof}
\begin{lemma}
\label{lem:sgtNaturality}
For any morphism $f\colon X\to Y$ in a topos, the diagram
\[
\begin{tikzcd}
X\ar[r,"\sgt_{X}", tail]\ar[d, "f"]&PY\ar[d,"\exists_f"]\\
Y\ar[r,"\sgt_Y", tail]&PY
\end{tikzcd}
\]
commutes.
\end{lemma}
\begin{proof}
Via the bojection $\E(X, PY) \cong \Sub(X\times Y)$,
both of two maps corresponds to the subobject
\[
\langle\id_X, f \rangle \colon X \rightarrowtail X\times Y.
\]
In fact, the right above part corresponds to the image of the composite
\[
\begin{tikzcd}
X \ar[r,rightarrowtail, "\Delta_X"] &X\times X \ar[r,"\id_X \times f"]& X\times Y,
\end{tikzcd}
\]
and the left below part corresponds to the pullback
\[
\begin{tikzcd}
X\ar[r, "f"] \ar[d, rightarrowtail, "{\langle \id_X, f\rangle }"'
] \ar[rd, phantom, "\lrcorner", very near start]
& Y\ar[d, "\Delta_Y", rightarrowtail]\\
X\times Y \ar[r,"f\times \id_Y"] & Y\times Y.
\end{tikzcd}
\]
\end{proof}
\begin{lemma}
\label{lem:sgtExtNaturality}
For any monomorphism $m \colon X\rightarrowtail Y$ in a topos,
\[
\begin{tikzcd}
X\ar[r,"\sgt_{X}", tail]\ar[d,tail, "m"]&PX\\
Y\ar[r,"\sgt_{Y}", tail]&PY\ar[u,"m^{-1}"']
\end{tikzcd}
\]
commutes.
\end{lemma}
\begin{proof}
Consider the following commutative diagram:
\[
\begin{tikzcd}[row sep = 10 pt]
X\times X\ar[rd,"\delta_X"]\ar[dd,"m\times m"', tail]&\\
& \Omega\\
Y \times Y.\ar[ru, "\delta_Y"']
\end{tikzcd}
\]
Taking the transposes of it with the naturality of the three-variable adjunction, we obtain the commutativity as stated.
\end{proof}
\printbibliography
\end{document}