在Lean中形式化Krull拓扑
Formalising the Krull Topology in Lean
摘要：
无限伽罗瓦扩张的伽罗瓦群有一个自然的拓扑，称为Krull拓扑，它有一个重要的性质是profinite。如果不首先定义克鲁尔拓扑，就不可能讨论伽罗瓦表示，也不可能讨论朗兰兹纲领。我们解释我们的形式化这个拓扑结构，我们的证明，它是profinite，在精益3定理证明。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
