Commit 2026-05-06 16:04 60da1e5a

feat(FunctionField): constant extensions are finite (#37388) 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.