# Formalising the Krull Topology in Lean

Preprint · Sebastian Monnet

- Archive id: arxiv:2207.09486
- Published: 2022-07-19
- arXiv: https://arxiv.org/abs/2207.09486
- Source URL: https://arxiv.org/abs/2207.09486
- PDF: https://arxiv.org/pdf/2207.09486
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.