3 The presheaf topos \(\widehat{\mathbb {N}^{\times }}\)
The topos underlying the Arithmetic Site is the simplest kind: a presheaf topos. Its objects are sets equipped with a left \(\mathbb {N}^{\times }\)-action by arbitrary functions — not necessarily bijections, since \(\mathbb {N}^{\times }\) is a monoid rather than a group — and its morphisms are \(\mathbb {N}^{\times }\)-equivariant maps between them. The multiplicative structure of \(\mathbb {N}^{\times }\) is entirely encoded in the composition of these actions: if \(n\) and \(m\) act on a set \(X\), then \(nm\) acts as the composite \(x \mapsto n \cdot (m \cdot x)\).
Connes and Consani note that \(\widehat{\mathbb {N}^{\times }} \simeq \mathrm{Sh}(\mathbb {N}^{\times }, J)\), where \(J\) is the chaotic topology on \(\mathbb {N}^{\times }\) — the topology in which every presheaf is already a sheaf. This means there are no genuine gluing conditions to check: the topos is simply the presheaf category, with no further data. The covering families arising from factorizations of integers, foreshadowed in Chapter 1, reflect a finer site structure that one can put on \(\mathbb {N}^{\times }\); the Arithmetic Site itself uses the coarser chaotic topology, where that combinatorial structure is not needed.
The presheaf topos \(\widehat{\mathbb {N}^{\times }}\) is the category of functors \(B{\mathbb {N}^{\times }}^{\mathrm{op}} \to \mathbf{Set}\), i.e. the category of sets equipped with a left \(\mathbb {N}^{\times }\)-action (using commutativity to exchange left and right actions). In Lean this is represented literally as the functor category BNplusop \(\mathbin {\leadsto }\) Type.
\(\widehat{\mathbb {N}^{\times }}\) has all small limits.
This is the pointwise limit construction for a Type-valued functor category, supplied by Mathlib’s HasLimits instance.
\(\widehat{\mathbb {N}^{\times }}\) has all small colimits.
Colimits in a Type-valued functor category are computed pointwise.
\(\widehat{\mathbb {N}^{\times }}\) is cartesian closed.
This is Mathlib’s closed monoidal structure on a presheaf category.
\(\widehat{\mathbb {N}^{\times }}\) has a subobject classifier.
Mathlib constructs the subobject classifier for presheaves. Together with finite limits and cartesian closure, this records the elementary topos structure in Lean; the standard general theorem says moreover that this presheaf category is a Grothendieck topos.
The points of \(\widehat{\mathbb {N}^{\times }}\) — geometric morphisms from \(\mathbf{Set}\) to \(\widehat{\mathbb {N}^{\times }}\) — are the deep link to number theory. Connes and Consani prove (Theorem 2.2 of their 2014 paper) that the category of points of \(\widehat{\mathbb {N}^{\times }}\) is canonically equivalent to the category of totally ordered groups isomorphic to non-trivial subgroups of \((\mathbb {Q}, \mathbb {Q}_+)\). The space of isomorphism classes of such points is canonically isomorphic to the double quotient
where \(\mathbb {A}^{f}\) is the ring of finite adèles of \(\mathbb {Q}\) and \(\hat{\mathbb {Z}}^* = \hat{\mathbb {Z}}^\times \) is the group of units of the profinite completion of \(\mathbb {Z}\). This quotient is a piece of the adèle class space of \(\mathbb {Q}\), the same space that appears in Connes’ noncommutative-geometric approach to the Riemann hypothesis. The structure sheaf \(\mathcal{O} = \bar{\mathbb {N}}\) then equips this space with characteristic-\(1\) geometry, whose Hasse–Weil zeta function recovers the Riemann zeta function.