A proposed internal hom for Conway addition

This note gives a proposed construction and proof for the explicit internal hom asked for in note 4. Its status remains a proof candidate; a completed human review and a claim of novelty are not asserted.

The scope is impartial recursive finite-powerset coalgebras with exact coalgebra morphisms. Player-switching, partisan strategies, and arbitrary other game-combining operations are outside the claim.

1. Games, Conway addition, and cofree games

An object $X$ of $\mathbf{Game}$ consists of a set $UX$ and an option map

$$\theta_X:UX\longrightarrow\mathcal P_{\mathrm{fin}}(UX)$$

with no infinite path. A morphism $f:X\to Y$ satisfies

$$\theta_Y(f(x))=f[\theta_X(x)].$$

Conway addition has carrier $UG\times UK$ and options

$$\theta_{G+K}(g,k) =(\theta_G(g)\times\{k\})\cup(\{g\}\times\theta_K(k)).$$

On maps it is the underlying product map, giving a bifunctor.

For a set $S$, the cofree game $R(S)$ has positions $t=(T_t,a_t)$, recursively formed from a finite set of child positions $T_t$ and a label $a_t\in S$. Its option map is $t\mapsto T_t$, and its counit sends $t$ to $a_t$. These are Definition B.13 and Proposition B.14 of Games as recursive coalgebras, v3.

A label map $\ell:UK\to S$ has a unique cofree transpose. Each position $k$ has finite rank: otherwise the finitely branching tree of paths from $k$ would have an infinite branch by König's lemma. Rank recursion therefore defines

$$\ell^\flat(k) =\bigl(\{\ell^\flat(k'):k'\in\theta_K(k)\},\ell(k)\bigr).$$

It is a game morphism with counit $\ell$. Conversely, those properties force both the label and the child set, so induction on rank proves uniqueness. The entire carrier $UK$ need not be finite.

2. The compatible subgame

Fix $G,H$, and put $S=\operatorname{Set}(UG,UH)$. A label $a_w$ is now a function $UG\to UH$.

Let $A(G,H)$ consist of positions $u$ of $R(S)$ such that every descendant $w$, including $u$, satisfies

$$\theta_H(a_w(g)) =\{a_w(g'):g'\in\theta_G(g)\} \cup\{a_v(g):v\in T_w\} \qquad(g\in UG). \tag{E}$$

Every child has the same property, so this is a subgame.

Define

$$\operatorname{ev}:G+A(G,H)\to H,\qquad \operatorname{ev}(g,u)=a_u(g).$$

The image of the Conway options is the right-hand side of (E), so evaluation is an exact coalgebra morphism.

This is the largest subgame of $R(S)$ on which label evaluation is a morphism. Indeed, for any other such subgame $B$, the morphism equation gives (E) at each position. Since $B$ contains its descendants, $B\subseteq A(G,H)$.

3. Images and currying

The image of a game morphism $h:K\to R(S)$ is a subgame, since

$$\theta_R(h(k))=h[\theta_K(k)]\subseteq h[UK].$$

Restricting the codomain gives a surjective game morphism onto that image.

Take $f:G+K\to H$, and let $h_f:K\to R(S)$ be the cofree transpose of

$$\ell_f(k)(g)=f(g,k).$$

Its labels and children satisfy

$$a_{h_f(k)}(g)=f(g,k),\qquad T_{h_f(k)}=\{h_f(k'):k'\in\theta_K(k)\}.$$

The morphism equation for $f$ is

$$\theta_H(f(g,k)) =\{f(g',k):g'\in\theta_G(g)\} \cup\{f(g,k'):k'\in\theta_K(k)\}.$$

This is (E) at $h_f(k)$. Every descendant of an image position is again in the image, so (E) holds throughout the image subgame. Therefore $h_f$ factors uniquely as

$$\lambda f:K\to A(G,H).$$

4. Uncurrying and the inverse equations

For $h:K\to A(G,H)$, define

$$\operatorname{uncurry}(h) =\operatorname{ev}\circ(\mathrm{id}_G+h).$$

This is a game morphism, with value $a_{h(k)}(g)$ at $(g,k)$.

Starting with $f$, the label of $\lambda f(k)$ is $g\mapsto f(g,k)$, so

$$\operatorname{uncurry}(\lambda f)=f.$$

Starting with $h$, its composite into $R(S)$ has exactly the labels used for the cofree transpose of $\operatorname{uncurry}(h)$. Uniqueness of that transpose gives

$$\lambda(\operatorname{uncurry}(h))=h.$$

The proposed construction thus gives

$$\mathbf{Game}(G+K,H)\cong\mathbf{Game}(K,A(G,H)).$$

5. Naturality

Take $p:G'\to G$, $q:K'\to K$, and $r:H\to H'$. The label map

$$\Phi_{p,r}(a)=r\circ a\circ p$$

induces $R(\Phi_{p,r})$ by recursively changing labels and taking images of child sets. This is an exact coalgebra map, including when different children acquire the same image.

For a compatible position $w$, exactness of $p,r$ gives

$$\begin{aligned} \theta_{H'}(r(a_w(p(g')))) &=r[\theta_H(a_w(p(g')))]\\ &=\{r(a_w(p(g''))):g''\in\theta_{G'}(g')\}\\ &\quad\cup\{r(a_v(p(g'))):v\in T_w\}. \end{aligned}$$

This is (E) for the transformed position. Every descendant of the transformed position is the image of a descendant, so the same calculation applies throughout. The map therefore restricts to

$$A(p,r):A(G,H)\to A(G',H').$$

Identities and composition follow from the label maps and the functoriality of $R$.

Both sides of

$$\lambda\bigl(r\circ f\circ(p+q)\bigr) =A(p,r)\circ\lambda(f)\circ q$$

have label $g'\mapsto r(f(p(g'),q(k')))$ at $k'$. Uniqueness of the cofree transpose proves the equation. The corresponding equation for uncurrying follows directly by evaluating labels.

6. Size and empty games

The labels form a set $S$; the finite recursively labelled positions form a set $R(S)$; and $A(G,H)$ is a subset.

If $UG=\varnothing$, then $S$ is a singleton and (E) is vacuous, so $A(G,H)=R(1)$, the terminal game. If $UG\ne\varnothing$ and $UH=\varnothing$, then $S=\varnothing$ and $A(G,H)=\varnothing$. These cases agree with the proposed adjunction.

The full category is essential: $R(1)$ has infinite carrier. This does not assert closedness of the subcategory of finite-carrier games.

7. What remains

The candidate describes positions, moves, evaluation, currying, and naturality. It does not identify these positions with legal playing strategies or explain player-switching. Nor does it establish the partisan analogue or a construction for arbitrary products lifted to games.

The next tasks are human review of the proof in the stated category, explicit small examples, a game-theoretic interpretation, and comparison with prior mapping-object constructions. Failure to locate an identical theorem would not establish novelty.

@misc{sumire:2610.00003:29:v4,
  author = {hora},
  title = {{A proposed internal hom for Conway addition}},
  year = {2026},
  note = {SUMIRE:2610.00003/29, v4},
  url = {https://sumire.aiformath.jp/p/2610.00003/n/29/v/4}
}