Formalizing the Ring of Adèles of a Global Field

Autor:	de Frutos-Fernández, María Inés
Jazyk:	angličtina
Rok vydání:	2022
Předmět:	FOS: Computer and information sciences class field theory algebraic number theory formal math mathlib FOS: Mathematics Lean Number Theory (math.NT) Theory of computation → Type theory Theory of computation → Logic and verification Logic in Computer Science (cs.LO)
DOI:	10.4230/lipics.itp.2022.14
Popis:	The ring of adèles of a global field and its group of units, the group of idèles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalized adic valuations on Dedekind domains. We present some 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. 15 pages
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8ebc46e189500e2998d1fa179f67ba06 Zobrazit plný text záznamu