Zulip Chat Archive

Stream: Is there code for X?

Topic: Algebraic extension of algebraically closed field


view this post on Zulip 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.

view this post on Zulip Alex J. Best (Dec 04 2020 at 01:45):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Dec 04 2020 at 01:48):

It is finite

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Dec 04 2020 at 01:56):

You want the algebra to be a domain

view this post on Zulip 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