English
The map sending a polynomial to its image in the adjoint algebra is injective when x is integral.
Русский
Отображение полинома в сопряжённую алгебру инъективно при условии интегральности x.
LaTeX
$$$\text{Minpoly.toAdjoin}\;{{R}\;{x}}\text{ injective given } IsIntegral R x$$$
Lean4
/-- Let `L / K` be a field extension. If `x` is a separable element over `K` and the minimal polynomial
of `x` splits in `L`, then `x` is not in `K` if and only if there exists a conjugate
root of `x` over `K` in `L` which is not equal to `x` itself.
-/
theorem notMem_iff_exists_ne_and_isConjRoot {x : L} (h : IsSeparable K x) (sp : (minpoly K x).Splits (algebraMap K L)) :
x ∉ (⊥ : Subalgebra K L) ↔ ∃ y : L, x ≠ y ∧ IsConjRoot K x y := by
calc
_ ↔ 2 ≤ (minpoly K x).natDegree := (minpoly.two_le_natDegree_iff h.isIntegral).symm
_ ↔ 2 ≤ Fintype.card ((minpoly K x).rootSet L) := ((Polynomial.card_rootSet_eq_natDegree h sp) ▸ Iff.rfl)
_ ↔ Nontrivial ((minpoly K x).rootSet L) := Fintype.one_lt_card_iff_nontrivial
_ ↔ ∃ y : ((minpoly K x).rootSet L), ↑y ≠ x :=
((nontrivial_iff_exists_ne ⟨x, mem_rootSet.mpr ⟨minpoly.ne_zero h.isIntegral, minpoly.aeval K x⟩⟩).trans
⟨fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mpr hy⟩, fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mp hy⟩⟩)
_ ↔ _ :=
⟨fun ⟨⟨y, hy⟩, hne⟩ => ⟨y, ⟨hne.symm, (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mpr hy⟩⟩,
fun ⟨y, hne, hy⟩ => ⟨⟨y, (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mp hy⟩, hne.symm⟩⟩
