English
If p is irreducible and p splits over E, then the action of p.Gal on the roots p.rootSet E is pretransitive; i.e., for any x,y there exists g ∈ p.Gal with g·x = y.
Русский
Если p неприводен и p распадается над E, то действие p.Gal на корни p.rootSet E является предперестановочным; для любых x,y существует g ∈ p.Gal с g·x = y.
LaTeX
$$$\\text{MulAction.IsPretransitive } p.Gal\\ (p.rootSet E).\\Elem$$$
Lean4
theorem galAction_isPretransitive [Fact (p.Splits (algebraMap F E))] (hp : Irreducible p) :
MulAction.IsPretransitive p.Gal (p.rootSet E) :=
by
refine ⟨fun x y ↦ ?_⟩
have hx := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm x).2).2
have hy := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm y).2).2
obtain ⟨g, hg⟩ := (Normal.minpoly_eq_iff_mem_orbit p.SplittingField).mp (hy.symm.trans hx)
exact ⟨g, (rootsEquivRoots p E).apply_eq_iff_eq_symm_apply.mpr (Subtype.ext hg)⟩
