restrict — Mathlib

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

Похожие утверждения