The different exponent of a tame or wild place

Let F' / k' be an extension of the algebraic function field F / k with F' / F finite and separable, and let P' be a place of F' / k' over P = P'.restrict k F. Dedekind's different theorem (Stichtenoth, Theorem 3.5.1) says that d(P' ∣ P) ≥ e(P' ∣ P) - 1 always, with equality exactly when the place is tame. The inequality is TauCeti.Place.ramificationIdx_le_differentExponent_add_one; this file introduces the tame/wild vocabulary (Stichtenoth, Definition 3.5.4) as TauCeti.Place.IsTame and TauCeti.Place.IsWild and supplies the second part: e(P' ∣ P) = d(P' ∣ P) + 1 holds exactly at the tame places, those where the residue extension of the local model is separable and the residue characteristic does not divide e(P' ∣ P), and at the wild places d(P' ∣ P) ≥ e(P' ∣ P) (Stichtenoth, Corollary 3.5.5).

Everything is read on the local model 𝒪_P ⊆ 𝒪'_P of TauCeti/FieldTheory/FunctionField/Different/Basic.lean, where the different exponent lives, so the two conditions are stated for the centre 𝔓 of P' on 𝒪'_P over the maximal ideal of the discrete valuation ring 𝒪_P, whose residue ring is the residue field of P (TauCeti.Place.center_restrict_asIdeal_eq_maximalIdeal). This is the same ideal-theoretic reading of the residue extension that TauCeti.Place.differentExponent_eq_zero_iff uses for unramifiedness. The theorem behind it is TauCeti.ramificationIdx_le_multiplicity_differentIdeal_iff.

Stichtenoth assumes a perfect constant field, under which residue extensions are separable and tameness is the single condition that the characteristic does not divide e(P' ∣ P). No such assumption is made here: over an imperfect residue field an inseparable residue extension already forces d(P' ∣ P) ≥ e(P' ∣ P), even at e(P' ∣ P) = 1, so the separability condition is part of the statement.

Main results

• TauCeti.Place.IsTame and TauCeti.Place.IsWild: tame and wild places, with TauCeti.Place.isTame_iff and TauCeti.Place.isWild_iff unfolding the two predicates into their defining residue conditions.
• TauCeti.Place.ramificationIdx_eq_differentExponent_add_one_iff: Dedekind's different theorem, second part (Stichtenoth, Theorem 3.5.1(b)), in the subtraction-free form e(P' ∣ P) = d(P' ∣ P) + 1, holding exactly at the tame places.
• TauCeti.Place.ramificationIdx_le_differentExponent_iff: e(P' ∣ P) ≤ d(P' ∣ P) exactly at the wild places (Stichtenoth, Corollary 3.5.5).
• TauCeti.Place.relativeDegree_eq_one_of_isSepClosed_of_differentExponent_eq_zero: a place with zero different exponent over a separably closed residue field has relative degree one.
• TauCeti.Divisor.coeff_different_add_one_eq_ramificationIdx_iff and TauCeti.Divisor.ramificationIdx_le_coeff_different_iff: the same statements read on the different divisor.
• TauCeti.Divisor.tameDifferent: the divisor ∑_{P'} (e(P' ∣ P) - 1) · P', with TauCeti.Divisor.tameDifferent_le_different and TauCeti.Divisor.tameDifferent_eq_different_iff: it is bounded by the different divisor, with equality exactly when every place is tame.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definition 3.5.4, Theorem 3.5.1 and Corollary 3.5.5.

def TauCeti.Place.IsTame (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') : Prop

A place P' of F' is tame over F (Stichtenoth, Definition 3.5.4) when the residue extension of its local model is separable and its ramification index is invertible in the residue field of P = P'.restrict k F.

The residue extension is read on the local model, between the residue ring of the maximal ideal of the discrete valuation ring 𝒪_P — which is the residue field of P, by TauCeti.Place.center_restrict_asIdeal_eq_maximalIdeal — and the residue ring of the centre of P' on 𝒪'_P. Stichtenoth assumes a perfect constant field, where the separability condition is automatic; unlike Stichtenoth's tamely ramified, an unramified place with separable residue extension also counts as tame here.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Place.isTame_iff (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') : IsTame k F P' ↔ Algebra.IsSeparable (↥(restrict k F P').integers ⧸ IsLocalRing.maximalIdeal ↥(restrict k F P').integers) (↥(integralClosure (↥(restrict k F P').integers) F') ⧸ (centerIntegralClosure k F P').asIdeal) ∧ ↑(ramificationIdx F P') ≠ 0

A place is tame exactly when the residue extension of its local model is separable and its ramification index is invertible in the residue field of P.

def TauCeti.Place.IsWild (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') : Prop

A place P' of F' is wild over F (Stichtenoth, Definition 3.5.4) when it is not tame: the residue extension of its local model is inseparable or its ramification index vanishes in the residue field of P.

Equations

• TauCeti.Place.IsWild k F P' = ¬TauCeti.Place.IsTame k F P'

@[simp]

theorem TauCeti.Place.isWild_iff (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') : IsWild k F P' ↔ ¬Algebra.IsSeparable (↥(restrict k F P').integers ⧸ IsLocalRing.maximalIdeal ↥(restrict k F P').integers) (↥(integralClosure (↥(restrict k F P').integers) F') ⧸ (centerIntegralClosure k F P').asIdeal) ∨ ↑(ramificationIdx F P') = 0

A place is wild exactly when the residue extension of its local model is inseparable or its ramification index vanishes in the residue field of P.

theorem TauCeti.Place.isTame_of_residueField_charZero (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') [CharZero (restrict k F P').ResidueField] : IsTame k F P'

A place is tame over a residue field of characteristic zero.

theorem TauCeti.Place.isTame_iff_not_dvd_ramificationIdx (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') [PerfectField k] (hF : IsFunctionField k F) (p : ℕ) [CharP k p] : IsTame k F P' ↔ ¬p ∣ ramificationIdx F P'

Over a perfect constant field a place is tame exactly when the characteristic does not divide its ramification index.

theorem TauCeti.Place.isTame_of_charZero (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') [CharZero k] : IsTame k F P'

In characteristic zero every place is tame: if the constant field k has characteristic zero, every place of F' is tame over F.

theorem TauCeti.Place.ramificationIdx_le_differentExponent_iff (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') : ramificationIdx F P' ≤ differentExponent k F P' ↔ IsWild k F P'

The different exponent reaches the ramification index exactly at the wild places (Stichtenoth, Corollary 3.5.5): e(P' ∣ P) ≤ d(P' ∣ P) if and only if P' is wild.

theorem TauCeti.Place.ramificationIdx_eq_differentExponent_add_one_iff (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k' F') : ramificationIdx F P' = differentExponent k F P' + 1 ↔ IsTame k F P'

Dedekind's different theorem, second part (Stichtenoth, Theorem 3.5.1(b)): the different exponent of P' is exactly one less than its ramification index if and only if P' is tame. It is stated as e(P' ∣ P) = d(P' ∣ P) + 1 so that no truncated subtraction of natural numbers appears.

theorem TauCeti.Place.relativeDegree_eq_one_of_isSepClosed_of_differentExponent_eq_zero (k : Type u) (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k F') [IsSepClosed (restrict k F P').ResidueField] (hd : differentExponent k F P' = 0) : relativeDegree k F P' = 1

If the residue field of the place below P' is separably closed and the different exponent of P' vanishes, then the relative residue degree of P' is one.

theorem TauCeti.Divisor.ramificationIdx_le_coeff_different_iff {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) (P' : Place k' F') : ↑(Place.ramificationIdx F P') ≤ AlgebraicGeometry.WeilDivisor.coeff (different k' F' hF) P' ↔ Place.IsWild k F P'

The different divisor at a wild place (Stichtenoth, Corollary 3.5.5): the coefficient of P' in Diff(F'/F) is at least e(P' ∣ P) if and only if P' is wild.

theorem TauCeti.Divisor.coeff_different_add_one_eq_ramificationIdx_iff {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) (P' : Place k' F') : AlgebraicGeometry.WeilDivisor.coeff (different k' F' hF) P' + 1 = ↑(Place.ramificationIdx F P') ↔ Place.IsTame k F P'

The different divisor detects tameness (Stichtenoth, Theorem 3.5.1(b) and Remark 3.4.4): the coefficient of P' in Diff(F'/F) is e(P' ∣ P) - 1, stated without subtraction, exactly when P' is tame.

noncomputable def TauCeti.Divisor.tameDifferent {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) : Divisor k' F'

The tame different ∑_{P'} (e(P' ∣ P) - 1) · P' of a finite separable extension F' / F of an algebraic function field: the value the different divisor Diff(F'/F) would take if every place of F' were tame (Stichtenoth, Theorem 3.5.1(b)). It is a divisor because a place with e(P' ∣ P) > 1 lies in the support of the different, and it is the lower bound for the different in the Hurwitz genus formula (Stichtenoth, Corollary 3.5.6).

Equations

• TauCeti.Divisor.tameDifferent k' F' hF = Finsupp.ofSupportFinite (fun (P' : TauCeti.Place k' F') => ↑(TauCeti.Place.ramificationIdx F P') - 1) ⋯

@[simp]

theorem TauCeti.Divisor.coeff_tameDifferent {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) (P' : Place k' F') : AlgebraicGeometry.WeilDivisor.coeff (tameDifferent k' F' hF) P' = ↑(Place.ramificationIdx F P') - 1

The coefficient of P' in the tame different is e(P' ∣ P) - 1.

theorem TauCeti.Divisor.zero_le_tameDifferent {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) : 0 ≤ tameDifferent k' F' hF

The tame different is effective: every ramification index is positive.

theorem TauCeti.Divisor.tameDifferent_le_different {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) : tameDifferent k' F' hF ≤ different k' F' hF

Dedekind's different theorem, first part, as an inequality of divisors (Stichtenoth, Theorem 3.5.1(a)): the tame different is bounded by the different divisor.

@[simp]

theorem TauCeti.Divisor.tameDifferent_eq_different_iff {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) : tameDifferent k' F' hF = different k' F' hF ↔ ∀ (P' : Place k' F'), Place.IsTame k F P'

The different divisor is the tame different exactly when every place is tame (Stichtenoth, Theorem 3.5.1(b)).