The different exponent under the Galois action

Let F / k be a field extension and F' / F a finite separable extension. An F-automorphism σ of F' moves the places of F' / k (TauCeti.Place.instMulActionAlgEquiv) without moving the places of F / k below them. This file proves that it also preserves the different exponent: d(σ • P' ∣ P) = d(P' ∣ P). Together with the transitivity of the Galois action on the places over a place, this gives the remaining part of Stichtenoth's Corollary 3.7.2: in a finite Galois extension F' / F all places over a given place of F share one different exponent, as they share one ramification index and one relative degree (TauCeti.Place.ramificationIdx_eq_of_restrict_eq, TauCeti.Place.relativeDegree_eq_of_restrict_eq). At the level of divisors, the different divisor Diff(F' / F) is fixed by every F-automorphism of F'.

The different exponent is read off the different ideal of the local model 𝒪_P ⊆ 𝒪'_P, where 𝒪'_P is the integral closure in F' of the valuation ring 𝒪_P of P. Since σ fixes F, it maps 𝒪'_P onto itself and preserves the trace of F' / F, so it preserves the complementary module C_P = {z ∣ Tr_{F'/F} (z · 𝒪'_P) ⊆ 𝒪_P} and hence the different ideal, the inverse of C_P (TauCeti.galRestrict_apply_mem_differentIdeal_iff). An element of the different ideal of order exactly d(P' ∣ P) at P' (TauCeti.Place.exists_mem_differentIdeal_ord_eq) is carried to an element of the different ideal of the same order at σ • P', which bounds d(σ • P' ∣ P) from above; applying this to σ⁻¹ gives the reverse bound.

Main results

• TauCeti.Place.differentExponent_smul: an F-automorphism of F' preserves the different exponent.
• TauCeti.Place.differentExponent_eq_of_restrict_eq: the different exponent is constant on the places over a place in a finite Galois extension (Stichtenoth, Corollary 3.7.2).
• TauCeti.Divisor.smul_different: an F-automorphism of F' fixes the different divisor.

References

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

@[simp]

theorem TauCeti.Place.differentExponent_smul {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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (σ : Gal(F'/F)) (P' : Place k F') : differentExponent k F (σ • P') = differentExponent k F P'

An F-automorphism of F' preserves the different exponent: d(σ • P' ∣ P) = d(P' ∣ P) for every place P' of F' / k over the place P of F / k.

theorem TauCeti.Place.differentExponent_eq_of_restrict_eq {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'] [FiniteDimensional F F'] [IsGalois F F'] {P Q : Place k F'} (h : restrict k F P = restrict k F Q) : differentExponent k F P = differentExponent k F Q

The different exponent is constant on a fibre (Stichtenoth, Corollary 3.7.2): in a finite Galois extension F' / F, two places of F' / k over the same place of F / k have the same different exponent.

@[simp]

theorem TauCeti.Divisor.smul_different {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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) (σ : Gal(F'/F)) : σ • different k F' hF = different k F' hF

An F-automorphism of F' fixes the different divisor Diff(F' / F), as it preserves the different exponent at every place.

theorem TauCeti.Divisor.degree_tameDifferent_eq_finrank_mul_sum {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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] [IsGalois F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') (s : Finset (Place k F)) (hs : ∀ (P' : Place k F'), 1 < Place.ramificationIdx F P' → Place.restrict k F P' ∈ s) : ↑(degree (tameDifferent k F' hF)) = ↑(Module.finrank F F') * ∑ P ∈ s, (1 - 1 / ↑(P.ramificationIdxIn F')) * ↑P.degree

The degree of the tame different of a Galois extension, through its branch data: the places over a place P of F share one ramification index e_P, so the tame different ∑_{P'} (e(P' ∣ P) - 1) · P' has degree

[F' : F] · ∑_P (1 - 1/e_P) · deg P,

the sum being over any finite set of places of F containing every ramified one. With the Hurwitz genus formula in its tame form this is Riemann--Hurwitz for the quotient F' / F: the branch data (genus F; e_P) has deficit (2g' - 2)/[F' : F].