6 Points of the topos
In topos theory a point of a topos \(\mathcal{E}\) generalises the notion of a point of a topological space: it is a geometric morphism \(p : \mathbf{Set} \to \mathcal{E}\), pulling back each sheaf to its stalk. For a presheaf topos \(\widehat{C}\), points correspond to flat functors \(C \to \mathbf{Set}\). For \(\widehat{\mathbb {N}^{\times }} = \widehat{B\mathbb {N}^{\times }}\) this means a point is represented by a flat \(\mathbb {N}^{\times }\)-action. The classification of these actions is a theorem of Connes–Consani. The present Lean development formalizes a flatness predicate and constructs the finite adèlic quotient occurring on the other side of that theorem; it does not yet formalize the classification equivalence itself.
A point of a topos \(\mathcal{E}\) is a geometric morphism \(p : \mathbf{Set} \to \mathcal{E}\), i.e. an adjoint pair \(p^* \dashv p_*\) where \(p^*\) is left exact.
Let \(X\) carry an action of \(\mathbb {N}^{\times }\). In the Lean development the proposition \(X\) is a flat \(\mathbb {N}^{\times }\)-action means that the category of elements of the associated type-valued action functor is cofiltered. This is the category-of-elements formulation of flatness used for the points of the presheaf topos.
A covariant \(\mathbb {N}^{\times }\)-action satisfies the elementary flatness axioms when its underlying set is nonempty, every two elements have a common predecessor under two positive-integer actions, and the action is free. Explicitly, the latter two conditions are
For an \(\mathbb {N}^{\times }\)-action, the elementary axioms are equivalent to cofilteredness of its category of elements, and hence to the flatness predicate used for points of the Arithmetic Site.
Nonemptiness and the common-predecessor axiom give the object cones in the definition of a cofiltered category. Freeness equalizes parallel arrows. Conversely, a cofiltered cone gives common predecessors, while a cofiltered equalizer and right cancellation in \(\mathbb {N}^{\times }\) imply freeness. Both directions are formalized directly in Lean.
The regular multiplication action of \(\mathbb {N}^{\times }\) on itself is flat.
The element \(1\) witnesses nonemptiness, the greatest common divisor of two positive integers supplies a common predecessor, and cancellation proves freeness.
There is an important positive-part convention in the classification. If \(H\) is a non-trivial ordered subgroup of \((\mathbb {Q},\mathbb {Q}_+)\), the associated flat action is on \(H_{{\gt}0}=H\cap \mathbb {Q}_{{\gt}0}\), with \(n\cdot h=nh\); it is not the action on the whole additive group \(H\). In particular, adjoining \(0\) to the action set would destroy the cancellation condition in the flatness axioms: for \(n\ne m\) one would have \(n\cdot 0=m\cdot 0\).
6.1 The finite adèlic side
The type \(\mathbb {A}^{f}\) of finite adèles of \(\mathbb {Q}\) is the restricted product of the finite completions of \(\mathbb {Q}\) with respect to their valuation subrings. In Lean this is Mathlib’s finite adèle ring for the Dedekind domain \(\mathbb {Z}\) and its fraction field \(\mathbb {Q}\).
The profinite integers \(\hat{\mathbb {Z}}\subset \mathbb {A}^{f}\) form the subring of finite adèles that are integral at every finite place. Its unit group is denoted \(\hat{\mathbb {Z}}^*\).
The finite adèle class space used here is the orbit quotient
Concretely, Lean combines the commuting actions of positive rational units and profinite-integer units into an action of their product and takes its orbit-relation quotient. At this stage this is a quotient type; no quotient topology is asserted.
Two finite adèles \(a,b\) have the same image in the formalized orbit quotient if and only if there is an element \(g\) of the combined scaling group such that \(g\cdot b=a\).
For \(a\in \mathbb {A}^{f}\), define the additive subgroup
where \(q\) is embedded diagonally in the finite adèles. This subgroup, including its membership criterion at every finite place, is constructed in Lean.
If \(u\in \hat{\mathbb {Z}}^*\) and \(a\in \mathbb {A}^{f}\), then multiplication by \(u\) does not change the associated rational subgroup:
If \(r\in \mathbb {Q}^{\times }_{+}\), \(a\in \mathbb {A}^{f}\), and \(x\in \mathbb {Q}\), then
Together with Lemma 6.12, this is the formalized orbit-invariance calculation needed on the adèlic side of the published point classification.
The space of isomorphism classes of points of \(\widehat{\mathbb {N}^{\times }}\) is canonically isomorphic to the double quotient
a piece of the adèle class space of \(\mathbb {Q}\). More precisely, the category of points of \(\widehat{\mathbb {N}^{\times }}\) is equivalent to the category of totally ordered groups isomorphic to non-trivial subgroups of \((\mathbb {Q}, \mathbb {Q}_+)\), with injective order-preserving homomorphisms as morphisms; the flat action associated to \(H\) uses \(H_{{\gt}0}\) as above.
This is the published classification theorem of Connes–Consani (Theorem 2.2 in the 2014 note, and Theorem 2.1 with Proposition 2.5 in the full treatment). Their proof extracts a rank-one ordered group from a filtering action and reconstructs the action from its strictly positive part. The adèlic parametrization then sends \(a\) to \(H_a\) and identifies isomorphic ordered groups with the indicated double orbits.
Formalization status. Lean currently contains the flatness predicate, its elementary action-axiom characterization, the restricted-product adèle ring, \(\hat{\mathbb {Z}}\), the orbit quotient, and \(a\mapsto H_a\). It does not yet contain the functors in both directions or a proof that they induce the stated categorical equivalence and bijection on isomorphism classes. Consequently this published theorem intentionally has no Lean declaration link.