exists_algEquiv — Mathlib

English

Let L/K be normal. If x is conjugate to y, there exists σ with σ y = x.

Русский

Пусть L/K нормальное. Если x сопряжён к y, существует σ с σ y = x.

LaTeX

$$$IsConjRoot(K, x, y) \Rightarrow \exists \sigma : L \cong_K L, \sigma(y) = x$$$

Lean4

/-- Let `L / K` be a normal field extension. For any two elements `x` and `y` in `L`, if `y` is a
conjugate root of `x`, then there exists a `K`-automorphism `σ : L ≃ₐ[K] L` such
that `σ y = x`.
-/
theorem exists_algEquiv [Normal K L] {x y : L} (h : IsConjRoot K x y) : ∃ σ : L ≃ₐ[K] L, σ y = x :=
  by
  obtain ⟨σ, hσ⟩ := exists_algHom_of_splits_of_aeval (normal_iff.mp inferInstance) (h ▸ minpoly.aeval K x)
  exact ⟨AlgEquiv.ofBijective σ (σ.normal_bijective _ _ _), hσ⟩

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