Integral generators at totally ramified places

Let P' be a totally ramified place of a finite extension F' / F. Every uniformizer at P' generates the integral closure of the valuation ring below P'. Thus its powers form a local integral basis, not merely a basis of F' / F.

The proof uses the distinct orders of the first [F' : F] powers of the uniformizer. If an integral element is expanded in that basis, its order is the least order of a nonzero term. Since the order of the whole element is nonnegative, every coefficient is regular at the place below. This is the local integral-basis input for computing differents from derivatives.

References

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

theorem TauCeti.Place.algebra_adjoin_integralClosure_eq_top_of_isTotallyRamified (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 F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} (htot : IsTotallyRamified F P') {z : ↥(integralClosure (↥(restrict k F P').integers) F')} (hz : P'.ord ((algebraMap (↥(integralClosure (↥(restrict k F P').integers) F')) F') z) = 1) : (↥(restrict k F P').integers)[z] = ⊤

A uniformizer at a totally ramified place generates the integral closure of the valuation ring below it. Equivalently, its powers are an integral power basis at that place.