restrictComp_surjective — Mathlib

English

The map restrictComp p q hq is equal to the restriction map from q.Gal to p.Gal on the splitting field of p ∘ q.

Русский

Отображение restrictComp p q hq равно ограничению Gal(q)→Gal(p) на поле разложения p ∘ q.

LaTeX

$$$\\mathrm{restrictComp}\\ p\\ q\\ hq = \\mathrm{restrict}\\ p\\ (p\\circ q).SplittingField$$$

Lean4

theorem restrictComp_surjective (hq : q.natDegree ≠ 0) : Function.Surjective (restrictComp p q hq) :=
  by
  haveI : Fact (Splits (algebraMap F (SplittingField (comp p q))) p) := ⟨splits_in_splittingField_of_comp p q hq⟩
  simpa only [restrictComp] using restrict_surjective _ _

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