Relative algebraic closure

Stream: Is there code for X?

[Michael Stoll]

Does Mathlib have the notion of the algebraic closure of F within F' when F and F' are fields and F' is an F-algebra (i.e., the subfield of F' consisting of all elements of F' tha are algebraic over F)?

[Adam Topaz]

You could take the integral closure. I’m not sure if it will have a field instance in the appropriate cases

[Adam Topaz]

docs#integralClosure

[Michael Stoll]

OK; that's what I would have fallen back on, too. We may have to add the conversion to a docs#Subfield ...

[Michael Stoll]

Somewhat related:

import Mathlib

example {R S A : Type*} [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra S A] :
    Algebra R A :=
  RingHom.toAlgebra <| (algebraMap S A).comp <| algebraMap R S

I would expect this transitivity of structures to be directly available, but can't seem to find it.

[Adam Topaz]

It’s explicitly not available as an instance because you are meant to use docs#IsScalarTower

[Adam Topaz]

In other words, assume [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A]

[Adam Topaz]

But as a def, we may have docs#Algebra.trans or something like that

[Adam Topaz]

Maybe not… but note that things like docs#Algebra.IsIntegral.trans are formulated in terms of IsScalarTower

[Michael Stoll]

Yes, but there is no obvious way to get IsScalarTower R S A directly from the two algebra instances, as far as I can see.

[Michael Stoll]

Context: I'm trying to extend the theory of algebraic function fields of one variable. We have docs#FunctionField, but this only assumes [Algebra (RatFunc F) FF], and I need IsScalarTower F (RatFunc F) FF.

So is the recommendation to refactor docs#FunctionField to assume [IsScalarTower F (RatFunc F) FF] right away?

[Michael Stoll]

OK, I just found this:

variable {F FF : Type} [Field F] [Field FF] [inst : Algebra (RatFunc F) FF] (hF : FunctionField F FF)

noncomputable instance : Algebra F FF := Algebra.trans (S := RatFunc F)

instance : IsScalarTower F (RatFunc F) FF := IsScalarTower.of_algebraMap_eq (congrFun rfl)

so it looks like I can work with docs#FunctionField as it is for the time being...

[Michael Stoll]

(where Algebra.trans is the example from above).

[Adam Topaz]

I see. To be honest, I disagree with this definition of docs#FunctionField (which IMO should just mean a finitely generated extension, possibly assuming relatively algebraically closed).

[Adam Topaz]

Even in the one dimensional case, I don’t think it makes sense to assume such a IsScalarTower instance. Such an instance essentially is equivalent to naming a transcendental element, and it’s not clear to me that such a transcendental should be named by default

[Michael Stoll]

My gut feeling is that for practical purposes it is good to have a fixed transcendental element around (rather than to have to conjure one up each time it is needed), but let's see how far I get with the present set-up.