English
There is a natural monoid hom restriction from automorphisms of E over F to automorphisms of p.Gal, obtained by restricting an F-automorphism of E to the splitting field p.SplittingField.
Русский
Существует естественное однородное отображение-ограничение из автоморфизмов E над F в автоморфизмы p.Gal, задаваемое ограничением автоморфизма над F к разложившемуся полю p.SplittingField.
LaTeX
$$$\\operatorname{restrict}_{F,E}^{p}: \\mathrm{Aut}_F(E) \\to p.\\mathrm{Gal}$$$
Lean4
/-- Restrict from a superfield automorphism into a member of `gal p`. -/
def restrict [Fact (p.Splits (algebraMap F E))] : (E ≃ₐ[F] E) →* p.Gal :=
AlgEquiv.restrictNormalHom p.SplittingField