Formalising the Krull Topology in Lean
Logic in Computer Science
2022-09-13 v2 Number Theory
Abstract
The Galois group of an infinite Galois extension has a natural topology, called the Krull topology, which has the important property of being profinite. It is impossible to talk about Galois representations, and hence the Langlands Program, without first defining the Krull topology. We explain our formalisation of this topology, and our proof that it is profinite, in the Lean 3 theorem prover.
Cite
@article{arxiv.2207.09486,
title = {Formalising the Krull Topology in Lean},
author = {Sebastian Monnet},
journal= {arXiv preprint arXiv:2207.09486},
year = {2022}
}
Comments
Minor corrections