Algebraic extensions of the constant field

Adjoining an arbitrary algebraic extension of constants to a function field produces a function field over the enlarged constants, even when the extension is infinite.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.6.

theorem TauCeti.isAlgebraic_constantCompositum {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] {k' : Type u'} [CommRing k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F'] [Algebra.IsAlgebraic k k'] : Algebra.IsAlgebraic F ↥(constantCompositum F k' F')

The compositum with an algebraic algebra of constants is algebraic over the original field. The constants need only form a commutative ring, and their map into the ambient field need not be injective.

theorem TauCeti.essFiniteType_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'] [Algebra.EssFiniteType k F] (h : constantCompositum F k' F' = ⊤) : Algebra.EssFiniteType k' F'

The compositum is finitely generated over the new constants. A finite field-generating set for F / k also generates F' / k', since the two fields generate the compositum.

theorem TauCeti.IsFunctionField.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'] [Algebra.IsAlgebraic k k'] (hF : IsFunctionField k F) (h : constantCompositum F k' F' = ⊤) : IsFunctionField k' F'

Adjoining an arbitrary algebraic extension of constants to a function field gives a function field over the enlarged constants, provided the ambient field is their compositum. No finite-degree or separability assumption on the constants is needed.