Constants form integral bases in a constant field extension

Let F' = F · k' be a finite separable constant field extension of a field F with exact constant field k, and let P be a place of F / k. A basis of constants — the F-basis of F' given by a k-basis of k' — is an integral basis at P: its 𝒪_P-span is the integral closure of 𝒪_P in F'. Both the basis and its trace dual consist of constants, which are integral over 𝒪_P, and a basis whose trace dual is integral is an integral basis.

So the elements of F' integral over 𝒪_P are exactly the 𝒪_P-combinations of constants: the local model of a constant field extension at P is 𝒪_P ⊗[k] k'. This is the local input to the comparison of the Riemann–Roch spaces of F / k and F' / k'.

Main result

• TauCeti.Place.isIntegralBasis_constantBasis: a basis of constants is an integral basis at every place of F / k.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.6, the proof of Theorem 3.6.3.

theorem TauCeti.Place.isIntegralBasis_constantBasis {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.IsSeparable k k'] (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) {ι : Type u_1} [Finite ι] (b : Module.Basis ι k k') (P : Place k F) : IsIntegralBasis F' P (constantBasis hex h b)

A basis of constants is an integral basis at every place (Stichtenoth, proof of Theorem 3.6.3): for a finite separable extension of constants k' / k with k exact in F and F' = F · k', the 𝒪_P-span of the image of a k-basis of k' is the integral closure of 𝒪_P in F', for every place P of F / k.