algebraic element over algebraically closed field

Stream: Is there code for X?

[Aaron Liu]

If L/K is a field extension and K is algebraically closed, then any element of L algebraic over K in fact belongs to K.

import Mathlib

variable {K : Type*} [Field K] [IsAlgClosed K]
-- variable {R : Type*} [CommRing R] [IsDomain R] [Algebra K R]
variable {L : Type*} [Field L] [Algebra K L]

example {x : L} (hx : IsAlgebraic K x) : ∃ y, algebraMap K L y = x := by
  sorry

[Artie Khovanov]

docs#IsAlgClosed.algebraMap_bijective_of_isIntegral

[Artie Khovanov]

or on the level of extensions: docs#IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic

[Artie Khovanov]

there's not a finrank_eq_one version, I think that should be added (I suppose I'll add it eventually when I merge my real closed field stuff, to make the APIs the same)

[Artie Khovanov]

also let me get on my soapbox and request a consensus for the spelling of "the given extension is trivial" and a consistent API on top of that

[Aaron Liu]

can you fill in the sorry?

[Artie Khovanov]

open IntermediateField in
example {x : L} (hx : IsAlgebraic K x) : ∃ y, algebraMap K L y = x := by
  have := isAlgebraic_adjoin_simple hx.isIntegral
  simpa [adjoin_eq_bot_iff, IntermediateField.mem_bot] using
    eq_bot_of_isAlgClosed_of_isAlgebraic K⟮x⟯

I wasn't very familiar with the IntermediateField API but we got there in the end, here you go

[Aaron Liu]

thanks

[Aaron Liu]

this should go in mathlib

[Aaron Liu]

do you wanna open a PR?

[Artie Khovanov]

nah
a principled API for "the algebra map is surjective" / "I am equal to the bottom subalgebra" should go in mathlib
but adding this lemma will do for now

[Artie Khovanov]

also IntermediateField.coe_bot and IntermediateField.mem_bot should be simp lemmas

[Aaron Liu]

I think this should also work for an integral domain R in place of the big field L

[Artie Khovanov]

yes
using docs#IsAlgClosed.algebraMap_bijective_of_isIntegral
but the API is worse there so I'm not gonna write a proof out rn