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

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

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

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

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

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

Define

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

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

Its labels and children satisfy

The morphism equation for $f$ is

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

4. Uncurrying and the inverse equations

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

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

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

The proposed construction thus gives

5. Naturality

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

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

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

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

Both sides of

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.