Conway addition の internal hom：cofree game 内の最大 compatible 部分game

このreportはDraft PR上の提案であり、洞のmergeまでは正本ではない。

判定

中心結果は theorem candidate / reviewed である。origin/main の瓶 g6c8vx は、Conway addition の右随伴の具体形を問い、R(Set(UG,UH)) 内で全子孫にoption等式を課す候補を既に記録している。以下はその候補について、外部のadjoint functor theoremや文献locatorを使わず、evaluationとcurryingの普遍性を直接証明する。

主張の範囲は瓶で定義されたimpartial recursive P_fin-coalgebraの圏Gameである。古典的player-switching、partisan strategy categoryとの一致、任意のproduct-liftingへの一般化は本claimに含めない。

1. Game、Conway addition、cofree game

Gameのobject Xは集合UXと有限option写像

θ_X:UX→P_fin(UX)

からなり、各positionから始まる無限pathを持たない。射 f:X→Y はexactなcoalgebra morphism、すなわち全xについて

θ_Y(f(x))=f[θ_X(x)]

を満たす写像である。単なるgraph morphismが与える包含ではなく、option像の等号を要求する。

Conway additionは

U(G+K)=UG×UK

θ_{G+K}(g,k)=(θ_G(g)×{k})∪({g}×θ_K(k))

で定まる。射p,qに対する p+q は基礎集合上で (g,k)↦(p(g),q(k)) であり、上のoption等号から+はbifunctorになる。

集合S上のcofree gameをR(S)と書く。そのpositionはS-labelled hereditarily finite set

t=(T_t,a_t)

であり、T_t は有限な子position集合、a_t∈S はlabelである。optionとcounitは

θ_R(t)=T_t, ε_S(t)=a_t

である。Hora v3ではこれは§B.2、Definition B.13とProposition B.14に記述されている。

ここでcofree transposeをreport内で直接再導出する。game Kとset map σ:UK→S に対し、各kから始まる有限pathの木を考える。これは有限分岐である。もしpath長が非有界ならKönigの補題により無限branchができ、gameのfinite-time条件に反する。従って各kには最大path長 ρ(k)∈N がある。ρに関する帰納で

σ♭(k)=({σ♭(k′) | k′∈θ_K(k)},σ(k))

と定められる。定義から

θ_R(σ♭(k))=σ♭[θ_K(k)], ε_S(σ♭(k))=σ(k)

なので σ♭:K→R(S) はgame morphismである。逆にこれら二等式を満たすhがあれば、h(k)のlabelはσ(k)、子集合は {h(k′)|k′∈θ_K(k)} に強制される。ρに関する帰納で h(k)=σ♭(k) となる。従ってtransposeは存在し一意である。

この議論はgame全体のcarrierが有限であるとは仮定しない。各rooted reachable partが有限であれば足りる。R(S)はfinite labelled trees全体なので集合であり、size上のproper-class問題もない。

2. internal hom候補のpositionと最大性

二つのgames G,Hを固定し

S=Set(UG,UH)

と置く。R(S) のposition uのlabelを関数 a_u:UG→UH と読む。u自身を含む全descendant wと全 g∈UG について

θ_H(a_w(g))={a_w(g′) | g′∈θ_G(g)}∪{a_v(g) | v∈θ_R(w)} (E)

を満たすu全体を A(G,H) とする。

この定義が実際に部分gameを与えることを確認する。u∈A(G,H) かつ v∈θ_R(u) なら、vとその全descendantはuのdescendantである。従って(E)はv以下でも成立し、v∈A(G,H) である。ゆえにAはoptionについて下向き閉で、option写像をR(S)から制限した部分gameになる。

次にset-level evaluationを

ev_{G,H}:G+A(G,H)→H, ev_{G,H}(g,u)=a_u(g)

とする。(g,u) のConway optionを評価した像は

{a_u(g′) | g′∈θ_G(g)}∪{a_v(g) | v∈θ_A(u)}

であり、(E)によってちょうど θ_H(a_u(g)) に等しい。従ってevaluationはgame morphismである。

Aはこの性質を持つ最大の部分gameでもある。実際、B⊆R(S) を部分gameとし、同じlabel evaluation ev_B:G+B→H がgame morphismだとする。任意の u∈B でmorphism等号をConway option式へ展開すると(E)がuで成立する。Bは子について閉じているのでuの全descendantもBに属し、各descendantで同じ等号が成立する。従って u∈A(G,H)、よって B⊆A(G,H) である。

以上でAは「evaluationがexactなgame morphismになるR(S)内の最大部分game」という、定義と独立な特徴づけも持つ。

3. image subgame因子化

後のcurryingで使う像の議論を明示する。game morphism h:K→R(S) に対し I=h[UK] と置く。y=h(k)∈I なら

θ_R(y)=θ_R(h(k))=h[θ_K(k)]⊆I

である。従ってIはoptionについて閉じた部分gameである。

同じ等号により、codomainをIへ狭めた写像 K→I もgame morphismで、基礎集合上全射である。包含 I↪R(S) も部分game射だから

K↠I↪R(S)

がgame morphismとしてのimage factorizationになる。特にhの各positionの全descendantはI内にあり、あるKのpositionの像として表せる。

4. currying：任意のfからA(G,H)への射を作る

任意のgame morphism

f:G+K→H

を取る。set map σ_f:UK→S を

σ_f(k)(g)=f(g,k)

で定め、その一意なcofree transposeを

h_f=σ_f♭:K→R(S)

とする。fのmorphism等号を (g,k) で展開すると

θ_H(f(g,k))={f(g′,k) | g′∈θ_G(g)}∪{f(g,k′) | k′∈θ_K(k)} (F)

となる。

u=h_f(k) とすればuのlabelは a_u(g)=f(g,k) で、子集合は

θ_R(u)={h_f(k′) | k′∈θ_K(k)}

である。従って(F)はuにおける(E)そのものである。Section 3のimage subgame I=h_f[UK] の各descendantもある h_f(k′) であり、同じ(F)を満たす。よってI上のevaluationはgame morphismである。Section 2の最大性から I⊆A(G,H) となる。

したがってh_fは一意に

λf:K→A(G,H)

へ因子化する。「一意に」はAからR(S)への包含が基礎集合上の包含であることによる。これがcurryingである。

5. uncurryingと二つの合成

逆にgame morphism h:K→A(G,H) に対し

uncurry(h)=ev_{G,H}∘(id_G+h):G+K→H

と定める。+のbifunctorialityとevaluationのmorphism性により、これはgame morphismである。基礎集合上では

uncurry(h)(g,k)=a_{h(k)}(g)

である。

二つの合成を別々に確認する。第一にfから始めると、λf(k) のlabelはcofree counitにより σ_f(k) である。従って

uncurry(λf)(g,k)=σ_f(k)(g)=f(g,k)

であり、uncurry(λf)=f である。

第二にhから始める。f=uncurry(h) に対応するlabel mapは

σ_f(k)(g)=a_{h(k)}(g)

である。包含を i:A(G,H)↪R(S) とすると、i∘h:K→R(S) はgame morphismで、そのcounit labelも同じσ_fである。Section 1のcofree transpose一意性により

σ_f♭=i∘h

となる。Aへの一意な像因子化を取れば λ(uncurry(h))=h である。

従って全単射

Game(G+K,H)≅Game(K,A(G,H))

を得る。よって A(G,H) がConway additionに関するinternal hom [G,H]_+ である。

6. G、K、Hの三変数自然性

射

p:G′→G, q:K′→K, r:H→H′

を取る。まずinternal hom object自体のfunctorialityを構成する。label集合の写像

Φ_{p,r}:Set(UG,UH)→Set(UG′,UH′)

Φ_{p,r}(a)=r∘a∘p

を定める。R(Φ_{p,r}) はrank再帰で

R(Φ)(T_w,a_w)=({R(Φ)(v) | v∈T_w}, Φ(a_w))

と定める。Φが非単射なら異なる子が同一化されることはあるが、定義から任意wについて

θ_{R(S′)}(R(Φ)(w))={R(Φ)(v)|v∈θ_{R(S)}(w)}=R(Φ)[θ_{R(S)}(w)]

が成り立つ。従ってR(Φ)はoption像の等号を満たすgame morphismである。

u∈A(G,H) の任意のdescendant wと g′∈UG′ に対し、pとrのexactなmorphism等号および(E)を順に使うと

θ_{H′}(r(a_w(p(g′))))

=r[θ_H(a_w(p(g′)))]

={r(a_w(p(g″))) | g″∈θ_{G′}(g′)}∪{r(a_v(p(g′))) | v∈θ_R(w)}

となる。右辺は変換後のtreeにおける(E)である。異なる子が R(Φ_{p,r}) で同一化されても、両辺は集合像なので等号は変わらない。全descendantで同じ計算が成立するため、R(Φ)は制限

A(p,r):A(G,H)→A(G′,H′)

を与える。label mapには

Φ_{id,id}=id

Φ_{p∘p′,r′∘r}=Φ_{p′,r′}∘Φ_{p,r}

が成り立つので、cofree functorialityと制限から A(-,-):Gameᵒᵖ×Game→Game はfunctorである。

次にcurryingを追う。f:G+K→H に対し

f′=r∘f∘(p+q):G′+K′→H′

と置く。そのlabel mapは各k′,g′で

σ_{f′}(k′)(g′)=r(f(p(g′),q(k′)))

である。一方、A(p,r)∘λf∘q をRへ包含した射のlabelも、Φの定義から同じ値になる。両者は同じset map UK′→Set(UG′,UH′) のcofree transposeなので、Section 1の一意性により

λ(r∘f∘(p+q))=A(p,r)∘λ(f)∘q (N)

である。

uncurrying側も基礎集合上で直接

uncurry(A(p,r)∘h∘q)(g′,k′)

=r(uncurry(h)(p(g′),q(k′)))

となる。従ってcurry/uncurry全単射はGに反変、KとHに共変であり、三変数すべてに自然である。

7. size、空端点、有限部分圏との境界

S=Set(UG,UH) は集合で、R(S)は有限S-labelled tree全体の集合、A(G,H)はその部分集合である。従って構成にlarge-objectの穴はない。

空端点も普遍性と一致する。

• UG=∅ ならSはsingletonで(E)は空虚だから A(G,H)=R(1)、すなわちterminal gameである。実際G+Kは空gameで、Hへの射は一意である。
• UG≠∅, UH=∅ ならSは空集合で R(S)=A(G,H)=∅ である。
• G,Hがともに空なら第一の場合に含まれる。

対象をfinite carrier gameだけへ制限するとR(1)は圏外になる。HoraのGameはcarrier全体の有限性ではなく、有限分岐とfinite-timeを仮定する圏である。本定理はその全圏に対するもので、finite carrier部分圏のclosednessを主張しない。

8. 既知性の限界

本reportが直接依拠する公開根拠はorigin/mainの瓶 g6c8vxである。瓶は、Conway additionのclosednessが抽象的には分かる一方、positions、moves、evaluation、curryingの具体形が未検証だと記録し、まさに本reportの最大compatible部分game式を候補として掲げている。本reportはその未完だった普遍性をSections 1–7で自己完結に閉じる。

cofree object内で構造保存条件を課してmapping objectを切り出す一般的技法には近接先行があり得る。しかし、同じrecursive GameとConway option式に対する直接の公刊先行定理はこのreportでは立証していない。negative searchは新規性の証明ではないため novelty=unsearched を維持する。既出性の最終判定は、数学的quorumとは分離して追加surveyに委ねる。

9. 解いた範囲と残る問い

本定理が与えるのはHoraのGameにおけるliteralなright adjointである。具体的には

• position：関数 UG→UH を各nodeにlabelした有限well-founded tree、
• admissibility：全descendantで(E)を満たすこと、
• move：admissible treeの子treeへ進むこと、
• evaluation：現在のlabelをgで評価すること、
• currying：k↦(g↦f(g,k)) のcofree transpose、

である。

一方、瓶が残る比較対象として挙げるplayer-switchingの意味は解いていない。impartial exact-map圏にはLeft/Rightの区別、negation、winning strategy、copycatがないため、このvertical internal homをstrategy categoryのinternal homと同一視しない。そこにはpartisan P_fin×P_fin-coalgebraとstrategyをhorizontal morphismに持つ別構造が必要である。

また、基礎集合の直積をstrictに持ち上げる任意のbifunctorに同じ最大compatible-subgame構成が通る、という一般化も本claimではない。合併でのcompatibility保存、全射imageへの降下、自然性を独立に証明してから別定理として扱う。今回の中心結果はSection 2のConway option式を直接使うため、その一般化に依存しない。

独立review

• codex: support — blocking issueなし (https://github.com/hora-algebra/kobin/blob/main/ideas/2025-10-27_internal-hom-for-conway-addition.md, https://arxiv.org/abs/2510.22886)
• claude: support — blocking issueなし (https://github.com/hora-algebra/kobin/blob/main/ideas/2025-10-27_internal-hom-for-conway-addition.md, https://arxiv.org/abs/2510.22886)

@misc{sumire:2610.00003:29:v1,
  author = {hora},
  title = {{AI evaluation report (2026-08-22): Internal hom for Conway addition}},
  year = {2026},
  note = {SUMIRE:2610.00003/29, v1},
  url = {https://sumire.aiformath.jp/p/2610.00003/n/29/v/1}
}