English
If k is separably closed and K is a separable k-algebra, the algebra map algebraMap k K is surjective.
Русский
Если k сепарабельное замкнутое поле и K — сепарабельное над k алгебраическое расширение, то алгебраическая карта k→K сюръективна.
LaTeX
$$Function.Surjective (algebraMap k K)$$
Lean4
theorem algebraMap_surjective [IsSepClosed k] [Algebra k K] [Algebra.IsSeparable k K] :
Function.Surjective (algebraMap k K) :=
by
refine fun x => ⟨-(minpoly k x).coeff 0, ?_⟩
have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (Algebra.IsSeparable.isIntegral k x)
have hsep : IsSeparable k x := Algebra.IsSeparable.isSeparable k x
have h : (minpoly k x).degree = 1 :=
degree_eq_one_of_irreducible k (minpoly.irreducible (Algebra.IsSeparable.isIntegral k x)) hsep
have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C, add_eq_zero_iff_eq_neg] at this
exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm
