English
There is a categorical isomorphism between the profinite Galerkin group built from automorphisms of K/k and the limit of Gal(L/k) over finite Galois intermediate fields.
Русский
Существует категориальная изоморфия между профинитной галуа-группой автоморфизмов K/k и пределом Gal(L/k) по конечным Галуа-полуистинным полям.
LaTeX
$$$\text{profiniteGalGrp } k K \cong \lim (\text{asProfiniteGaloisGroupFunctor } k K)$$$
Lean4
/-- The `ContinuousMulEquiv` between `K ≃ₐ[k] K` and `lim Gal(L/k)` where `L` is a
`FiniteGaloisIntermediateField` ordered by inverse inclusion, obtained
from `InfiniteGalois.mulEquivToLimit` -/
noncomputable def continuousMulEquivToLimit [IsGalois k K] : (K ≃ₐ[k] K) ≃ₜ* limit (asProfiniteGaloisGroupFunctor k K)
where
toMulEquiv := mulEquivToLimit k K
continuous_toFun := algEquivToLimit_continuous
continuous_invFun := mulEquivToLimit_symm_continuous
