It dawned on me that we are really close to being able to define the adeles of a number field in Lean, at least as an abstract ring. We don't have polynomials (edit: yes we do) or number fields, so it seems like we are a million miles away, but we now have enough abstract commutative algebra to make everything else very simple. Here is a roadmap.

1) Define the polynomial ring R[X] in one variable X over a commutative ring R (perhaps as functions f from nat to R for which there exists some bound B=B(f) such that f(n)=0 for n>B, or perhaps as some inductive type), and prove it's a commutative ring. Define the evaluate-at-r map (r in R) from R[X] to R (induction).

Edit: this is already in Lean e.g. import data.finsupp

check finsupp.to_comm_ring

2) Define a number field K to be a field which is abstractly isomorphic (as a ring) to the quotient ring Q[X]/M for M some maximal ideal of Q[X] (Q the rationals) (the isomorphism is not strictly speaking part of the data). Define i : Q -> K to be the canonical map (composition of functions) (this is independent of the choice of isomorphism).

3) Define the algebraic integers of a number field K to be the elements x in K such that there exists some monic polynomial f(X) in Z[X] with f(x)=0.

4) Prove that the algebraic integers form a ring. The most natural proof involves deducing it from some more abstract and general facts about finitely-generated modules over a Noetherian ring, namely that if M is such a module then M satisfies the ascending chain condition for submodules, and that any submodule of M is also finitely-generated. The point is that x in K is an algebraic integer iff the subring of K generated over Z by x is finitely-generated as a Z-module.

5) Define the completion of a commutative ring R at an ideal J to be the projective limit of R/J^n, n>=0.

Edit: Kenny Lau has done this.

6) Now define the finite adeles of K to be a subring of the following product of rings: the product is over the set of maximal ideals of R, the algebraic integers of K, and the term in the product corresponding to a maximal ideal M is the field of fractions K_M of the M-adic completion R_M of R. It is not true that completing an arbitrary integral domain at a prime ideal will give you an integral domain (the fact that this fails is not obvious ring-theoretically but it is obvious if you think about rings geometrically as affine schemes), however it's true in this case. Now R_M is a subring of K_M and an element of this product is a finite adele iff its component at M is in R_M for all but finitely many M.

7) Define the infinite adeles of K=Q[X]/M to be R[X]/M. It's also a ring.

8) Finally, define the adeles of K to be the product of the finite and the infinite adeles of K.

leanprover-community / mathlib3

Definition of the ring of adeles of a number field #40

check finsupp.to_comm_ring