2 The tropical semiring \(\bar{\mathbb {N}}\)
The tropical semiring \(\bar{\mathbb {N}}\) is the second fundamental ingredient of the Arithmetic Site. It plays the role of the structure sheaf: as Connes and Consani put it, \(\bar{\mathbb {N}}\) is the semiring on which \(\mathbb {N}^{\times }\) acts by multiplication, and it is this action that makes \(\bar{\mathbb {N}}\) into a sheaf of semirings over the topos \(\widehat{B\mathbb {N}^{\times }}\). The arithmetic of \(\bar{\mathbb {N}}\) is characteristic-\(1\) arithmetic — addition is idempotent — which is the tropical, or min-plus, shadow of ordinary arithmetic. Connes and Consani define \(\bar{\mathbb {N}}\) explicitly as \((\mathbb {N} \cup \{ \infty \} , \inf , +)\), confirming the min-plus convention: addition is \(\min \), with \(+\infty \) as the additive identity. When elements of \(\bar{\mathbb {N}}\) are written as exponents \(q^x\) for \(q \in (0,1)\), the addition becomes \(\max \) on values (since smaller exponent means larger value), which is why the stalks in the paper appear in max-plus form as \([0,1]_{\max }\) and \(\mathbb {R}_{\max }\).
The tropical semiring \(\bar{\mathbb {N}}\) is the set \(\mathbb {N} \cup \{ +\infty \} \) equipped with:
Tropical addition: \(a \oplus b := \min (a, b)\), with identity element \(+\infty \).
Tropical multiplication: \(a \odot b := a + b\) (ordinary addition), with identity element \(0\).
In Lean, \(\bar{\mathbb {N}}\) is represented as Tropical (WithTop \(\mathbb {N}\)), via the abbreviation NBar. The zero element is trop \(\top \) (i.e. \(+\infty \)) and the multiplicative identity is trop 0.
\(\bar{\mathbb {N}}\) is a commutative semiring.
This is Mathlib’s canonical CommSemiring instance for the Tropical type over WithTop \(\mathbb {N}\).
Tropical addition on \(\bar{\mathbb {N}}\) is idempotent: \(a \oplus a = a\) for all \(a \in \bar{\mathbb {N}}\).
\(a \oplus a = \min (a,a) = a\). In Lean this follows from Tropical.add_eq_left.
Idempotency of addition — equivalently, the identity \(1 \oplus 1 = 1\) — is the defining feature of characteristic \(1\) arithmetic. It is what places \(\bar{\mathbb {N}}\) in the same conceptual family as finite fields \(\mathbb {F}_p\) (characteristic \(p\)), with \(\min \) playing the role that \(+\bmod p\) plays there. The scaling endomorphisms defined below are the characteristic-\(1\) analogue of the Frobenius endomorphism \(x \mapsto x^p\) of \(\mathbb {F}_p\).
For each \(n \in \mathbb {N}^{\times }\), the scaling endomorphism \(\varphi _n : \bar{\mathbb {N}}\to \bar{\mathbb {N}}\) is defined by
where \(nx\) denotes ordinary multiplication in \(\mathbb {N}\). Equivalently, \(\varphi _n(x) = x^{\odot n}\), the \(n\)-fold tropical product of \(x\) with itself. In Lean, \(\varphi _n\) is defined as a semiring endomorphism NBar ->+* NBar via scalingEndomorphism.
For each \(n \in \mathbb {N}^{\times }\), the map \(\varphi _n\) is a semiring endomorphism of \(\bar{\mathbb {N}}\): it preserves both operations and both identities.
Preservation of \(+\infty \) and of tropical multiplication are immediate. Preservation of tropical addition uses \(n \cdot \min (a,b) = \min (na,nb)\) for \(n {\gt} 0\), which holds because scaling by \(n\) is order-preserving on \(\mathbb {N} \cup \{ +\infty \} \). In Lean this is the map_add’ field of scalingEndomorphism, proved via monotonicity of nsmul and a case split on le_total.
The scaling endomorphisms compose multiplicatively:
for all \(m, n \in \mathbb {N}^{\times }\). In particular, the map \(n \mapsto \varphi _n\) is a monoid homomorphism from \((\mathbb {N}^{\times }, \times )\) into the semiring endomorphism monoid \(\mathrm{End}_{\mathrm{Semiring}}(\bar{\mathbb {N}})\).
\((\varphi _m \circ \varphi _n)(x) = m(nx) = (mn)x = \varphi _{mn}(x)\). In Lean this is scalingEndomorphism_comp, proved via pow_mul.
If \(n{\gt}1\), the fixed points of \(\varphi _n\) on \(\bar{\mathbb {N}}\) are exactly the tropical zero \(+\infty \) and tropical one \(0\).
For a finite exponent \(x\), the equation \(nx=x\) with \(n{\gt}1\) forces \(x=0\); the point \(+\infty \) is also fixed. Lean proves this by splitting WithTop \(\mathbb N\) into its finite and top cases.
The Frobenius correspondences \(\Psi (\lambda )\), parametrised by \(\lambda \in \mathbb {Q}^{\times }_{+}\), are a more refined object: they live in the square \(\widehat{B{\mathbb {N}^{\times }}^2}\) of the Arithmetic Site and are defined via the action of \(\mathbb {N}^{\times }\times \mathbb {N}^{\times }\) on \(\bar{\mathbb {N}}\otimes _{\mathbb {B}} \bar{\mathbb {N}}\). They are introduced in Chapter 7.