7 The Frobenius correspondences
The Frobenius correspondences are the analogue, in characteristic \(1\), of the Frobenius endomorphisms of a variety over a finite field. They do not act on the Arithmetic Site itself — that would require endomorphisms of the ringed topos \((\widehat{\mathbb {N}^{\times }}, \mathcal{O})\) — but are constructed on its square. The algebra formalized so far is the raw tensor semiring \(\bar{\mathbb {N}}\otimes _{\mathbb {B}}\bar{\mathbb {N}}\), where \(\mathbb {B}=(\{ 0,1\} ,\max ,\times )\) is the Boolean semifield. There are two different levels below:
tensor-algebra endomorphisms and rational evaluation maps, which are now implemented and proved in Lean; and
reduced correspondences, their real parameter, their composition, and the exceptional tangential deformation, which remain published mathematics not yet represented by Lean structures.
7.1 The formalized tensor-algebra layer
The Boolean semifield \(\mathbb {B}\) is realized in Lean as the bottom subsemiring of the idempotent semiring \(\bar{\mathbb {N}}\). Its elements are the additive and multiplicative identities of \(\bar{\mathbb {N}}\).
The raw structure semiring on the square is Mathlib’s semiring tensor product
Each scaling semiring endomorphism \(\varphi _n\) fixes the embedded Boolean semifield, and hence defines a \(\mathbb {B}\)-algebra endomorphism of \(\bar{\mathbb {N}}\).
For \(n,m\in \mathbb {N}^{\times }\), functoriality of the tensor product defines
On a pure tensor,
Multiplication in \(\bar{\mathbb {N}}\) induces the \(\mathbb {B}\)-algebra homomorphism
On pure tensors the product map satisfies \(\mu (x\otimes y)=xy\).
For \(n,m\in \mathbb {N}^{\times }\), the rational Frobenius evaluation formalized in Lean is the algebra homomorphism
The Lean identifier retains the historical name frobeniusCorrespondence, but its type correctly records that it is an evaluation out of the tensor product, not an endomorphism of \(\bar{\mathbb {N}}\) and not a reduced-correspondence triple. Lean does not impose coprimality on \(n,m\); lowest terms matter only when the ratio \(n/m\) is used as a normalized rational parameter.
The rational evaluation has the expected pure-tensor formula
The tensor Frobenius endomorphisms compose multiplicatively in each index:
The two algebra homomorphisms are equal by tensor-product extensionality. On the left and right generating factors the claim reduces respectively to \(\varphi _n\circ \varphi _k=\varphi _{nk}\) and \(\varphi _m\circ \varphi _l=\varphi _{ml}\), both already proved for the scaling endomorphisms.
The theorem above is a theorem about an action on the raw tensor semiring. The maps \(E_{n,m}\) have source \(\bar{\mathbb {N}}\otimes _{\mathbb {B}}\bar{\mathbb {N}}\) and target \(\bar{\mathbb {N}}\), so an expression such as \(E_{n,m}\circ E_{k,l}\) is not even the relevant typed composition. It must not be confused with composition of the reduced correspondences described next.
7.2 Published reduced correspondences
For every positive real parameter \(\lambda \in \mathbb {R}_{+}^{\times }\), Connes and Consani construct a semiring homomorphism
with a multiplicatively cancellative range semiring \(R(\lambda )\). Thus the parameter in this formula is real, not merely rational. When \(\lambda =n/m\in \mathbb {Q}^{\times }_{+}\) is in lowest terms, the integral-exponent map \(E_{n,m}\) above is the raw rational evaluation underlying the construction; passing to the appropriate range and reduction is additional structure.
A reduced correspondence in the sense of Connes–Consani is a triple \((R,\ell ,r)\), where \(R\) is a multiplicatively cancellative semiring and \(\ell ,r\) are semiring maps from the one-sided tropical semiring to \(R\), each with zero kernel, whose two images generate \(R\). Composition is defined from a tensor product over the middle semiring followed by multiplicatively cancellative reduction.
This structure, its reduction operation, and its composition are not yet defined in Lean in this project.
For \(\lambda \in \mathbb {R}_{+}^{\times }\), the published Frobenius correspondence is
obtained from \(F(\lambda ,q)\) and the two inclusions of the tensor factors. On geometric points over \(\mathbb {R}_{+}^{\max }\) it corresponds to the positive-real scaling action on the associated adèle-class description. This geometric correspondence is not the ordinary \(\mathbb {N}^{\times }\)-scaling action on the global semiring, although that action is one algebraic ingredient in its rational models.
Let \(\lambda ,\lambda '\in \mathbb {R}_{+}^{\times }\). Composition of the published reduced Frobenius correspondences gives
when \(\lambda ,\lambda '\) are both rational, and also whenever \(\lambda \lambda '\) is irrational. If \(\lambda \) and \(\lambda '\) are both irrational but \(\lambda \lambda '\) is rational, the composite is instead the canonical tangential deformation of \(\Psi (\lambda \lambda ')\).
This is Theorem 4.3 of the 2014 Connes–Consani note and Theorem 7.7 of the full paper. The proof computes the multiplicatively cancellative reduction of the tensor product of the range semirings \(R(\lambda )\) and \(R(\lambda ')\). Flexibility present for irrational slopes survives the exceptional rational product and produces the tangential deformation.
Formalization status. Neither this reduction argument nor the irrational and tangential constructions are formalized. Accordingly, this theorem has no Lean declaration link; the proved theorem 7.10 is only its raw tensor-algebra precursor.