English
The restricted action is compatible with the original action: applying restrict(p,E) to ϕ and then smul on x yields the same result as applying ϕ to x via rootsEquivRoots.
Русский
Ограниченное действие совместимо с исходным: применение restrict(p,E) к ϕ и последующее умножение на x даёт тот же результат, что и применение ϕ к x через rootsEquivRoots.
LaTeX
$$$\\uparrow(\\mathrm{restrict}(p,E)\\,\\varphi\\,\\cdot\\, x) = \\varphi\\,x$$$
Lean4
/-- `Polynomial.Gal.restrict p E` is compatible with `Polynomial.Gal.galAction p E`. -/
@[simp]
theorem restrict_smul [Fact (p.Splits (algebraMap F E))] (ϕ : E ≃ₐ[F] E) (x : rootSet p E) :
↑(restrict p E ϕ • x) = ϕ x :=
by
let ψ := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
change ↑(ψ (ψ.symm _)) = ϕ x
rw [AlgEquiv.apply_symm_apply ψ]
change ϕ (rootsEquivRoots p E ((rootsEquivRoots p E).symm x)) = ϕ x
rw [Equiv.apply_symm_apply (rootsEquivRoots p E)]
