Unramified constant field extensions

Let k' / k be finite and separable and suppose that F' is the compositum F k'. Then F' / F is separable and is unramified at every place.

These are the local inputs to the comparison of the divisor theories of F / k and F' / k'. Vanishing different exponents say that the different divisor of F' / F is zero, and e(P' | P) = 1 says that no place of F ramifies in F', so the conorm of the point divisor of a place of F is the sum of the point divisors of the places of F' above it with no multiplicities, leaving the residue degrees as the only local data to track. The genus, divisor-degree and Riemann–Roch comparisons of Stichtenoth, Section III.6 consume these local facts, but do not follow from them alone: they also need the constant field of F', the comparison of degrees normalised over k with those normalised over k', and base change for the Riemann–Roch spaces L(D), none of which is proved here.

Separability is inherited by scalar extension, which is TauCeti.isSeparable_of_constantCompositum_eq_top. For unramifiedness, choose a primitive element c of k' / k. Its image generates F' / F, while the derivative of the minimal polynomial of c evaluated at c is a nonzero element of k', so its image in F' is a constant and hence a unit at every place of F'. The derivative criterion for the different therefore makes every different exponent vanish.

Read backwards, unramifiedness detects new constants. If F' / F has prime degree and k is exact in F, a constant of F' outside k generates, together with F, all of F'; so as soon as a single place of F ramifies in F', the constant field of F' is still k. This is how the exactness of the constants of a Kummer cover such as y ^ 2 = f(x) is established.

Main results

• TauCeti.Place.differentExponent_eq_zero_of_constantCompositum_eq_top: every different exponent of the constant extension vanishes.
• TauCeti.Place.isUnramifiedAt_of_constantCompositum_eq_top: each corresponding local model is unramified.
• TauCeti.Place.ramificationIdx_eq_one_of_constantCompositum_eq_top: every place has ramification index one.
• TauCeti.isIntegrallyClosedIn_of_finrank_prime_of_ramificationIdx_ne_one: conversely, an extension of prime degree in which some place ramifies has no new constants.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 3.6.3(a), and the argument of Proposition 3.7.3(c).

theorem TauCeti.Place.differentExponent_eq_zero_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'] (hcomp : constantCompositum F k' F' = ⊤) (P' : Place k' F') : differentExponent k F P' = 0

Every different exponent of a finite separable constant extension vanishes (Stichtenoth, Proposition 3.6.3(a)): for a place P' of F' / k' lying over the place P = P'.restrict k F of F / k, the different exponent d(P' ∣ P) is zero, so the different divisor of F' / F is the zero divisor.

theorem TauCeti.Place.isUnramifiedAt_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'] (hcomp : constantCompositum F k' F' = ⊤) (P' : Place k' F') : Algebra.IsUnramifiedAt (↥(restrict k F P').integers) (centerIntegralClosure k F P').asIdeal

A finite separable constant extension is unramified at every place (Stichtenoth, Proposition 3.6.3(a)), in Mathlib's local formulation: for a place P' of F' / k' over P = P'.restrict k F, the local model of F' at P — the integral closure of the valuation ring 𝒪_P in F' — is unramified at the centre of P', so P' is unramified over P with separable residue extension.

theorem TauCeti.Place.ramificationIdx_eq_one_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'] (hcomp : constantCompositum F k' F' = ⊤) (P' : Place k' F') : ramificationIdx F P' = 1

Every place in a finite separable constant extension has ramification index one.

Ramification keeps the constant field exact

theorem TauCeti.isIntegrallyClosedIn_of_finrank_prime_of_ramificationIdx_ne_one {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'] [Algebra.IsSeparable F F'] (hex : IsIntegrallyClosedIn k F) (hp : Nat.Prime (Module.finrank F F')) {P' : Place k F'} (hP' : Place.ramificationIdx F P' ≠ 1) : IsIntegrallyClosedIn k F'

A ramified extension of prime degree acquires no new constants (the argument of Stichtenoth, Proposition 3.7.3(c)): if F' / F is finite separable of prime degree, k is the exact constant field of F, and some place of F' is ramified over F, then k is the exact constant field of F'.