\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}} \title{Normalization operator in a category and the local state classifier of a hyperconnected quotient} \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, and its use in analyzing hyperconnected geometric morphisms from a given topos. We first define a normalization operator 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_{\text{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}}] 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. This % 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.}] 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 \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, the "normalization operator", precisely describes the *self-referential aspect* of the local state classifier. By using this, Corollary 2.5 shows that for a filter $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}$ is the component of the colimit cocone $\{\xi_X \colon X \to\Xi\}_{X\in \ob(\E)}$ at 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}[Directed graphs] \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$. In fact, 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\})$. % \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} 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$. \begin{lemma} \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} \colon \G X \to F\}_{X\in \ob(\E)}$ is jointly epimorphic, where $\G$ denotes the corresponding lex comonad. \end{lemma} \begin{proof} Take an arbitrary subobject $S\rightarrowtail F$ such that every arrow in $\{\xi_{\G X} \colon\G X \to F\}_{X\in \ob(\E)}$ lifts along $S\rightarrowtail F$. It suffices to prove that $S=F$. (If there are two morphisms $f,g \colon F \to Z$ that are not distinguished by any morphisms in the family, then one can take their equalizer as $S$.) For every object $X \in \ob(\E)$, by the pullback square (\ref{eq:PullbackDescriptionOfTheCounitAndComonad}) \[ \begin{tikzcd} \G X\ar[r, "\xi_{\G X}"]\ar[d, "\epsilon_X", tail]& F\ar[d,tail]\\ X\ar[r , "\xi_X"']& \Xi \end{tikzcd} \] and its epi-mono factorization \[ \begin{tikzcd} \G X\ar[r, two heads]\ar[rr, bend left, "\xi_{\G X}"]\ar[d, "\epsilon_X", tail]&\Image(\xi_X)\land F\ar[r, tail]\ar[d, tail]& F\ar[d,tail]\\ X\ar[rr, bend right , "\xi_X"']\ar[r, two heads]&\Image(\xi_X)\ar[r, tail]& \Xi, \end{tikzcd} \] we have an inequality \[ \Image(\xi_X)\land F = \Image(\xi_{\G X}) \leq S \] in the Heyting algebra $\Sub(\Xi)$. This implies that $\Image(\xi_X) \leq (F \mathbin{\rightarrow} S)$. Since $\{\xi_X \colon X \to \Xi\}_{X \in \ob(\E)}$ is jointly epimorphic (because it is a colimit cocone), we have $\Xi = F \mathbin{\rightarrow} S$, i.e., $F\leq S$. This completes the proof. \end{proof} \begin{lemma} \label{lem:sgtExtNaturality} For a 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} \] and take the transposes of it. \end{proof} \begin{lemma} \label{lem:sgtNaturality} For a morphism $f\colon X\to Y$ in a topos, \[ \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} Both maps are corresponding to the subobject \[ \langle\id_X, f \rangle \colon X \rightarrowtail X\times Y \] as an element of $\E(X, PY) \cong \Sub(X\times Y)$. \end{proof} \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 a locally determined cocone $\{\phi_Z\colon Z\to L\}_{Z \in \ob(\F)}$, \[ \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 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_X}^{-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{tikzcd} % [column sep = 10pt] [row sep = 50pt] &\G X\ar[ld, "\xi_{\G X}"']\ar[d,"\epsilon_X", tail]\ar[rd, "\phi_{\G X}"]&\\ F\ar[d,tail] &X\ar[ld,"\xi_X"']\ar[rd,"\psi_X"]&L\ar[d,"\sgt_L", tail]\\ \Xi\ar[rr,"\gamma"]&&PL \end{tikzcd} \] Now that, it remains to prove that $F\rightarrowtail \Xi \to PL$ lifts along $\sgt_L$: \[ \begin{tikzcd} % [column sep = 10pt] [row sep = 50pt] &\G X\ar[ld, "\xi_{\G X}"']\ar[rd, "\phi_{\G X}"]&\\ F\ar[d,tail] \ar[rr, dashed, "?"]&&L\ar[d,"\sgt_L", tail]\\ \Xi\ar[rr,"\gamma"]&&PL. \end{tikzcd} \] Take the characteristic morphism of $L \rightarrowtail PL$ as \[ \begin{tikzcd} % [column sep = 10pt] [row sep = 50pt] &\G X\ar[ld, "\xi_{\G X}"']\ar[rd, "\phi_{\G X}"]&&\\ F\ar[d,tail] \ar[rr, dashed, "?"]&&L\ar[d,"\sgt_L", tail]\ar[rr, "!"]&&1\ar[d,"\true", tail]\\ \Xi\ar[rr,"\gamma"]&&PL\ar[rr,"\chi"]&&\Omega. \end{tikzcd} \] We prove that the composite $F\rightarrowtail \Xi \to PL \to \Omega$ is the true morphism $\true_{F}\colon F \to \Omega$. \Cref{lem:JointlyEpimorphic} reduces this problem to proving the composition $\G X \to F \to \Xi \to PL \to \Omega$ is $\true_{\G X}$ for every $X \in \G X$, and this follows from the commutativity of the perimeter of \[ \begin{tikzcd} % [column sep = 10pt] [row sep = 50pt] &\G X\ar[ld, "\xi_{\G X}"']\ar[rd, "\phi_{\G X}"]\ar[rrrd, bend left, "!"]&&\\ F\ar[d,tail] \ar[rr, dashed, "?"]&&L\ar[d,"\sgt_L", tail]\ar[rr, "!"]&&1\ar[d,"\true", tail]\\ \Xi\ar[rr,"\gamma"]&&PL\ar[rr,"\chi"]&&\Omega. \end{tikzcd} % \begin{tikzcd} % % [column sep = 10pt] % [row sep = 50pt] % &\G X\ar[ld, "\xi_{\G X}"']\ar[rrrd, bend left, "!"]&&\\ % F\ar[d,tail] &&&&1\ar[d,"\true", tail]\\ % \Xi\ar[rr,"\gamma"]&&PL\ar[rr,"\chi"]&&\Omega. % \end{tikzcd} \] \end{proof} % \section{A motivating example} \printbibliography \end{document}