English
For towers E/L/F and E/K/F with normality assumptions, there is a natural homomorphism from automorphisms of E fixing L to automorphisms of K fixing F, given by restriction to K.
Русский
Для цепей E/L/F и E/K/F при нормировочных условиях существует естественный гомоморфизм от автоморфизмов E, фиксирующих L, к автоморфизмам K, фиксирующим F, задающийся ограничением кK.
LaTeX
$$$\operatorname{RestrictRestrictAlgEquivMapHom}_{F}(K,L,E): \bigl(\operatorname{Aut}_L(E)\bigr) \to \bigl(\operatorname{Aut}_F(K)\bigr)$ является моноид-гомоморфизм, реализованный ограничением на $K$. $$
Lean4
/-- The map from the `Gal(E/L)` to `Gal(K/F)` where `E/L/F` and `E/K/F` are two towers of
extensions induced by the restriction to `K`. Note that we do require `K/F` to be normal but not
`E/L`. If this is the case (and everything is finite dimensional) and `K ∩ L = F` then this
map is surjective, see `IntermediateField.restrictRestrictMapHom_surjective`.
This map is injective if the compositum of `K` and `L` is `E`,
see `IntermediateField.restrictRestrictAlgEquivMapHom_injective`.
-/
noncomputable def restrictRestrictAlgEquivMapHom (F K L E : Type*) [Field F] [Field K] [Field L] [Field E] [Algebra F K]
[Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E] [IsScalarTower F K E] [IsScalarTower F L E] [Normal F K] :
(E ≃ₐ[L] E) →* (K ≃ₐ[F] K) :=
(AlgEquiv.restrictNormalHom K).comp (MulSemiringAction.toAlgAut (E ≃ₐ[L] E) F E)
