The different exponent of a place #
Let F' / k' be an extension of the field extension F / k in which F' / F is finite and
separable, and let P' be a place of F' / k' lying over the place P = P'.restrict k F of
F / k. Stichtenoth attaches to that pair the different exponent d(P' ∣ P), read off the
complementary module of the local extension 𝒪_P ⊆ 𝒪'_P, where 𝒪_P is the valuation ring of P
and 𝒪'_P its integral closure in F'. This file defines it and proves the two facts that make
it a divisor-theoretic invariant: Dedekind's different theorem, d(P' ∣ P) ≥ e(P' ∣ P) - 1,
and the vanishing criterion that singles out the unramified places.
The complementary module C_P = {z | Tr_{F'/F} (z · 𝒪'_P) ⊆ 𝒪_P} is an invertible fractional
𝒪'_P-ideal whose inverse is Mathlib's differentIdeal 𝒪_P 𝒪'_P, so Stichtenoth's -v_{P'}(t)
for a generator t of C_P is the multiplicity of the centre of P' on 𝒪'_P in that ideal.
That multiplicity is the definition used here, and no complementary module is rebuilt.
The local model 𝒪_P ⊆ 𝒪'_P is a pair of affine models in the sense of
TauCeti/FieldTheory/FunctionField/AffineModel/, the smallest one that sees P: 𝒪_P is a
discrete valuation ring with fraction field F, and 𝒪'_P is a Dedekind domain, module-finite
over it, with fraction field F'. It is constructed in
TauCeti/FieldTheory/FunctionField/Place/Extension/Basic.lean; the action of 𝒪_P on F'
and the scalar tower it sits in are deliberately not global instances, so they are reinstalled
here as local instances. The identification of the extension-theoretic data of P' with the
ideal-theoretic data of its centre on 𝒪'_P is then the affine-model dictionary of
TauCeti/FieldTheory/FunctionField/AffineModel/Extension.lean.
Separability of F' / F is the hypothesis of record for the different: without it the
complementary module degenerates. Nothing here needs an exactness hypothesis on the constant
fields, and nothing needs k perfect.
Main definitions #
TauCeti.Place.centerIntegralClosure: the centre ofP'on the local model𝒪'_P.TauCeti.Place.differentExponent: the different exponentd(P' ∣ P)(Stichtenoth, Definition 3.4.3).
Main results #
TauCeti.Place.center_restrict_asIdeal_eq_maximalIdeal: the prime of𝒪_Pbelow the centre ofP'on the local model is the maximal ideal of𝒪_P, so the residue extension the different exponent reads is the residue-field extension of the two places.TauCeti.Place.pow_dvd_differentIdeal_iff_le_differentExponent: the characteristic property of the different exponent,𝔓'^n ∣ differentIdeal 𝒪_P 𝒪'_P ↔ n ≤ d(P' ∣ P).TauCeti.Place.ramificationIdx_le_differentExponent_add_one: Dedekind's different theorem (Stichtenoth, Theorem 3.5.1(a)), in the subtraction-free forme(P' ∣ P) ≤ d(P' ∣ P) + 1.TauCeti.Place.differentExponent_pos_of_one_lt_ramificationIdx: a ramified place has positive different exponent — the direction of Stichtenoth's Corollary 3.5.5 that needs no hypothesis on the residue extension.TauCeti.Place.differentExponent_eq_zero_iff: the different exponent vanishes exactly at the places where the local model is unramified, in Mathlib'sAlgebra.IsUnramifiedAtsense, which asks for a separable residue extension as well ase(P' ∣ P) = 1.TauCeti.Place.differentIdeal_eq_top_of_ord_discr_eq_zeroandTauCeti.Place.differentExponent_eq_zero_of_ord_discr_eq_zero: the different ideal of the local model, and hence the different exponent aboveP, is trivial as soon as someF-basis ofF'is integral atPwith unit discriminant there.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definition 3.4.1, Proposition 3.4.2, Definition 3.4.3, Theorem 3.5.1 and Corollary 3.5.5.
A basis integral at P with unit discriminant makes the local model self-dual: if some
F-basis of F' has vectors integral over 𝒪_P and discriminant a unit at P, then the trace
dual of 𝒪'_P is 𝒪'_P itself.
The different ideal of the local model is trivial away from the discriminant: if some
F-basis of F' has integral vectors and unit discriminant at P, then the local model
𝒪_P ⊆ 𝒪'_P has unit different ideal.
The local model 𝒪'_P of F' / k' at P' consists of functions regular at P': its
elements are integral over 𝒪_P, whose functions are regular at P'.
The prime of 𝒪_P below the centre of P' on the local model is the maximal ideal of
𝒪_P: the residue extension read on the local model is the residue-field extension of the two
places.
The centre of P' on the local model 𝒪'_P: the height one prime of the integral closure
of 𝒪_P in F' consisting of the functions that vanish at P'.
Equations
- TauCeti.Place.centerIntegralClosure k F P' = P'.center ⋯
Instances For
The centre of P' on the local model lies over the maximal ideal of 𝒪_P, so the residue
extension of the local model is read at the residue field of P.
The different exponent d(P' ∣ P) of a place P' of F' / k' over the place
P = P'.restrict k F of F / k (Stichtenoth, Definition 3.4.3), for F' / F finite and
separable: the multiplicity with which the centre of P' on the local model 𝒪'_P divides the
different ideal of 𝒪'_P over 𝒪_P.
Stichtenoth defines it as -v_{P'}(t) for a generator t of the complementary module
C_P = {z | Tr_{F'/F} (z · 𝒪'_P) ⊆ 𝒪_P}; that module is the inverse of the different ideal, so
the two readings agree.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The characteristic property of the different exponent: the n-th power of the centre of
P' divides the different ideal of the local model exactly when n ≤ d(P' ∣ P).
Dedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)): the different
exponent of a place is at least one less than its ramification index. It is stated as
e(P' ∣ P) ≤ d(P' ∣ P) + 1 so that no truncated subtraction of natural numbers appears.
Unlike the second part of that theorem — equality exactly in the tame case — this half needs no
hypothesis beyond separability of F' / F, and in particular none on the residue extension.
A ramified place has a positive different exponent, so it lies in the support of the different divisor (Stichtenoth, Corollary 3.5.5; this direction needs no hypothesis on the residue extension).
The different exponent of P' vanishes exactly at the unramified places (Stichtenoth,
Corollary 3.5.5). Unramifiedness is Mathlib's Algebra.IsUnramifiedAt for the local model at the
centre of P', which asks for a separable residue extension as well as e(P' ∣ P) = 1; over an
imperfect residue field the two conditions genuinely differ, and
TauCeti.Place.differentExponent_pos_of_one_lt_ramificationIdx is the half that survives without
the separability.
The different exponent vanishes away from the discriminant: if some F-basis of F' has
integral vectors and unit discriminant at the place P = P'.restrict k F below P', then
d(P' ∣ P) = 0.