English
The map galActionHom is injective: different Galois automorphisms induce different permutations of the roots.
Русский
Отображение galActionHom инъективно: разные галуа-автоморфизмы порождают разные перестановки корней.
LaTeX
$$$\\mathrm{galActionHom\\,injective}$$$
Lean4
/-- `gal p` embeds as a subgroup of permutations of the roots of `p` in `E`. -/
theorem galActionHom_injective [Fact (p.Splits (algebraMap F E))] : Function.Injective (galActionHom p E) :=
by
rw [injective_iff_map_eq_one]
intro ϕ hϕ
ext (x hx)
have key := Equiv.Perm.ext_iff.mp hϕ (rootsEquivRoots p E ⟨x, hx⟩)
change
rootsEquivRoots p E (ϕ • (rootsEquivRoots p E).symm (rootsEquivRoots p E ⟨x, hx⟩)) =
rootsEquivRoots p E ⟨x, hx⟩ at key
rw [Equiv.symm_apply_apply] at key
exact Subtype.ext_iff.mp (Equiv.injective (rootsEquivRoots p E) key)
