Rational-parameter degrees after extending constants

For an exact constant field k in F, extending constants by a finite separable extension k' / k preserves [F : k(x)]. The ambient field F' is the compositum of F and k', expressed by constantCompositum F k' F' = ⊤. No function-field hypothesis is needed.

Main results

• TauCeti.finrank_over_adjoin_simple_eq_of_constantCompositum_eq_top: [F' : k'(x)] = [F : k(x)] for every x ∈ F.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 3.6.1(c).

theorem TauCeti.finrank_over_adjoin_simple_eq_of_constantCompositum_eq_top {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] [Algebra.IsSeparable k k'] (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (x : F) : Module.finrank (↥k'⟮(algebraMap F F') x⟯) F' = Module.finrank (↥k⟮x⟯) F

A finite separable extension of an exact constant field preserves the degree over the subfield generated by any element of the original field (Stichtenoth, Proposition 3.6.1(c)).