English
If k is a field and K is a domain with an integral extension, the algebra map algebraMap k K is bijective when k is algebraically closed.
Русский
Если k — поле и K — домен с интегральным расширением, то алгебраическая карта algebraMap k K является биективной при условии, что k алгебраически замкнуто.
LaTeX
$$$\forall {k K} [\mathrm{Field}\;k] [\mathrm{Ring}\;K] [\mathrm{IsDomain}\;K] [IsAlgClosed k] [\mathrm{Algebra}\;k\;K],\; \mathrm{Bijective} (algebraMap\; k\; K)$$$
Lean4
theorem algebraMap_bijective_of_isIntegral {k K : Type*} [Field k] [Ring K] [IsDomain K] [hk : IsAlgClosed k]
[Algebra k K] [Algebra.IsIntegral k K] : Function.Bijective (algebraMap k K) :=
by
refine ⟨RingHom.injective _, fun x ↦ ⟨-(minpoly k x).coeff 0, ?_⟩⟩
have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (Algebra.IsIntegral.isIntegral x)
have h : (minpoly k x).degree = 1 :=
degree_eq_one_of_irreducible k (minpoly.irreducible (Algebra.IsIntegral.isIntegral x))
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
