field extension tower

Stream: Is there code for X?

[Edison Xie]

Do we have that for a finite field extension L over F and F's algclosure F_bar, F_bar is also an L-algebra and L_bar = F_bar?

[Edison Xie]

import Mathlib

noncomputable def algClosure_ext (L F F_bar: Type*) [Field F] [Field L] [Field F_bar] [Algebra F L]
    [Algebra F F_bar] [FiniteDimensional F L] [IsAlgClosure F F_bar] : Algebra L F_bar :=
  haveI : IsAlgClosed F_bar := IsAlgClosure.isAlgClosed F
  haveI : Algebra.IsAlgebraic F L := by exact Algebra.IsAlgebraic.of_finite F L
  RingHom.toAlgebra <| IsAlgClosed.lift (R := F) (S := L) (M := F_bar)

Should this be an instance?

[Junyan Xu]

It can't be an instance because the goal doesn't contain F. It could be if F_bar is replaced by AlgebraicClosure F.

[Edison Xie]

Junyan Xu said:

It can't be an instance because the goal doesn't contain F. It could be if F_bar is replaced by AlgebraicClosure F.

thanks! And do you have any suggestion toward my second question which is L / F being finite (or algebraic) then F_bar is also the closure of L?

[Junyan Xu]

I think you just need Algebra.IsAlgebraic.tower_top for that?

[Edison Xie]

docs#Algebra.IsAlgebraic.tower_top shows that F_bar is algebraic over L but why does it show F_bar is the algebraic closure of L I'm a bit confused

[Junyan Xu]

IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K (by definition)