5 The Arithmetic Site
All the ingredients are now in place. The presheaf topos \(\widehat{\mathbb {N}^{\times }}\) provides the geometric stage. Connes–Consani identify its point classes with an adèlic quotient; the later chapter states precisely which part of that classification is currently formalized. The tropical semiring \(\bar{\mathbb {N}}\), equipped with its \(\mathbb {N}^{\times }\)-action by scaling endomorphisms, is a semiring object of \(\widehat{\mathbb {N}^{\times }}\): it plays the role of the ring of functions, recording characteristic-\(1\) algebra at every point. Their combination is the Arithmetic Site.
The Arithmetic Site is the ringed topos \((\widehat{\mathbb {N}^{\times }}, \mathcal{O})\) consisting of the presheaf topos \(\widehat{\mathbb {N}^{\times }}\) together with its structure sheaf \(\mathcal{O} = \bar{\mathbb {N}}\). Since this Lean development fixes the ambient topos, arithmeticSite is the bundled commutative-semiring-valued presheaf on \((B\mathbb {N}^{\times })^{\mathrm{op}}\); forgetting its algebraic structure gives structureSheaf.
The Arithmetic Site is a ringed topos of characteristic \(1\): its structure sheaf is a semiring with idempotent addition (\(a \oplus a = a\)), placing the entire construction in the world of tropical algebra rather than classical commutative ring theory. Connes and Consani describe it as the “algebraic geometric incarnation” of the non-commutative geometric approach to the Riemann hypothesis: the site provides a geometric framework, analogous to the function-field setting of the Weil proof, in which the relevant \(L\)-function — the Riemann zeta function — arises as a Hasse–Weil zeta function. The subsequent chapters make this precise by analysing the points of the site and the Frobenius correspondences acting on them.