← Topoi of automata II
Oldversions__20250310.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{array}
\usepackage{cleveref}
\usepackage[style=alphabetic,sorting=nyt]{biblatex}
\renewbibmacro{in:}{}
\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{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\LC}{\mathbb{L}}
\newcommand{\SQ}{\mathbb{S}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\ob}{\mathrm{ob}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\FinSet}{\mathbf{FinSet}}
\newcommand{\BoolAlg}{\mathbf{BoolAlg}}
\newcommand{\Cont}{\mathbf{Cont}}
\newcommand{\PSh}{\mathbf{PSh}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\DFA}{\mathrm{DFA}}
% \newcommand{\DFA}{\mathcal{DFA}\mathrm{}}
\newcommand{\Coalg}{\mathbf{Coalg}}
\newcommand{\G}{\mathbb{G}}
\newcommand{\true}{\mathrm{true}}
\newcommand{\Image}{\mathrm{Im}}
\newcommand{\Nor}{\mathrm{N}}
\newcommand{\Sub}{\mathrm{Sub}}
\newcommand{\sgt}{\{\cdot\}}
\newcommand{\je}{\mathbf{je}}
\newcommand{\Cl}{\mathrm{Clopen}}
\newcommand{\Gal}{\mathrm{Gal}}
\newcommand{\A}{\Sigma}
\newcommand{\MA}{{{\Sigma}^{\ast}}}
\newcommand{\proMA}{\widehat{\MA}}
\newcommand{\FA}{F_{\A}}
\newcommand{\pFA}{\hat{\FA}}
% \newcommand{\Aset}{\PSh (\MA)}
\newcommand{\Aset}{\A\text{-}\Set}
\newcommand{\T}{2x^{\A}}
% \newcommand{\Atmt}{\T\text{-}\mathbf{Coalg}}
\newcommand{\Atmt}{\mathbf{Atmt}}
% \newcommand{\Lan}{\mathcal{L}\mathrm{ng}}
% \newcommand{\Reg}{\mathcal{R}\mathrm{eg}}
\newcommand{\Lan}{\mathcal{L}}
\newcommand{\Reg}{\mathcal{R}}
\newcommand{\K}{\mathcal{K}}
\newcommand{\Func}[2]{[#1,#2]}
\newcommand{\Pow}{\mathcal{P}}
\newcommand{\HQ}{\mathrm{HQ}}
\newcommand{\pt}{\mathrm{pt}}
\newcommand{\f}{\mathrm{f.}}
\newcommand{\of}{\mathrm{o.f.}}
\newcommand{\pof}{{p_{\of}}}
\newcommand{\fAtmt}{\Atmt_{\f}}
\newcommand{\ofAtmt}{\Atmt_{\of}}
% \newcommand{\fAset}{{\Aset}_{\f}}
\newcommand{\fAset}{\A\text{-}\FinSet}
\newcommand{\ofAset}{{\Aset}_{\of}}
\newcommand{\AFinMon}{\A\text{-}\mathbf{FinMon}}
\newcommand{\empword}{\varepsilon}
\newcommand{\Lsq}{L_{\text{sq}}}
\newcommand{\Cong}{\mathrm{Cong}}
\newcommand{\colim}{\mathrm{colim}}
\newcommand{\Filt}{\mathrm{Filt}}
\newcommand{\bool}{\{\top, \bot\}}
\newcommand{\CoE}{{\int} \hspace{-2pt}}
\newcommand{\CoL}{{\CoE \Lan}}
\newcommand{\qslc}{\mathrm{LC}_{\text{q.s.}}}
\newcommand{\demph}[1]{\textit{\textbf{#1}}}
\newcommand{\Geom}{\mathbf{Geom}}
\newcommand{\SigmaInf}{\Sigma^{\leq \omega}}
\font\maljapanese=dmjhira at 2.5ex
\newcommand{\yo}{\textrm{\!\maljapanese\char"48}}
\newcommand{\abs}[1]{\left | #1 \right|}
\newcommand{\ADJ}[4]
{
\begin{tikzcd}[ampersand replacement = \&, column sep = small]
{#1}
\ar[rr, shift right=1.3ex, "{#2}"']
\&\perp\&
{#3}
\ar[ll, shift right=1.3ex,"{#4}"']
\end{tikzcd}
}
\newcommand{\Lv}{{Local variety}}
\newcommand{\lv}{{local variety}}
\newcommand{\Lvs}{{Local varieties}}
\newcommand{\lvs}{{local varieties}}
\title{Topoi of automata II: Hyperconnected geometric morphisms, syntactic monoids, and language classes}
\author{Ryuya Hora}
\thanks{Graduate School of Mathematical Sciences, University of Tokyo. \url{hora@ms.u-tokyo}}
% \date{\today}
\subjclass[2020]{18F10, 68Q70, 20M35, 18B20}
\keywords{Automaton, topos, regular language, hyperconnected geometric morphism, coalgebra, finite monoid, profinite word, Myhill-Nerode theorem}
\begin{document}
\begin{abstract}
\end{abstract}
\maketitle
\tableofcontents
\section{Introduction}
\memo{acknowledgement}
Compared to
\cite{gehrke2008duality, adamek2014generalized, ballester2015dual, uramoto2017semi}
As we have seen so far, the hyperconnected geometric morphism
\[
\begin{tikzcd}
\Aset \ar[r,"h"] & \ofAset
\end{tikzcd}
\]
plays a central role in our theory of regular languages. This section aims to observe that other hyperconnected geometric morphisms
\[
\begin{tikzcd}
&\E\\
\Aset \ar[r]\ar[ru]\ar[rd] & \F\\
& \mathcal{G}\\
\end{tikzcd}
\]
correspond to other classes of languages.
\section{Preliminaries: Hyperconnected quotient and local state classifier}
\subsection{Hyperconnected geometric morphism}
See \cite{johnstone2002sketchesv1, johnstone1981factorization} for the detailed definitions of hyperconnected geometric morphisms.
\begin{definition}[Hyperconnected geometric morphisms]
\label{def:hyperconnected}
A geometric morphism $f\colon \E \to \F$ is \demph{hyperconnected} if $f^{\ast}$ is fully faithful and $f$ satisfies the following equivalent conditions:
\begin{itemize}
\item The essential image of $f^{\ast}$ is closed under taking subquotients.
\item The essential image of $f^{\ast}$ is closed under taking subobjects.
\item The essential image of $f^{\ast}$ is closed under taking quotient objects.
\item The counit $\epsilon \colon f^{\ast}f_{\ast} \Rightarrow \id_{\E}$ is monic.
\end{itemize}
\end{definition}
Since $f^{\ast}$ for a hyperconnected geometric morphism $f\colon \E \to \F$ is fully faithful, the codomain topos $\F$ can be regarded as a full subcategory of the domain topos $\E$. If we regard it as a full subcategory, we call it a \demph{hyperconnected quotient}, according to the terminology in \cite[][section VII.]{lawvere2007axiomatic}.
\begin{proposition}
For a Grothendieck topos $\E$, the partially ordered class of (equivalence classes of ) hyperconnected quotients $\HQ(\E)$ is a small complete lattice.
\end{proposition}
\subsection{Local state classifier}
We will recall the description of $\HQ(\E)$ given in \cite{hora2024internal}.
\begin{definition}
We adopt the following definitions:
\begin{itemize}
\item \demph{A local state classifier} of a category $\C$ is the colimit of all monomorphisms
\[
\Xi \coloneqq \colim\left ( \C_{\text{mono}}\to \C \right),
\] where $\C_{mono}$ denotes the subcategory consisting of all objects and all monomorphisms of $\C$.
\item Its associated cocone is denoted by $\{\xi_X\colon X \to \Xi\}_{X\in \ob(\C)}$.
\end{itemize}
\end{definition}
\begin{fact}[\cite{hora2024internal}]
\label{fact:LSCClassification}
For a Grothendieck topos $\E$, we have the following facts:
\begin{itemize}
\item $\E$ has a local state classifier $\Xi$.
\item $\Xi$ admits the canonical $\land$-semilattice structure such that
\[
\begin{tikzcd}
&X\times Y\ar[ld, "\xi_X \times \xi_Y"']\ar[rd, "\xi_{X\times Y}"]&\\
\Xi\times \Xi\ar[rr,"\land"]&&\Xi
\end{tikzcd}
\] commutes for every pair of objects $(X,Y)$.
\item The complete lattice of internal filters of $\Xi$, which is denoted by $\Filt(\Xi)$, is isomorphic to $\HQ(\E)$.
\[
\HQ(\E) \cong \Filt(\Xi)
\]
\item For an internal filter $F\rightarrowtail \Xi$, the counit $\epsilon_X\colon f^* f_* X \rightarrowtail X$ of the associated geometric morphism $f\colon \E \to \F$ is given by the pullback diagram
\[
\begin{tikzcd}
f^* f_* X \ar[r]\ar[d, "\epsilon_X", rightarrowtail]\ar[dr, phantom, "\lrcorner", very near start]&F\ar[d,rightarrowtail]\\
X\ar[r, "\xi_X"] &\Xi\\
\end{tikzcd}
\]
\end{itemize}
\end{fact}
From the next subsection, we will specialize this theorem to the topos $\Aset$.
% \subsection{A Galois conection for a ringed topos}
\section{The Galois connection between hyperquotients and subalgebras}
% Let $T$ be an equational theory \footnote{or just a functional language}.
\begin{theorem}\label{thm:GaloisConnectionBetweenHQandSubalgebras}
For a Grothendieck topos $\E$, an equational theory $T$, and an $\E$-internal $T$-algebra $A$, we obtain the following Galois connection
\[
\ADJ{\HQ(\Aset)}{}{\Sub(A)}{}.
\]
\end{theorem}
\begin{definition}\label{def:PerfectAlgebra}
An internal $T$-algebra $A$ in a Grothendieck topos $\E$ is \demph{perfect}, if the Galois connection in \Cref{thm:GaloisConnectionBetweenHQandSubalgebras} is an equivalence of the complete lattices.
\end{definition}
\begin{example}
Let $K/\Q$ be a finite-dimensional Galois extension of the field $\Q$. Then the field $K$ is an internal $\Q$-algebra in the topos $\PSh(\Gal(K/Q))$. Then, the Galois connection in \Cref{thm:GaloisConnectionBetweenHQandSubalgebras} is the equivalence between the lattice of normal subgroups of $\Gal(K/Q)$ and the lattice of sub-Galois-extensions $K/M/\Q$. This proves that $K \in \PSh(\Gal(K/\Q))$ is perfect. \memo{Similarly, by replacing $\Q$, we can construct perfect $T$-algebra for any finite-group action topos.}
\end{example}
\memo{Perfect algebra seems to be preserved by hyperconnected geometric morphism}
\section{Hyperconnected geometric morphisms from \texorpdfstring{$\Aset$}{Aset}}
\subsection{The local state classifier of \texorpdfstring{$\Aset$}{Aset}.}
This section describes \demph{the local state classifier} of the topos $\Aset$.
% See \cref{sssec:LSC} or \cite{hora2024internal} for details.
Automata-theoretically, the local state classifier provides a categorical description of congruences, varieties, and Myhill-Nerode theorem.
% Topos-theoretically, the local state classifier classifies \demph{hyperconnected quotients}., which gives a generalized variety theorem.
\begin{definition}We introduce the notion of right-congruences:
\begin{itemize}
\item A \demph{right congruence} on $\A$ is an equivalence relation $\sim$ such that for any $u,v,w \in \MA$, if $u\sim v$ then $uw \sim vw$.
\item For two congruences $\sim $ and $ \sim'$, the order relation $\sim \leq \sim'$ means the condition: for any $u,v \in \MA$, $u\sim v$ implies $u\sim'v$.
\item The poset of all congruences on $\MA$ and their order is denoted by $\Xi$.
\item The action of $\sim \ast w$ is defined by $u (\sim \ast w) v \iff wu \sim wv$.
\end{itemize}
\end{definition}
\begin{proposition}We have the following properties:
\begin{itemize}
\item Those data amount to make $\Xi$ to be an internal semilattice in the topos $\Aset$. Furthermore, this is the local state classifier \cite{hora2024internal} of the topos $\Aset$.
\item In other words, the $\A$-set $\Xi$ is the colimit of all monomorphisms in $\Aset$.
\item The colimit cocone $\{\xi_{X}\colon X=(Q, \delta)\to \Xi\}_{X\in \ob(\Aset)}$ is given by
\[
w\left (\xi_X (q)\right) v \iff qw=qv.
\]
\end{itemize}
\end{proposition}
In particular, the morphism $\xi_{\Lan}\colon \Lan \to \Xi$ captures the notion of Nerode congruence.
\begin{lemma}
\label{lem:NerodeCongruenceAsXi}
The component of the colimit cocone $\xi_{\Lan}\colon \Lan \to \Xi$ sends a language $L$ to \demph{its Nerode congruence} $\sim_{L}$, where
\[
u \sim_{L} v \iff u^{-1}L = v^{-1} L.
\]
\end{lemma}
% This means that the $\A$-set $\Xi$ is the colimit of all monomorphisms in $\Aset$. The colimit cocone will be refered to by $\{\xi_{X}\colon X=(Q, \delta)\to \Xi\}_{X\in \ob(\Aset)}$.
% % To affirmatively answer the question \ref{QuestionInjectivity}, it is enough to answer the following question affirmatively:
% \begin{question}
% Is the function $\xi_{\Lan}$ surjective? In other words, is every congruence induced by a language? \memo{Unless $|\A|<2$, No! Consider an (accessible) automaton (with a start state) with $3$ sinks. At least $2$ of the $3$ sinks define the same language ($\emptyset$ or $\MA$).}
% \end{question}
\begin{proposition}[\cite{hora2024internal} for $\Aset$]
\label{prop:LSCcorresinAset}
There is a bijective correspondence between (equivalence classes of) hyperconnected geometric morphisms from $\Aset$ and the internal filters of $\Xi$, which furthermore correspond to subsets $F \subset \Xi$ such that
\begin{itemize}
\item $F$ is closed under $\MA$-actions,
\item $F$ is closed under taking finite intersections (in particular, $F$ contains the top element), and
\item $F$ is upward closed.
\end{itemize}
\end{proposition}
For a hyperconnected geometric morphism $h\colon \Aset \to \E$, let $F_{h}$ denote the corresponding internal filter of $\Xi$.
\begin{example}
\label{exmp:TheFilterForRegularOrbitFinite}
For the hyperconnected geometric morphism $h\colon \Aset \to \ofAset$, the corresponding filter $F_h$ is the set of all congruences $\sim$ whose quotient set $\MA/{\sim}$ is finite.
\end{example}
\subsection{Example 1: Quotient monoids of \texorpdfstring{$\MA$}{MA}}
\subsection{Example 2: Language Classes}
\section{The correspondence between hyperconnected quotients and language classes}
% \texorpdfstring{$\mapsto$}{mapsto} language class construction}
\subsection{Myhill-Nerode theorem for a hyperconnected geometric morphism}
The following proposition connects languages and hyperconnected quotient:
\begin{proposition}
\label{prop:EquivRecognitionOfLnagByHyperconnected}
For a hyperconnected geometric morphism $h\colon \Aset \to \E$ and a language $L\in \Lan$, the following conditions are equivalent:
\begin{enumerate}
\item $L$ is an element of $h^* h_* \Lan \subset \Lan$\footnote{Since the counit $\epsilon_{\Lan}c\colon h^* h_* \Lan \rightarrowtail \Lan$ is monic, we can regard it as a subset of $\Lan$.}.
\item The corresponding filter $F_{h}$ contains \text{the Nerode congruence} $\sim_{L}$ of $L$ (\cref{lem:NerodeCongruenceAsXi}).
% , which is defined by
% \[
% u \sim_{L} v \iff u^{-1}L = v^{-1} L.
% \]
\item There is a $\A$-set $(Q, \delta)$ in the topos $\E$ (regarded as a full subcategory of $\Aset$), such that $(Q, \delta)$ (with a suitable choice of the initial state $q_0$ and the accept states $F\subset Q$) recognizes $L$.
\end{enumerate}
\end{proposition}
\begin{proof}
By \cref{fact:LSCClassification}, we have the following pullback diagram:
\[
\begin{tikzcd}
h^* h_* \Lan \ar[r]\ar[d, "\epsilon_{\Lan}", rightarrowtail]\ar[dr, phantom, "\lrcorner", very near start]&F_{h}\ar[d,rightarrowtail]\\
\Lan\ar[r, "\xi_{\Lan}"] &\Xi.\\
\end{tikzcd}
\]
This and \cref{lem:NerodeCongruenceAsXi} proves the equivalence between (1) and (2).
Assuming (1), the counit morphism $\epsilon_{\Lan}\colon h^* h_* \Lan \to \Lan$ itself can be regarded as an automaton (without initial state) (see \cref{thm:AutomataAsSliceTopos}). This automaton (with the initial state $L\in h^* h_* \Lan$) recognizes the language $L$. This proves that (1) implies (3).
Lastly, let us assume (3). If a $\A$-set $(Q, \delta)$ recognize the language $L$, then there is a morphism $\chi_F \colon (Q, \delta) \to \Lan$ such that the image of $\chi_F$ contains $L$. If $(Q, \delta)$ is in $\E$, the universality of the counit implies that there is a lift of $\chi_F$ along the counit:
\[
\begin{tikzcd}
&h^* h_* \Lan \ar[r]\ar[d, "\epsilon_{\Lan}", rightarrowtail]\ar[dr, phantom, "\lrcorner", very near start]&F_{h}\ar[d,rightarrowtail]\\
(Q, \delta)\ar[ru, dashed]\ar[r, "\chi_F"]&\Lan\ar[r, "\xi_{\Lan}"] &\Xi.\\
\end{tikzcd}
\]
This proves that $L$ is an element of $h^* h_* \Lan$.
\end{proof}
\begin{remark}[Myhill-Nerode theorem]
In the case where $\E = \ofAset$, \cref{prop:EquivRecognitionOfLnagByHyperconnected} is exactly the \demph{Myhill-Nerode theorem}, since the following pullback daigram
\[
\begin{tikzcd}
\Reg \ar[r]\ar[d, "\epsilon_{\Lan}", rightarrowtail]\ar[dr, phantom, "\lrcorner", very near start]&F_{h}\ar[d,rightarrowtail]\\
\Lan\ar[r, "\xi_{\Lan}"] &\Xi.\\
\end{tikzcd}
\]
states that a language $L$ is regular if and only if its Nerode congruence $\sim_L$ has finitely many equivalece classes.
Therefore, we can regard \cref{prop:EquivRecognitionOfLnagByHyperconnected} as a topos-theoretic generalization of the Myhill-Nerode theorem.
\end{remark}
% In the theory of formal languages, it is central to study \demph{classes of languages}:
% \begin{definition}
% For a hyperconnected geometric morphism $h \colon \Aset \to \E$ from the Grothendieck topos $\Aset$,
% \begin{itemize}
% \item the \demph{associated class of language} is the subobject $\LC_h \coloneqq h^{\ast}h_{\ast} \Lan \rightarrowtail \Lan$ obtained as the component of the counit\footnote{Rigorously, one need to take the strict image of the component of the counit.}.
% \item a language $L$ is \demph{recognized by $h$} if it is an element of (the underlying set of) $L \in \LC_h$.
% \end{itemize}
% \end{definition}
% \begin{definition}
% For a hyperconnected geometric morphism $h\colon \Aset \to \E$, \demph{the associated language class} is the set of languages satisfying the equivalent conditions in \cref{prop:EquivRecognitionOfLnagByHyperconnected}, which is denoted by $\LC_{h}$.
% \end{definition}
% \begin{definition}
% We say that a hyperconnected geometric morphism $h\colon \Aset \to \E$ \demph{recognizes} a language $L$, if they satisfy the equivalent conditions of \cref{prop:EquivRecognitionOfLnagByHyperconnected}.
% \end{definition}
\subsection{The Galois connection between language recognition and syntactic monoids.}
\begin{definition}
We say that a hyperconnected geometric morphism $h\colon \Aset \to \E$ \demph{recognizes} a language $L$, if they satisfy the equivalent conditions of \cref{prop:EquivRecognitionOfLnagByHyperconnected}.
The set of languages recognized by $h\colon \Aset \to \E$ is denoted by $\LC_{h}$ (or $\LC(\E)$ by abuse of notation).
\end{definition}
As we have seen, the set $\LC_h$ is in fact a sub$\A$-set $\LC_h = h^* h_* (\Lan) \xrightarrow{\epsilon_{\Lan}} \Lan$, constructed by the pullback diagram
\[
\begin{tikzcd}
\LC_{\Lan}= h^* h_* \Lan \ar[r]\ar[d, "\epsilon_{\Lan}", rightarrowtail]\ar[dr, phantom, "\lrcorner", very near start]&F_{h}\ar[d,rightarrowtail]\\
\Lan\ar[r, "\xi_{\Lan}"] &\Xi.\\
\end{tikzcd}
\]
The fact that $\LC_h$ is a sub$\A$-set is equivalent to saying that it is quotient-stable:
\begin{definition}\label{dfn:quotientStable}
A \demph{language class} is a subset $\LC \subset \Lan$ of the set of languages $\Lan$. A language class is \demph{quotient-stable} if $\LC$ is a sub $\A$-set of $\Lan$, i.e., if $\forall L\in \LC, \forall w\in \MA, \; w^{-1}L \in \LC$.
The set of quotient-stable language classes will be denoted by $\qslc$.
\end{definition}
% \subsection{Galois correspondence}
\begin{theorem}\label{thm:GaloisConnection}
This construction $h \mapsto \LC_h$ provides a Galois connection between two complete lattices $\HQ(\Aset)$ and $\qslc$ with a left adjoint which will be denoted by $\SQ$:
% \[
% \ADJ{\HQ(\Aset) \cong \Filt(\Xi)}{\LC = \xi_{\Lan}^{\ast}}{\Sub(\Lan)\cong \qslc}{}.
% \]
% The left adjoint in \cref{thm:GaloisConnection} will be denoted by $\SQ$.
\[
\ADJ{\HQ(\Aset)}{\LC}{\qslc}{\SQ}.
\]
\end{theorem}
\begin{proof}
We will prove it via the following paraphrase:
\[
\ADJ{\HQ(\Aset) \cong \Filt(\Xi)}{\LC = \xi_{\Lan}^{\ast}}{\Sub(\Lan)\cong \qslc}{}.
\]
Two isomorphisms above are due to \cref{fact:LSCClassification} and the fact that a language class is quotient-stable if and only if it is a sub$\A$-set of $\Lan$. To prove that the construction $\LC$ has a left adjoint, it is enough to prove that it preserves all infimums. Since the construction $\LC$ is just a pullback along the morphism $\xi_{\Lan}$, the proof is completed.
\end{proof}
Because this is a Galois connection, we automatically obtain the following bijective correspondence between \dq{fixed points.}
\begin{corollary}\label{Cor:TheCorrespondence}
There is a canonical isomorphism between two complete lattices
\[
\Image(\SQ) \cong \Image(\LC).
\]
\end{corollary}
\begin{proof}
This is the equivalence of categories induced by the adjunction \cref{thm:GaloisConnection}.
\end{proof}
We have reached an abstract viewpoint. In the following subsection, we will observe through concrete examples how these abstract \cref{thm:GaloisConnection} and \cref{Cor:TheCorrespondence} subsume some concrete theories of automata. In order to calculate $\SQ$, let us explicitly write down the construction $\SQ$.
\begin{proposition}[Concrete description of $\SQ$]
For a quotient-stable language class $C$, the hyperconnected geometric morphism $\SQ(C)\colon \Aset \to \E$ corresponds to the filter $F_{\SQ(C)}\subset \Xi$ defined by
\[
F_{\SQ(C)} = \{{\sim} \in \Xi \mid \text{There exists a finite family of languages $L_1 \dots L_k \in C$, such that $\bigwedge_{i=1}^{k} {\sim_{L_i}} \leq {\sim}$}\}
\]
\end{proposition}
\begin{proof}
$F_{\SQ(C)}$ should be the minimum internal filter of $\Xi$ that contains $\xi_{\Lan}(L)$ for every $L \in C$, in other words, $F_{\SQ(C)}$ is the closure of $\{\sim_L \mid L \in C\}$ by the three operations in \cref{prop:LSCcorresinAset}.
% Such closure must contain $\{\simeq \in \Xi \mid \text{There exists a finite family of languages $L_1 \dots L_k \in C$, such that $\bigwedge_{i=1}^{k} {\sim_{L_i}} \leq {\sim}$}\}$
\end{proof}
For a quotient-stable language class $C$, $\SQ(C)$ is a hyperconnected geometric morphism $\Aset \to \E$. However, if it is not confusing, it will be referred to just by the codomain topos $\E$.
\subsection{The construction \texorpdfstring{$\SQ$}{SQ} subsumes syntactic monoids}
This subsection aims to explain how the construction $\SQ$ works, and generalizes the construction of syntactic monoid.
We will divide this subsection into two parts:
\begin{enumerate}
\item Hyperconnected geometric morphisms subsume surjective monoid homomorphisms.
\item Construction $\SQ$ subsumes syntactic monoids.
\end{enumerate}
\para{Hyperconnected geometric morphisms subsume surjective monoid homomorphisms}
The next fact in topos theory is the key to connect surjective monoid homomorphisms and hyperconnected geometric morphisms.
\begin{definition}
A geometric morphism
\[
\ADJ{\E}{f_*}{\F}{f^*}
\]
is essential, if $f^*$ has a left adjoint.
\end{definition}
\begin{fact}
A full and bijective-on-objects functor $F\colon \C \to \D$ induces a hyperconnected and essential geometric morphism
\[
\ADJ{\PSh(\C)}{\mathrm{Ran}_{F}}{\PSh(\D)}{ {-}\circ F}.
\]
Furthermore, this construction provides a one-to-one correspondence between
\begin{itemize}
\item (isomorphism classes of) full and bijective-on-objects functors $F\colon \C \to \D$ and
\item
(equivalence classes of) hyperconnected and essential geometric morphisms from $\PSh(\C)$.
\end{itemize}
\end{fact}
\begin{proof}
The first half is easy to prove and well-known. For example, you can find the details in \cite{johnstone2002sketchesv1}.
For the latter, \cite{el2002simultaneously} proves that every essential and connected geometric morphism from $\PSh(\C)$ is induced by a bijective-on-objects (and lax-epi) functor $F\colon \C \to \D$. If the induced essential geometric morphism $\mathrm{Lan}_{F} \dashv {-}\circ F \dashv \mathrm{Ran}_{F}$ is hyperconnected, the unit $\C(-, c) \twoheadrightarrow \mathrm{Lan}_{F}(\C(-,c)) \circ F = \D(F{-}, Fc)$ is epic, which means that $F$ is full.
\end{proof}
% In particular, surjective monoid homomorphisms from $\MA$ are in one-to-one correspondence with hyperconnected and essential geometric morphism from $\Aset$.
% \begin{proposition}
% For a hyperconnected geometric morphism $h\colon \Aset\to \E$, the following conditions are equivalent:
% \begin{enumerate}
% \item $h$ is essential
% \item There is a surjective monoid homomorphism $\phi \colon \MA \twoheadrightarrow N$ such that $h$ is (equivalent to) the geometric morphism induced by $\phi$
% \[
% \Aset = \PSh(\MA) \xrightarrow{\phi_{\ast}} \PSh(N).
% \]
% \item The corresponding internal filter $F \subset \Xi$ is principal, in the sense that there is a minimum element ${\sim} \in F$\footnote{This is not equivalent to the existence of the minimal \demph{global} element $1 \to F$, which should be the fixed point of the quotient-action.}.
% % such that ${\sim} \leq {\sim'}$ for every ${\sim'}\in \Xi$
% \end{enumerate}
% \end{proposition}
\begin{definition}
A right congruence ${\sim}$ is \demph{a two-sided congruence}, if
\[
v\sim v' \implies uvw \sim uv'w
\]
for any words $u,v,v',w \in \MA$.
\end{definition}
\begin{lemma}
For a right congruence ${\sim} \in \Xi$, the following conditions are equivalent:
\begin{enumerate}
\item $\sim$ is a two-sided congruence.
% , in the sense that
% \[
% v\sim v' \implies uvw \sim uv'w
% \]
% for any words $u,v,v',w \in \MA$.
\item ${\sim}$ is a \demph{congruence of monoid}, in the sense that the quotient set $\MA/ {\sim}$ admits a (necessarily unique) monoid structure such that the quotient map \[\MA \twoheadrightarrow \MA/{\sim}\]is a monoid homomorphism.
\item For any word $w\in \Xi$, ${\sim} \leq (\sim\ast w)$.
\item Its upward closure $\{{\sim'}\mid {\sim}\leq {\sim'}\}$ is an internal filter of $\Xi$.
\end{enumerate}
\end{lemma}
\begin{proposition}
There is a one-to-one correspondence between (equivalence classes of)
\begin{enumerate}
\item Hyperconnected and essential geometric morphism $h\colon \Aset \to \E$.
\item Surjective monoid homomorphism $\phi \colon \MA \twoheadrightarrow N$.
\item Two-sided congruence ${\sim}\in \Xi$.
\end{enumerate}
Furthermore, for a language $L\in \Lan$, the following conditions are equivalent:
\begin{enumerate}
\item $h$ recognizes $L$, i.e., $L\in \LC(h)$.
\item $\phi$ recognizes $L$.
% Surjective monoid homomorphism $\phi \colon \MA \twoheadrightarrow N$.
\item ${\sim} \leq {\sim}_{L}\in \Xi$.
\end{enumerate}
\end{proposition}
\begin{remark}[Detail of the correspondence]
Let us clarify the correspondence between them. Between (1) and (2), from (2) a surjective monoid homomorphism $\phi\colon \MA \to N$, the corresponding (1) Hyperconnected and essential geometric morphism is given by
\[
\ADJ{\PSh(\MA)}{\mathrm{Ran}_{\phi}}{\PSh(N)}{ {-}\circ \phi}.
\]
The converse is a little more difficult\footnote{The monoid can be recovered as an endomorphism monoid of the forgetful functor $\E \to \Aset \to \Set$}.
Between (2) and (3), from (2) we can define $w\sim v$ by $\phi(w)=\phi(v)$. The converse construction is just by considering the surjection $\MA \twoheadrightarrow N$.
Between (1) and (3), from (1), the corresponding internal filter $F\subset \Xi$ has a minimum element ${\sim}\in \Xi$. Conversely, for a two-sided congruence ${\sim}$, its upward closure $\{{\sim'}\mid {\sim}\leq {\sim'}\}$ is an internal filter, and the corresponding hyperconnected geometric morphism to $F$, is what we want.
\end{remark}
\para{Construction $\SQ$ subsumes syntactic monoids}
By abuse of notation, for a language $L$, let $\SQ(L)$ denote $\SQ(\{w^{-1}L\mid w \in \MA\})$. This is reasonable, since the Galois connection \cref{thm:GaloisConnection} can be extended to all langugage classes $\Pow(\Lan)$
\[
\begin{tikzcd}[column sep = small]
{\HQ(\Aset)}
\ar[rr, shift right=1.3ex, "{\LC}"']
&\perp&
{\qslc}
\ar[ll, shift right=1.3ex,"{\SQ}"'] \ar[rr, shift right=1.3ex, hook]
&\perp&
{\Pow(\Lan)},
\ar[ll, shift right=1.3ex,""']
\end{tikzcd}
\]
and $\SQ(L)$ is none other than the value of the composite left adjoint at $\{L\}$. We call $\SQ(L)$ \demph{the syntactic quotient} of the language $L$.
% \begin{lemma}
The universality of $\LC$ implies that,
% for a language $L$ and a hyperconnected geometric morphism $h\colon \Aset \to \E$, the following conditions are equivalent:
% \begin{enumerate}
% \item $L \in \LC(h)$.
% \item $\SQ(L)\leq h$ in $\HQ(\Aset)$.
% \end{enumerate}
% % \end{lemma}
% In particular,
\textbf{ $\SQ(L)$ is the minimum hyperconnected quotient that \demph{recognizes} $L$.}
The Myhill-Nerode theorem states that a language $L$ is regular if and only if its orbit $\{w^{-1}L\mid w\in \MA\}$ is finite. By analogy, we define the regularity of right congruence as follows.
\begin{definition}
A right congruence ${\sim}$ is \demph{regular}, if its orbit $\{{\sim}\ast w\mid w\in \MA\}$ is finite.
\end{definition}
Notice that if a language $L$ is regular, then its Nerode congruence $\sim_L$ is also regular.
\begin{remark}
\memo{Pullback diagram and normalizer operator}
\end{remark}
\begin{proposition}
For a language $L$ whose Nerode congruence $\sim_{L}$ is regular (in particular for a regular language), its syntactic quotient $\SQ(L)$ is equal to the one induced by the canonical surjective monoid homomorphism $\MA \twoheadrightarrow M_L$ to the syntactic monoid $M_L$.
\[
\begin{tikzcd}
\SQ(L)\colon \Aset \ar[r, "", twoheadrightarrow] &\PSh(M_{L})
\end{tikzcd}
\]
\end{proposition}
\subsection{Examples and calculations of the correspondence}
This subsection aims to give some concrete examples of the correspondence \cref{thm:GaloisConnection} and \cref{Cor:TheCorrespondence}.
\para{Toy examples}
Let us see some of the easiest examples.
\begin{example}[Maximum element]
The identity geometric morphism $\id_{\Aset}\colon \Aset \to \Aset$ is the maximum hyperconnected quotient. The associated language class $\LC_{\id_{\Aset}}$ is the set of all languages. Conversely, the hyperconnected quotient $\SQ(\Lan)$ is $\id_{\Aset}$, since there is a language $L$ whose Nerode congruence ${\sim_{L}}$ is trivial \footnote{If $\abs{\A}\leq 1$, it is easy to construct such a language. For the case where $\abs{\A}>1$, see \cref{Exmp:SquareLanguage}.}.
\[
\begin{tikzcd}
\Aset \ar[r, bend right, "\LC"', mapsto ] & \Lan \ar[l, bend right, "\SQ"', mapsto]
\end{tikzcd}
\]
\end{example}
\begin{example}[Minimum element]
Since $\SQ$ is a left adjoint, it sends the empty language class $\{\}$ to the smallest hyperconnected quotient, which is
the global section geometric morphism \[
!\colon \Aset \to \Set.\]
% is hyperconnected.
The corresponding class $\LC_{\Set}$ is the set $\{\emptyset, \MA\}$.
\[
\begin{tikzcd}
&\{\}\ar[ld, "\SQ"', mapsto]\\
\Set \ar[r, bend right, "\LC", mapsto ] & \{\emptyset, \MA\} \ar[l, bend right, "\SQ", mapsto]
\end{tikzcd}
\]
\end{example}
\para{Integers, and profinite integers}
\begin{example}[Regular cases]
For a regular language $L$, its syntactic quotient is given by
\[
\begin{tikzcd}
\SQ(L)\colon \Aset \ar[r, "", twoheadrightarrow] &\PSh(M_{L})
\end{tikzcd}
\]
since its Nerode congruence $\sim_L$ is regular. For example, for a positive interger $n>0$, let us consider the (regular) language $L_n \coloneqq \{w\mid \abs{w}_a \cong \abs{w}_b \mod n\}$, where $\abs{w}_a$ (respectively, $\abs{w}_b$) denotes the number of $a$ (respectively $b$) in the word $w$.
Its Nerode congruence $\sim_{L_n}$ is given by
\[
w\sim_{L_n} w' \iff \abs{w}_a - \abs{w}_b \cong \abs{w'}_a - \abs{w'}_b \mod n,
\]
and
its syntactic quotient is given by
\[
\begin{tikzcd}
\SQ({L_n})\colon \Aset \ar[r, "", twoheadrightarrow] &\PSh(\Z/n\Z).
\end{tikzcd}
\]
\end{example}
\begin{example}[Non-regular example]
Let us consider the (non-regular) language $L_0\coloneqq \{w\mid \abs{w}_a = \abs{w}_b\}$, where $\abs{w}_a$ (respectively, $\abs{w}_b$) denotes the number of $a$ (respectively $b$) in the word $w$. Its Nerode congruence $\sim_{L_0}$ is given by
\[
w\sim_{L_0} w' \iff \abs{w}_a - \abs{w}_b = \abs{w'}_a - \abs{w'}_b,
\]
which is regular, since it is fixed by the word action.
Then, its syntactic quotient is given by
\[
\begin{tikzcd}
\SQ({L_0})\colon \Aset \ar[r, "", twoheadrightarrow] &\PSh(\Z).
\end{tikzcd}
\]
\end{example}
\begin{example}
The geometric morphism $\Aset \to \mathbf{Cont}(\hat{F_{\A}})$ to the topos of continuous actions of the profinite completion of the free group on $\Sigma$ is hyperconnected. The corresponding class is the set of \demph{group languages} (\memo{cite}).
\end{example}
\begin{example}
Similarly, in the case where $\A$ is a singleton, the geometric morphism $\Aset = \sigma\text{-}\Set \to \mathbf{Cont}(\mathbb{Z}_p)$ to the topos of continuous actions of the topological group of $p$-adic integers is hyperconnected. The corresponding class is the set of languages $L$ such that $L$ is periodic and its period is a power of $p$.
\end{example}
\begin{example}
The geometric morphism $\Aset \to \sigma\text{-}\Set = \PSh(\N)$ to the topos of discrete dynamical systems (also known as difference sets), induced by the monoid homomorphism $\MA \to \N\colon w \mapsto (\text{the length of }w)$, is hyperconnected. The corresponding class is the set of \demph{length languages} $L$, which is a language $L$ such that if $w$ and $v$ have the same length and $w \in L$, then $v \in L$.
\end{example}
\begin{example}
The geometric morphism $\Aset \to \Aset_{\mathrm{e.f.}}$ to the topos of eventually fixed $\A$-sets is hyperconnected. The corresponding class is the set of \demph{prefix languages} $L$, which is a language $L$ such that there exists a finite set of words $P$, and a word $w \in \Lan$ belongs to $L$ if and only if at least one element of $P$ is a prefix of $w$.
\end{example}
\begin{example}
\cite{lawvere1989display, pin2010mathematical}
\end{example}
\begin{example}
Commutative language
\end{example}
\begin{example}
Lattice
\end{example}
\begin{example}[Syntactic monoid]
\end{example}
\begin{table}[ht]
\centering
\begin{tabular}{c|c}
$\E = \mathrm{cod}(h)$& $\Lan_h$\\ \hline
$\Aset$& $\Lan$\\ \hline
$\ofAset$&$\Reg$\\ \hline
$\mathbf{Cont}(\hat{F_{\A}})$& Group languages\\ \hline
$\sigma\text{-}\Set$ & Length languages\\ \hline
$\Aset_{\mathrm{e.f.}}$&Prefix languages\\ \hline
$\Set$&$\{\emptyset, \A\}$\\
\end{tabular}
\caption{A few examples of associated classes}
\label{TableExampleofHQcorrespondence}
\end{table}
\begin{example}[Regular languages: Profinite words in \cite{pin2010mathematical}, conceptually]
Let $\ofAset$ be a full subcategory of $\Aset$ that consists of orbit-finite automata. Then the embedding $\ofAset\to \Aset$ has a right adjoint, and provides a hyperconnected geometric morphism $q\colon \Aset \to \ofAset$. A language $L$ is a $q$-language if and only if $L$ is regular!
\end{example}
\begin{example}[Group languages]
Let $\pFA$ be the profinite completion of the free group $\FA$, equipped with the canonical profinite topology. Let $\mathrm{Cont}(\pFA)$ be the topos of continuous right $\pFA$ actions (see \cite{maclane1994sheaves}). Then, the dense monoid morphism $\MA \to \pFA$ induces a hyperconnected geometric morphism $q\colon \Aset \to \mathrm{Cont}(\pFA)$. A language $L$ is a $q$-language, if and only if $L$ is a group language.
\end{example}
\begin{conjecture}
The lattice of hyperconnected quotients of $\ofAset$ is isomorphic to \memo{local varieties of?} regular languages and finite $\A$-monoids
\end{conjecture}
\printbibliography
\end{document}