The different divisor of a finite separable extension

Let F' / k' be an extension of the algebraic function field F / k with F' / F finite and separable. The different exponent d(P' ∣ P) of TauCeti/FieldTheory/FunctionField/Different/Basic.lean vanishes at all but finitely many places of F', so the formal sum

Diff(F'/F) = ∑_{P'} d(P' ∣ P) · P'

is a divisor of F' / k' — the different divisor (Stichtenoth, Definition 3.4.3 and Remark 3.4.4). It is effective, its support is exactly the set of ramified places, and Dedekind's different theorem reads on it as e(P' ∣ P) ≤ Diff(F'/F)(P') + 1.

The finiteness

Fix once and for all an F-basis b of F'. At a place P of F / k at which every b i is integral and at which the discriminant disc(b) ∈ F is a unit, the complementary module of the local model 𝒪_P ⊆ 𝒪'_P is 𝒪'_P itself: Mathlib's isIntegral_discr_mul_of_mem_traceDual makes disc(b) · x integral for every x of the trace dual, and dividing by the unit disc(b) puts x back in 𝒪'_P. So the different ideal of the local model is the unit ideal and d(P' ∣ P) = 0 for every P' over P.

Both exceptional conditions hold at only finitely many P: the first because a fixed element of F' is integral at almost every place (TauCeti.Place.finite_setOf_not_isIntegral), the second because disc(b) is a nonzero element of F and so has finitely many zeros and poles (TauCeti.Place.finite_setOf_ord_ne_zero). Each of the finitely many exceptional places carries finitely many places of F' (TauCeti.Place.finite_setOf_restrict_eq), which bounds the support.

No local integral basis is needed for this, only integrality of the vectors of one fixed global basis: the discriminant estimate bounds the trace dual of 𝒪'_P by disc(b)⁻¹ · 𝒪'_P for any integral spanning family, and once disc(b) is a unit at P that bound already forces equality, whether or not b happens to be an 𝒪_P-basis of 𝒪'_P.

Main definitions

• TauCeti.Divisor.different: the different divisor Diff(F'/F).

Main results

• TauCeti.Place.finite_setOf_differentExponent_ne_zero and TauCeti.Place.finite_setOf_exists_differentExponent_ne_zero: the different exponent vanishes at all but finitely many places of F', and only finitely many places of F ramify.
• TauCeti.Divisor.zero_le_different: the different divisor is effective (Stichtenoth, Remark 3.4.4).
• TauCeti.Divisor.mem_support_different_iff_not_isUnramifiedAt: its support is the set of ramified places (Stichtenoth, Corollary 3.5.5).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definition 3.4.3, Remark 3.4.4 and Corollary 3.5.5.

theorem TauCeti.Place.finite_setOf_differentExponent_ne_zero (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 F 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' | differentExponent k F P' ≠ 0}.Finite

The different exponent vanishes at all but finitely many places of F' / k' (Stichtenoth, Proposition 3.4.2 and Definition 3.4.3). This is what makes the different divisor a divisor.

theorem TauCeti.Place.finite_setOf_exists_differentExponent_ne_zero (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 F 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 | ∃ (P' : Place k' F'), restrict k F P' = P ∧ differentExponent k F P' ≠ 0}.Finite

Almost every place of F is unramified in F': only finitely many places of F / k carry an extension with nonzero different exponent. This is the downstairs form of the finiteness, the one a sum over the ramified places of F runs on.

noncomputable def TauCeti.Divisor.different {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 F 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 different divisor Diff(F'/F) = ∑_{P'} d(P' ∣ P) · P' of a finite separable extension F' / F of an algebraic function field (Stichtenoth, Definition 3.4.3).

Equations

• TauCeti.Divisor.different k' F' hF = Finsupp.ofSupportFinite (fun (P' : TauCeti.Place k' F') => ↑(TauCeti.Place.differentExponent k F P')) ⋯

@[simp]

theorem TauCeti.Divisor.coeff_different {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 F 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' = ↑(Place.differentExponent k F P')

The coefficient of P' in the different divisor is the different exponent d(P' ∣ P).

theorem TauCeti.Divisor.mem_support_different_iff {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 F 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'} : P' ∈ (different k' F' hF).support ↔ Place.differentExponent k F P' ≠ 0

A place lies in the support of the different divisor exactly when its different exponent is nonzero.

theorem TauCeti.Divisor.isEffective_different {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 F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) : AlgebraicGeometry.WeilDivisor.IsEffective (different k' F' hF)

The different divisor is effective (Stichtenoth, Remark 3.4.4).

theorem TauCeti.Divisor.zero_le_different {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 F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) : 0 ≤ different k' F' hF

Effectivity of the different divisor, in the order form the degree bound consumes.

theorem TauCeti.Divisor.zero_le_degree_different {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 F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) : 0 ≤ degree (different k' F' hF)

The different divisor has nonnegative degree, the input the Hurwitz genus formula reads it through.

theorem TauCeti.Divisor.mem_support_different_iff_not_isUnramifiedAt {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 F 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'} : P' ∈ (different k' F' hF).support ↔ ¬Algebra.IsUnramifiedAt (↥(Place.restrict k F P').integers) (Place.centerIntegralClosure k F P').asIdeal

The support of the different divisor is the set of ramified places (Stichtenoth, Corollary 3.5.5), ramification being read in Mathlib's Algebra.IsUnramifiedAt sense at the centre of P' on the local model, which asks for a separable residue extension as well as e(P' ∣ P) = 1.

theorem TauCeti.Divisor.mem_support_different_of_one_lt_ramificationIdx {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 F 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'} (h : 1 < Place.ramificationIdx F P') : P' ∈ (different k' F' hF).support

A ramified place lies in the support of the different divisor, with no hypothesis on the residue extension (Stichtenoth, Corollary 3.5.5).

theorem TauCeti.Divisor.ramificationIdx_le_coeff_different_add_one {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 F 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' + 1

Dedekind's different theorem (Stichtenoth, Theorem 3.5.1(a)) at the level of divisors: the coefficient of P' in Diff(F'/F) is at least e(P' ∣ P) - 1, stated without subtraction.

theorem TauCeti.Divisor.different_eq_zero_iff {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 F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) : different k' F' hF = 0 ↔ ∀ (P' : Place k' F'), Place.differentExponent k F P' = 0

The different divisor vanishes exactly when no place of F' ramifies.