Exact completion of games and the Leibniz obstruction

Current result and proof status

The category of games is not itself a topos; see the original question. The proposed replacement is its exact completion, presented as sheaves on finite games. This note records that construction and a concrete obstruction to its proposed differential structure: the Leibniz law below gives 6 maps on one side and 2 on the other.

The exact-completion and Day-tensor arguments are in the linked manuscripts. The finite map counts below are explicit; their interpretation as a sheaf counterexample uses the embedding and closed-tensor results. The open questions below remain separate from those results.

• Regularity, the site, and the noneffective relation (Japanese).
• Exact completion as a sheaf topos (Japanese).
• Properties and points of the topos (Japanese).
• Conway addition and ex/reg completion (Japanese).
• The Day-tensor descent proof (Japanese); this supplies the corrected proof required by the preceding manuscript.
• The species comparison and Leibniz counterexample (Japanese).

Definitions and the exact-completion construction

Let $\mathrm{Games}=\operatorname{RecCoalg}(P_f)$, with maps satisfying
$\operatorname{succ}(f(x))=f[\operatorname{succ}(x)]$.
Let $\mathrm{Games}_{\mathrm{fin}}$ be the full subcategory on finite carriers, and let $J_{\mathrm{coh}}$ be generated by finite jointly surjective families. Put

Write $\mathrm{Star}_m$ for a root with $m$ terminal children.

The construction asserts that Games is regular, with epimorphisms equal to surjections and regular epimorphisms, stable under pullback. It is infinitary extensive but not exact: $\Delta\cup\Gamma_\sigma\subseteq\mathrm{Star}_2\times\mathrm{Star}_2$, with $\sigma$ swapping the two terminal children, is a six-element noneffective equivalence relation. Its ex/reg completion is

The proof uses that every subobject of $N(X)$ comes from a subgame and that $N$ preserves coproducts, surjections, and filtered colimits. The subobject classifier is $\Omega_{\mathcal E}=N(\Omega_{\mathrm{Games}})$, described using truth-closed hereditarily finite sets.

An exact-completion object $(X,R)$ retains a game together with witnesses of its equivalence relation. A quotient is already represented in Games when its relation is a kernel pair. In particular,
$Q=N(\mathrm{Star}_2)/(\Delta\cup\Gamma_\sigma)$
is outside the image of $N$; it has $N(\mathrm{Star}_1)$ as a quotient, not as a claimed retract.

Properties asserted by the construction

• The terminal object is $N(V)$, where $V$ is the game of all hereditarily finite sets. It is not quasi-compact, so $\mathcal E$ is not coherent. The subterminal objects $N(V_{<n})$ give an open cover by coherent topoi
  $\mathcal E_n\simeq\operatorname{Sh}((\mathrm{Games}_{\mathrm{fin}})_{<n},J_{\mathrm{coh}})$.
  Thus $\mathcal E$ has enough points. Its proposed geometric theory combines the coherent theories at each finite height with the infinitary assertion that every position has some finite height.
• $\mathcal E_1\simeq\mathrm{Set}$ is a dense open point and $\operatorname{Sh}_{\neg\neg}(\mathcal E)\simeq\mathrm{Set}$. The point is given by the terminal-position functor. The one-position no-move game is projective; so is every finite discrete no-move game. No uniqueness or classification of connected projectives is claimed here.
• $\mathcal E$ is not Boolean: the terminal-position subgame of $\mathrm{Star}_1$ has no complement. It is not localic: $N(\mathrm{Star}_2)$ is not covered by subterminal objects. Its proposed localic reflection is the presheaf topos on $(V_\omega,\in^+)$.
• A proposed family of points, indexed by nonempty perfect Stone spaces $S$, is
  $F_S(X)=\{(x,e):\operatorname{succ}(x)\text{ consists of terminal positions},\ e:S\twoheadrightarrow\operatorname{succ}(x)\text{ continuous}\}$.
  This is not a classification of all points.

Conway addition and the tensor

Conway addition $+$ is not left exact: the comparison involving
$(\mathrm{Star}_2\times_{\mathrm{Star}_1}\mathrm{Star}_2)+\mathrm{Star}_1$
and
$(\mathrm{Star}_2+\mathrm{Star}_1)\times_{\mathrm{Star}_1+\mathrm{Star}_1}(\mathrm{Star}_2+\mathrm{Star}_1)$
has respectively $7$ and $7\cdot127$ roots. Therefore its descent to the completion cannot simply use the 2-functoriality of ex/reg completion on left-exact functors.

The proposed alternative is the sheafified Day tensor $\oplus$ on $\mathcal E$. It is symmetric monoidal closed, with $N$ strong monoidal and
$N(A)\oplus N(B)\cong N(A+B)$.
For finite $A,B$, their presheaf Day tensor is already the representable sheaf $N(A+B)$. The closed structure uses a separate descent argument proving that $F(-+B)$ is a sheaf; cover preservation alone does not suffice. No claim is made here that arbitrary presheaf Day convolution is already a sheaf. See Reflected Day convolution for the distinction between convolution and its reflection.

Species with Cauchy product and nominal sets with separated product suggest comparisons through Day convolution on finite objects; those analogies do not by themselves identify the game tensor or its differential structure.

The proposed Leibniz law fails for this operator

The symbol $\sqcup$ denotes coproduct. Use the sheafified Day tensor $\oplus$ described above and set

Here the tensor unit is $I=N(\{*\})$, where $\{*\}$ is the one-position game with no moves (the unit for Conway addition); $\mathrm{Star}_1$ is not the tensor unit.

The evaluation formula follows from the internal-hom adjunction and Yoneda: for a finite game $A$,

This uses the stated closed Day tensor and its tensor formula on representables.

Take $F=G=N(\mathrm{Star}_1)$. A coalgebra morphism preserves height. Thus
$\mathrm{Games}(A+\mathrm{Star}_1,\mathrm{Star}_1)$ has one element when every position of $A$ is terminal, and is empty otherwise. This is exactly $N(\{*\})(A)$, so $DF=DG=I$. Using the stated strong monoidality and coproduct preservation of $N$, the proposed law

would therefore identify, at $A=\mathrm{Star}_2$,

The first set has $6$ elements. Its source has one height-two root, three height-one positions, and two terminal positions; the target has one height-two root, two height-one positions, and one terminal position. Height preservation fixes the root and terminal images. Each of the three height-one positions can map to either target position, and the coalgebra equation
$\operatorname{succ}(f(x))=f[\operatorname{succ}(x)]$ at the root requires both images to occur. There are $2^3-2=6$ such maps.

The second set has $2$ elements. The root of $\mathrm{Star}_2$ chooses one of the two coproduct components; both terminal children must then map to that component's terminal position. Hence the two evaluated sheaves cannot be isomorphic.

This refutes the displayed Leibniz isomorphism for this particular $D$ and $\oplus$. It does not refute the successor formula defining Conway addition, or every possible differential structure on games. The remaining question is a replacement rule accounting for the four additional maps in this example. The finite map counts can be checked directly from the coalgebra equation; the identification with these sheaf values still uses the Day-tensor and embedding properties stated above.

Remaining questions

1. Find a replacement for the failed Leibniz law, accounting for the four additional maps in this example. Compare Differential structures of games and the differential 2-rig axioms.
2. Classify the points of $\mathcal E$. Do Stone-game constructions exhaust them? Is $\mathcal E$ a presheaf topos? The expectation recorded here is negative, not a proof.
3. Determine when the tensor internal hom$$[NX,NY]_{\oplus}(A)=\int_B\operatorname{Set}(\mathrm{Games}(B,X),\mathrm{Games}(A+B,Y))$$lies in the image of $N$; compare Internal hom for Conway addition.
4. Is there an ex/reg analogue of Menni's ex/lex criterion using weak dependent products and a generic proof? The proposed sufficient conditions for a Grothendieck-topos completion are regularity, infinitary extensivity, and a small generating family. The earlier comparison with Worrell, Corollary 5.5.7, still requires its precise hypotheses to be matched. The remembered realizability comparison $\mathrm{Eff}\simeq\mathrm{Asm}_{\mathrm{ex/reg}}$ is not used as evidence here.

The distinction between ex/reg and ex/lex matters: ex/reg completion is idempotent on exact categories, whereas ex/lex completion is not generally idempotent. The existing proof manuscripts and their hypothesis checks are needed before the general criterion above can be reused as a theorem.