English
Under the congruence isomorphism, the action on an element x ∈ L agrees with the original G-action: (mulEquivCongr G H K L g) • x = g • x.
Русский
Существующий изоморфизм сохраняет действие на элемент x ∈ L: (mulEquivCongr G H K L g) • x = g • x.
LaTeX
$$mulEquivCongr_apply_smul G H K L g x$$
Lean4
/-- The homomorphism from `Gal(K/k)` to `lim Gal(L/k)` where `L` is a
`FiniteGaloisIntermediateField k K` ordered by inverse inclusion. It is induced by the
canonical projections from `Gal(K/k)` to `Gal(L/k)`.
-/
noncomputable def algEquivToLimit : (K ≃ₐ[k] K) →* limit (asProfiniteGaloisGroupFunctor k K)
where
toFun
σ :=
{ val := fun L ↦ σ.restrictNormalHom L.unop
property := fun {L₁ L₂} π ↦ by
algebraize [Subsemiring.inclusion π.1.le]
have : IsScalarTower k L₂.unop L₁.unop := IsScalarTower.of_algebraMap_eq (congrFun rfl)
have : IsScalarTower L₂.unop L₁.unop K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
apply (IsScalarTower.AlgEquiv.restrictNormalHom_comp_apply L₂.unop L₁.unop σ).symm }
map_one' := by
simp only [map_one]
rfl
map_mul' x
y := by
simp only [map_mul]
rfl
