English
If k is a field and K is an integral algebra over k with IsAlgClosed k, then the algebra map k → K is bijective.
Русский
Если k — поле и K — интегральное расширение над k, и k алгебраически замкнуто, то карта алгебра k → K биективна.
LaTeX
$$$\forall {k} {K} [\mathrm{Field}\;k] [\mathrm{CommRing}\;K] [\mathrm{IsDomain}\;K] [IsAlgClosed k] [\mathrm{Algebra}\;k\;K],\; Function.Bijective (algebraMap k K)$$$
Lean4
/-- If E/L/K is a tower of field extensions with E/L algebraic, and if M is an algebraically
closed extension of K, then any embedding of L/K into M/K extends to an embedding of E/K.
Known as the extension lemma in https://math.stackexchange.com/a/687914. -/
theorem surjective_restrictDomain_of_isAlgebraic {E : Type*} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E]
[Algebra.IsAlgebraic L E] : Function.Surjective fun φ : E →ₐ[K] M ↦ φ.restrictDomain L := fun f ↦
IntermediateField.exists_algHom_of_splits' (E := E) f fun s ↦
⟨Algebra.IsIntegral.isIntegral s, IsAlgClosed.splits_codomain _⟩
