Formalizing the ring of adèles and some applications in Lean

Abstract: I will present a formalization of the ring of adèles and group of idèles of a global field in the Lean 3 theorem prover. Lean is an interactive theorem prover with an ever-growing mathematics library. I will give a quick introduction to Lean and explain how these definitions were formalized, with a focus on the kind of decisions one has to make during the formalization process.

Besides the definition of the adèles, we will discuss the formalization of applications including the statement of the main theorem of global class field theory and a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its idèle class group.

number theory

Audience: researchers in the topic

London number theory seminar

Series comments: For reminders, join the (very low traffic) mailing list at mailman.ic.ac.uk/mailman/listinfo/london-number-theory-seminar

For a record of talks predating this website see: wwwf.imperial.ac.uk/~buzzard/LNTS/numbtheo_past.html