Commit 2025-08-14 12:53 ee835422

feat(RatFunc): liftAlgebra and rank (#27640) Add analogous results from FractionRing in the special case of RatFunc. This is needed as RatFunc is a one-field-struct. The first three are scoped instances lifting structure from K[X] to RatFunc K. Our application is two results stating that with appropriate context, the rank of RatFunc K over RatFunc k is the rank of K over k.

• RatFunc.liftAlgebra (FractionRingversion)
• RatFunc.isScalarTower_liftAlgebra (FractionRing version)
• RatFunc.faithfulSMul' (FractionRing version)
• RatFunc.rank_ratFunc_ratFunc (mathlib has a version for FractionRing but we use the version for IsFractionRing combined with rank_polynomial_polynomial.)
• RatFunc.finrank_ratFunc_ratFunc The first three are declared as scoped instances of RatFunc. This creates a conflict with the current LaurentSeries file. To fix this, I have refactored to use the algebra instance coming from RatFunc.liftAlgebra instead of the coeAlgHom map defined in LaurentSeries. This has two main effects:
• It simplifies the file.
• The instance RatFunc.instCoePolynomial does not need to be hidden anymore. Looking forward to feedback! Xavier