English
Let L be a field extension of K, with L normal over K. If y ∈ L is algebraic over K and x ∈ L is a root of the minimal polynomial of y over K, then there exists a K-algebra automorphism σ of L such that σ(x) = y. In other words, x and y are Galois conjugates over K.
Русский
Пусть L есть расширение поля K и L нормально над K. Пусть y ∈ L является алгебраическим над K и x ∈ L является корнем минимального многочлена y над K. Тогда существует K-алгебраическая автоморфия σ L → L такая, что σ(x) = y. Иными словами, x и y являются Галуа-сопряженными над K.
LaTeX
$$$\exists \sigma: L \simeq_K L, \ σ(x) = y,$$$
Lean4
/-- If `x : L` is a root of `minpoly K y`, then we can find `(σ : L ≃ₐ[K] L)` with `σ x = y`.
That is, `x` and `y` are Galois conjugates. -/
theorem exists_algEquiv_of_root [Normal K L] {x y : L} (hy : IsAlgebraic K y)
(h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ x = y :=
by
have hx : IsAlgebraic K x := ⟨minpoly K y, ne_zero hy.isIntegral, h_ev⟩
set f : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := algEquiv hx (eq_of_root hy h_ev)
have hxy : (liftNormal f L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y := by
rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]
exact ⟨(liftNormal f L), hxy⟩
