instTopologicalSpaceAbsoluteGaloisGroup

English

The absolute Galois group carries a natural topology, specifically the Krull topology coming from the algebraic closure.

Русский

Абсолютная Галуа-группа оснащена естественной топологией, в частности топологией Крюля, полученной из алгебраического замыкания.

LaTeX

$$$$\text{instTopologicalSpaceAbsoluteGaloisGroup: }\text{TopologicalSpace}(\mathrm{Field.absoluteGaloisGroup}\,K)$$$$

Lean4

/-- `absoluteGaloisGroup` is a topological space with the Krull topology. -/
noncomputable instance : TopologicalSpace (G_K K) :=
  krullTopology K (AlgebraicClosure K)

Похожие утверждения