Algebraic extension of algebraically closed field

Stream: Is there code for X?

[Devon Tuma]

I've started looking at what is needed to eventually derive the classical nullstellensatz from #4962 and one thing that seems to be missing from mathlib is that an integral/algebraic extension of an algebraically closed field is surjective. Something like:

example {R S : Type*} [field R] [is_alg_closed R] [comm_ring S]
  (f : R →+* S) (hf : f.is_integral) : function.surjective f :=
begin
  intro x,
  obtain ⟨p, hp⟩ := hf x,
  sorry
end

I can't find anything giving this in mathlib, and trying to prove it myself I ran into trouble trying to get a particular linear factor corresponding to a particular root of p.

[Alex J. Best]

I don't think the statement you have is true is it? $\mathbf C \hookrightarrow \mathbf C [\epsilon]/ \epsilon^2$ is integral but the map isn't surjective

[Devon Tuma]

Ah, then there should probably also be an assumption that the extension is finite, however that is expressed in mathlib.

[Kenny Lau]

It is finite

[Devon Tuma]

Maybe my mistake is expecting the original map to give the isomorphism? An algebraically closed field has no proper algebraic extensions, but the map giving the isomorphism isn't necessarilly the original map?

[Adam Topaz]

You want the algebra to be a domain

[Devon Tuma]

Yes, I only really need the case where the algebraic extension is R[x]/M for a maximal ideal M, in which case its a domain