Reading the different exponent on an arbitrary affine model

The different exponent d(P' ∣ P) of a place P' of F' / k' is defined on the local model 𝒪_P ⊆ 𝒪'_P at P = P'.restrict k F. This file shows that it may be read on any affine model of F on which P' is finite: if B is such a model and C is its integral closure in F', then d(P' ∣ P) is the coefficient of differentIdeal B C at the centre of P' on C.

The local model is the localization of B at the centre of P, and 𝒪'_P is the matching localization of C, so this is the localization invariance of the coefficients of the different ideal, TauCeti.multiplicity_differentIdeal_eq_multiplicity_under.

Main results

• TauCeti.Place.differentExponent_eq_multiplicity_center: the different exponent is the coefficient of the different ideal of an affine model at the centre of the place.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.4.

theorem TauCeti.Place.differentExponent_eq_multiplicity_center {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 F F'] [Algebra.IsSeparable F F'] {B : Type u_1} {C : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra B F] [IsFractionRing B F] [CommRing C] [IsDedekindDomain C] [Algebra C F'] [IsFractionRing C F'] [Algebra B C] [Algebra B F'] [IsScalarTower B C F'] [IsScalarTower B F F'] [IsIntegralClosure C B F'] [Module.IsTorsionFree B C] (P' : Place k' F') (hC : ∀ (c : C), (algebraMap C F') c ∈ P'.integers) : differentExponent k F P' = multiplicity (P'.center hC).asIdeal (differentIdeal B C)

The different exponent can be read on an affine model: if P' is finite on the integral closure C in F' of an affine model B of F, then d(P' ∣ P) is the coefficient of the different ideal of C over B at the centre of P'.