Almost every place admits a prescribed integral basis

Let F' / F be a finite separable extension and fix an F-basis b of F'. This file proves that b is an integral basis over the valuation ring of all but finitely many places of an algebraic function field F / k. This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Theorem 3.3.6.

There are two finiteness steps. First, any fixed element of F' is integral over 𝒪_P for all but finitely many P: outside the poles of the finitely many coefficients of its minimal polynomial over F, that polynomial is defined over 𝒪_P. Second, apply this simultaneously to the vectors of b and its trace-dual basis. If both bases are integral at P, the trace formula for the coordinates in b shows that every integral element has integral coordinates; integrality of the vectors of b proves the converse.

This theorem is the finiteness input for the different divisor: a single basis can be used to compute the complementary module away from finitely many places.

Main results

• TauCeti.Place.finite_setOf_not_isIntegral: an element integral over F is integral over the valuation rings of all but finitely many places.
• TauCeti.Place.finite_setOf_not_isIntegralBasis: every basis is an integral basis at all but finitely many places (Stichtenoth, Theorem 3.3.6).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.3.6.

Elements integral at almost every place

theorem TauCeti.Place.finite_setOf_not_isIntegral {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (hF : IsFunctionField k F) (x : F') (hx : IsIntegral F x) : {P : Place k F | ¬IsIntegral (↥P.integers) x}.Finite

A fixed element integral over F is integral at all but finitely many places.

Indeed, outside the poles of the coefficients of its minimal polynomial over F, that monic polynomial has coefficients in 𝒪_P and witnesses integrality over 𝒪_P.

Bases integral at almost every place

theorem TauCeti.Place.finite_setOf_not_isIntegralBasis {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (hF : IsFunctionField k F) {ι : Type u_1} [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (b : Module.Basis ι F F') : {P : Place k F | ¬IsIntegralBasis F' P b}.Finite

Every basis of a finite separable extension is an integral basis at all but finitely many places (Stichtenoth, Theorem 3.3.6).