Let F be a function field over Fq. If E is an algebraic extension of Fq which is contained in F then it is finite over Fq.

To implement this, we model the following tower of extensions:

                            E(X) - F
                           /   \   |
                        E[X]   Fq(X)
                        /  \    /
                       E   Fq[X]
                        \  /
                          Fq

by assuming algebra hypotheses on the level of Fq[X] and E[X] and use

attribute [local instance] Polynomial.algebra

together with the scoped RatFunc instances RatFunc.liftAlgebra and RatFunc.isScalarTower_liftAlgebra to obtain the appropriate algebra instances from RatFunc Fq/E.

One annoying thing is that using these instances creates a diamond with RatFunc.instSMulOfFractionRingPolynomial, I am working on trying to find a fix but don't have anything at the moment. I am open to suggestions!

Here are some details on this diamond:
Since both RatFunc E and FractionRing E[X] (which are not defeq) have an IsFractionRing E[X] instance we get two maps coming from RatFunc.liftAlgebra:

1. (RatFunc.liftAlgebra Fq (FractionRing E[X]))
2. (RatFunc.liftAlgebra Fq (RatFunc E))

Where the first one is transported back to RatFunc E via RatFunc.instSMulOfFractionRingPolynomial. Analyzing

@RatFunc.instSMulOfFractionRingPolynomial _ _ (RatFunc Fq) (RatFunc.liftAlgebra Fq (FractionRing E[X])).toSMul
    = (RatFunc.liftAlgebra Fq (RatFunc E)).toSMul

we see that this boils down to
{ toFractionRing := (IsLocalization.lift ⋯) x } = (IsFractionRing.lift ⋯) x not being defeq.

Co-authored-by: María Inés de Frutos Fernández <[email protected]>