English
There is a multiplicative equivalence between the group of k-algebra automorphisms of K and the profinite limit of Gal(L/k) over finite Galois intermediate fields L.
Русский
Существует мульти-эквивалентность между группой automorphisms_K/k и профинитным пределом Gal(L/k) по конечным Галуа-полюгам L.
LaTeX
$$$\text{mulEquivToLimit}\; k\; K : (K \simeq_k K) \simeq_* \ \lim \limits_{\leftarrow} \; (\text{asProfiniteGaloisGroupFunctor } kK)\,,$$$
Lean4
/-- `algEquivToLimit` as a `MulEquiv`. -/
noncomputable def mulEquivToLimit [IsGalois k K] : (K ≃ₐ[k] K) ≃* limit (asProfiniteGaloisGroupFunctor k K)
where
toFun := algEquivToLimit k K
map_mul' := map_mul _
invFun := limitToAlgEquiv
left_inv := fun f ↦ AlgEquiv.ext fun x ↦ AlgEquiv.restrictNormal_commutes f (adjoin k { x }).1 ⟨x, _⟩
right_inv := fun g ↦ by
apply Subtype.val_injective
ext L
change (limitToAlgEquiv g).restrictNormal _ = _
ext x
have : ((limitToAlgEquiv g).restrictNormal L.unop) x = (limitToAlgEquiv g) x.1 := by
exact AlgEquiv.restrictNormal_commutes (limitToAlgEquiv g) L.unop x
simp_rw [this]
exact proj_adjoin_singleton_val _ _ _ _ x.2
