The different in a tower of function fields

For a tower of finite separable extensions F₀ ⊆ F₁ ⊆ F₂, the different exponent at a place P₂ satisfies

d(P₂ / P₀) = e(P₂ / P₁) d(P₁ / P₀) + d(P₂ / P₁).

Consequently the different divisors satisfy

Diff(F₂ / F₀) = Con(Diff(F₁ / F₀)) + Diff(F₂ / F₁).

The proof reads Mathlib's transitivity theorem for different ideals coefficientwise on the local model over P₀. Its middle layer is an affine model of F₁ rather than the local model at P₁ used to define d(P₂ / P₁); TauCeti.Place.differentExponent_eq_multiplicity_center shows that the different exponent can be read on any affine model, by localizing it at the centre of P₁.

This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Corollary 3.4.12.

Main results

• TauCeti.Place.differentExponent_restrict_add: transitivity of different exponents.
• TauCeti.Divisor.different_eq_conorm_add: transitivity of different divisors.

theorem TauCeti.Place.differentExponent_restrict_add {k₀ : Type u₀} {k₁ : Type u₁} {k₂ : Type u₂} {F₀ : Type v₀} {F₁ : Type v₁} {F₂ : Type v₂} [Field k₀] [Field k₁] [Field k₂] [Field F₀] [Field F₁] [Field F₂] [Algebra k₀ k₁] [Algebra k₁ k₂] [Algebra k₀ k₂] [Algebra F₀ F₁] [Algebra F₁ F₂] [Algebra F₀ F₂] [IsScalarTower F₀ F₁ F₂] [Algebra k₀ F₀] [Algebra k₁ F₁] [Algebra k₂ F₂] [Algebra k₀ F₁] [Algebra k₁ F₂] [Algebra k₀ F₂] [IsScalarTower k₀ k₁ F₁] [IsScalarTower k₁ k₂ F₂] [IsScalarTower k₀ F₀ F₁] [IsScalarTower k₁ F₁ F₂] [IsScalarTower k₀ k₂ F₂] [IsScalarTower k₀ F₀ F₂] [FiniteDimensional F₀ F₁] [FiniteDimensional F₁ F₂] [Algebra.IsSeparable F₀ F₁] [Algebra.IsSeparable F₁ F₂] (P₂ : Place k₂ F₂) : differentExponent k₀ F₀ P₂ = ramificationIdx F₁ P₂ * differentExponent k₀ F₀ (restrict k₁ F₁ P₂) + differentExponent k₁ F₁ P₂

Different exponents are transitive in towers (Stichtenoth, Corollary 3.4.12): the different exponent of P₂ over P₀ is the different exponent over P₁, plus the exponent of P₁ over P₀ multiplied by e(P₂ / P₁).

theorem TauCeti.Divisor.different_eq_conorm_add {k₀ : Type u₀} {k₁ : Type u₁} {k₂ : Type u₂} {F₀ : Type v₀} {F₁ : Type v₁} {F₂ : Type v₂} [Field k₀] [Field k₁] [Field k₂] [Field F₀] [Field F₁] [Field F₂] [Algebra k₀ k₁] [Algebra k₁ k₂] [Algebra k₀ k₂] [Algebra F₀ F₁] [Algebra F₁ F₂] [Algebra F₀ F₂] [IsScalarTower F₀ F₁ F₂] [Algebra k₀ F₀] [Algebra k₁ F₁] [Algebra k₂ F₂] [Algebra k₀ F₁] [Algebra k₁ F₂] [Algebra k₀ F₂] [IsScalarTower k₀ k₁ F₁] [IsScalarTower k₁ k₂ F₂] [IsScalarTower k₀ F₀ F₁] [IsScalarTower k₁ F₁ F₂] [IsScalarTower k₀ k₂ F₂] [IsScalarTower k₀ F₀ F₂] [FiniteDimensional F₀ F₁] [FiniteDimensional F₁ F₂] [Algebra.IsSeparable F₀ F₁] [Algebra.IsSeparable F₁ F₂] (hF₀ : IsFunctionField k₀ F₀) (hF₁ : IsFunctionField k₁ F₁) : different k₂ F₂ hF₀ = (conorm k₂ F₂) (different k₁ F₁ hF₀) + different k₂ F₂ hF₁

Different divisors are transitive in towers (Stichtenoth, Corollary 3.4.12): the different of F₂ / F₀ is the conorm of the different of F₁ / F₀, plus the different of F₂ / F₁.