## Stream: Is there code for X?

### Topic: Algebraic extension of algebraically closed field

#### Devon Tuma (Dec 04 2020 at 01:34):

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 (Dec 04 2020 at 01:45):

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 (Dec 04 2020 at 01:48):

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

It is finite

#### Devon Tuma (Dec 04 2020 at 01:55):

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 (Dec 04 2020 at 01:56):

You want the algebra to be a domain

#### Devon Tuma (Dec 04 2020 at 01:58):

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

Last updated: May 19 2021 at 02:10 UTC