Topoi II 五重対応
## Trigger
*Topoi of automata II* の完成に向け，hora-tex の本文・proof audit・関連する未解決瓶を横断して，orbit-finite（= every orbit finite）な \(\Sigma^*\)-sets の toposについて中心予想を再構成した．Adámek--Milius--Myers--Urbat の local Eilenberg theorem，Gehrke--Grigorieff--Pin の equational theory，Reiterman 型定理，Uramoto の semi-Galois theory，Morgan Rogers の topological monoid action topoi と比較した．
## Result
有限 alphabet \(\Sigma\) と \(M=\Sigma^*\) に対し，\(\mathcal A=\mathbf{PSh}(M)\)，\(\mathcal A_{\mathrm{of}}\subseteq\mathcal A\) を every orbit finite な \(M\)-sets の full subtopos とする．また \(\Xi_f\) を finite-index right congruences の \(M\)-setとする．すると標準的な complete-lattice isomorphisms
\[
\operatorname{HQ}(\mathcal A_{\mathrm{of}})
\cong \operatorname{Filt}(\Xi_f)
\cong \operatorname{LV}(\Sigma)
\cong \operatorname{LPV}(\Sigma)
\cong \operatorname{ProfQuot}(\widehat{M})
\cong \operatorname{ProfCong}(\widehat M)^{\mathrm{op}}
\]
が得られる．ここで
- \(\operatorname{LV}(\Sigma)\) は regular languages の Boolean subalgebrasで，left/right derivativesの双方で閉じるもの，
- \(\operatorname{LPV}(\Sigma)\) は finite \(\Sigma\)-generated monoids の classesで，quotients と finite subdirect products で閉じるもの，
- \(\operatorname{ProfQuot}(\widehat M)\) は free profinite monoid \(\widehat M\) の profinite quotient monoids，
- \(\operatorname{ProfCong}(\widehat M)\) は quotient が profinite になる closed two-sided congruences（すべての closed congruences ではない）
である．
language-sideの写像は
\[
\mathbb L(F)=\{L\subseteq M\mid \sim_L\in F\},\qquad
\mathcal T(C)=\langle\sim_L\mid L\in C\rangle
\]
であり，Topoi II の既存の Galois connection \(\mathcal T\dashv\mathbb L\) は interval \(\operatorname{HQ}(\mathcal A_{\mathrm{of}})\) 上で同型へ強化される．
## Proof spine
1. Hyperconnected quotients of a hyperconnected quotient are the lower interval of ambient hyperconnected quotients．これにより
\[
\operatorname{HQ}(\mathcal A_{\mathrm{of}})\cong\operatorname{Filt}(\Xi_f).
\]
2. finite-index right congruence \(\rho\) の各 equivalence class \(C_i\subseteq M\) を language とみると，それぞれ regular で
\[
\rho=\bigwedge_i\sim_{C_i}.
\]
したがって finite-index filter は Nerode congruences から復元できる．
3. two-sided core
\[
\rho^\sharp:=\bigwedge_{w\in M}(\rho*w)
\]
は \(\rho\) 以下最大の two-sided congruence．\(\rho\) が finite-index なら orbit \(\{\rho*w\}\) は有限なので，これは finite meet で filter 内に残る．
4. 2と3から \(\mathbb L\mathcal T=\mathrm{id}\)，\(\mathcal T\mathbb L=\mathrm{id}\) および \(F\leftrightarrow F\cap\Xi^2\) を得る．
5. \(F\) に対し
\[
N_F=\varprojlim_{\theta\in F\cap\Xi^2}M/\theta
\]
と置けば profinite monoidであり，\(\mathcal E_F\simeq\mathbf{Cont}(N_F)\)．
6. compactness により，local pseudovariety は profinite equations \(u=v\) で公理化できる．逆に equations の models は quotients と finite subdirect products で閉じる．これは fixed-alphabet Reiterman theoremである．
## Important correction
\(\operatorname{HQ}(\mathcal A_{\mathrm{of}})^{\mathrm{op}}\) を「\(\widehat M\) 上の全 closed congruences」と同一視してはいけない．安全な対象は，quotient が再び profiniteになる congruences，すなわち intersections of clopen finite-index congruences である．一般の profinite algebraには closed congruence whose quotient is not profinite が存在しうる．
## Examples
- top: all regular languages / all finite \(\Sigma\)-generated monoids / \(\widehat M\)．
- bottom: \(\{\varnothing,M\}\) / trivial monoid / one-point profinite quotient．
- group languages: finite \(\Sigma\)-generated groups / free profinite group quotient．
- star-free languages: finite aperiodic \(\Sigma\)-generated monoids．
- one-letter alphabet: \(p\)-power periodic languagesに \(\mathbb Z_p\) が対応する．
## Literature comparison
local variety \(\leftrightarrow\) local pseudovariety自体は既知であり，その新規性を主張しない．本結果の候補的新規性は，同じ lattice を local state classifier によって **fixed ambient automata topos の hyperconnected quotient intervalそのもの** と同定し，\(\mathbb L/\mathcal T\) を具体的に inverseとして与える点にある．Uramoto の semi-Galois/topos-theoretic formulationとは競合ではなく，LSCによる quotient-topos側の明示化として比較する．
## Goal
この五重対応を *Topoi of automata II* の主定理に昇格し，現在の abstract の bijection claim，local-variety conjecture，profinite-equation節を一つの定理として統合する．
## Terminology correction: prodiscrete topology versus prodiscrete monoid
Morgan Rogersは次を明確に区別する．
- **prodiscrete monoid**: discrete monoids の projective limitとして TopMon 内で得られるもの（Definition 2.19）．
- **monoid endowed with a prodiscrete topology**: underlying topological spaceが discrete sets の projective limit topologyをもつ topological monoid．coordinate quotientsは monoidsである必要がない．
任意の hyperconnected quotientから得られる canonical complete powder monoid \(L_F\) は常に後者である（Theorem 3.20）．前者になる必要十分条件は filterが two-sided congruences の basisを持つこと（Corollary 3.33）．従って一般の language classについても topological/prodiscrete-topology representationは存在し，Dyckが否定するのは discrete monoids の pro-objectとしての representationだけである．regular/orbit-finite側ではこの distinctionが消え，canonical monoidは profiniteになる．