instCompactSpaceAlgEquivOfIsGalois

English

There is a natural isomorphism between the profinite Galerkin group built from K ≃ₐ[k] K and the limit of Gal(L/k).

Русский

Существует естественное изоморфное соответствие между профинитной галуа-группой и пределом Gal(L/k).

LaTeX

$$$\text{profiniteGalGrp } k K \cong \lim (\text{asProfiniteGaloisGroupFunctor } k K)$$$

Lean4

instance [IsGalois k K] : CompactSpace (K ≃ₐ[k] K) :=
  (continuousMulEquivToLimit k K).symm.compactSpace

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