Games の ex/reg 完備化は層 topos

Trigger

Gameの圏はtoposか「Gameの圏はtoposか」は Remark B.27 で否定的に閉じたが，その Notion 原案にあった「有限ゲームのなす site」の方向を，Games の exact completion と突き合わせて追った（2026-09-26，hora-tex PR #216 の explain-math PDF 4 本）．

Idea

定理． Games = RecCoalg(P_f) は regular（epi = 全射 = regular epi，pullback 安定）かつ infinitary extensive だが exact でない（Δ∪Γ_σ ⊂ Star₂×Star₂ は 6 元の非有効同値関係）．その ex/reg 完備化は有限ゲームの圏上の coherent 位相の層 topos と同値：

Map(Games) ≃ ℰ := Sh(Games_fin, J_coh), N(X) = Games(−, X)|_{Games_fin}.

鍵は (i) N(X) の部分層はすべて部分ゲームから来る，(ii) N は余積・全射・filtered 余極限を保つ．Ω_ℰ = N(Ω_Games)（truth-closed HF 集合）．

ℰ の性質．

• coherent topos ではない：1 = N(V)（V = HF 集合全体）は quasi-compact でない．高さ < n の部分終対象 N(V_{<n}) が開被覆を与え，各開部分 topos ℰ_n ≃ Sh((Games_fin)_{<n}, J_coh) は coherent．よって点を十分にもち，分類する理論は「各高さの coherent 理論 + 無限選言 ⊤ ⊢ ⋁_n(高さ<n)」の geometric 理論．
• ℰ_1 = Set は稠密な開点で Sh_¬¬(ℰ) = Set（点 = 終端位置関手 T，{∗} が唯一の projective 有限ゲーム）．
• Boolean でない（{t} ⊂ Star₁ に補元なし），localic でない（N(Star₂) は部分終対象で覆えない）．localic 反映は (V_ω, ∈⁺) 上の前層 topos．
• 点の例：perfect Stone 空間 S に対し F_S(X) = {(x, e) : succ x ⊆ 終端, e: S ↠ succ x 連続全射}．全点が「Stone ゲーム」かは未確認．
• 対象 (X,R) は「ゲーム X と双模倣の証拠（証明木）の体系 R」．Games に商があるのは R が kernel pair（全証拠）のときだけ．Star₂/ℤ₂ = N(Star₂)/(Δ∪Γ_σ) が最小の非 Games 対象で，N(Star₁) をその商にもつ．

一般論． ex/reg は冪等（exact なら Map(C) ≃ C），ex/lex は冪等でない．Map(C) が Grothendieck topos になる十分条件：regular + infinitary extensive + 小生成集合（Giraud，Worrell Cor 5.5.7 の Coalg(F) と同型の議論）．Menni の判定（weak dependent product + generic proof）は ex/lex 版で，ex/reg 版は未確認．realizability（Eff ≃ Asm_ex/reg）は記憶引用で未検証．

Conway 和． + は lex でない（(Star₂×{Star₁}Star₂)+Star₁ の根 7 個に対し (Star₂+Star₁)×{Star₁+Star₁}(Star₂+Star₁) の根は 7·127 個）ので Map の 2-関手性では降りない．代わりに (Games_fin, +) 上の Day convolution の層化 ⊕ が ℰ の対称 monoidal closed 構造を与え（A+− が J_coh 被覆を保つ），N は強 monoidal，有限ゲームでは N(A)⋆N(B) = N(A+B) と層化不要．Reflected Day convolution の「反映された Day convolution」が ℰ では反映なしで成立．種（FinBij，Cauchy 積）・nominal 集合（Schanuel，separated 積）と同じ「有限対象の余積に沿う Day convolution の層化」の型．

Goal

• ℰ の点の分類（Stone ゲームで尽きるか），前層 topos かどうか（否定的と予想）．
• Leibniz 則 D(F⊕G) ≅ DF⊕G ⊔ F⊕DG（D = [N Star₁, −]）の成否と，Differential structures of games の differential 構造の ℰ での定式化（Loregian–Trimble の differential 2-rig）．
• ex/reg 版 Menni 判定を Menni 本人に問う：regular + Ω で十分か．
• ℰ の内部 hom [NX, NY](A) = ∫_B Set(Games(B,X), Games(A+B,Y)) が N の像に入るかで Internal hom for Conway addition の内部 hom を読む．

Personal context

証明は hora-tex papers/games-recursive-coalgebras/ の explain-map-games-coherent-sheaves-2026-09-26.tex，explain-topos-properties-2026-09-26.tex，explain-exreg-conway-day-2026-09-26.tex，および topos-checks-1-4-proofs-2026-09-26.md にある．検算済みと未検証の区別は各 PDF に明記．

@misc{sumire:2610.00003:42:v1,
  author = {hora},
  title = {{Games の ex/reg 完備化は層 topos}},
  year = {2026},
  note = {SUMIRE:2610.00003/42, v1},
  url = {https://sumire.aiformath.jp/p/2610.00003/n/42/v/1}
}