Towers of extensions of places

Restriction of places is functorial through a tower of algebraic field extensions. The ramification index and relative residue degree are multiplicative in the same tower. These are the tower statements in Stichtenoth, Algebraic Function Fields and Codes, Proposition 3.1.6.

The constants are allowed to grow with the function fields. Thus the setup contains parallel towers k₀ → k₁ → k₂ and F₀ → F₁ → F₂, with each Fᵢ an algebra over kᵢ and the expected commuting scalar towers. No function-field, finite-dimensionality, separability, or perfectness hypothesis is needed: restriction uses only integrality of the field extensions, and the degree identity is the ordinary finrank tower formula for the residue fields.

Main results

• TauCeti.Place.restrict_restrict: restricting first to F₁ and then to F₀ agrees with restricting directly to F₀.
• TauCeti.Place.ramificationIdx_restrict_mul: ramification indices multiply in a tower.
• TauCeti.Place.relativeDegree_restrict_mul: relative residue degrees multiply in a tower.

Mathematical context

Multiplicativity in towers for extensions of places is Stichtenoth, Proposition 3.1.6. The restriction identity also supplies the functoriality needed to define induced places and to construct dual isogenies.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.1.6.

@[simp]

theorem TauCeti.Place.restrict_restrict {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₂] [Algebra.IsIntegral F₀ F₁] [Algebra.IsIntegral F₁ F₂] (P : Place k₂ F₂) : restrict k₀ F₀ (restrict k₁ F₁ P) = restrict k₀ F₀ P

Restriction of places is functorial in a tower: restricting a place of F₂ / k₂ first to F₁ / k₁ and then to F₀ / k₀ gives its direct restriction to F₀ / k₀.

This is the normalized-place form of transitivity of valuation restriction.

theorem TauCeti.Place.ramificationIdx_restrict_mul {k₁ : Type u₁} {k₂ : Type u₂} {F₀ : Type v₀} {F₁ : Type v₁} {F₂ : Type v₂} [Field k₁] [Field k₂] [Field F₀] [Field F₁] [Field F₂] [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₂] [IsScalarTower k₁ k₂ F₂] [IsScalarTower k₁ F₁ F₂] [Algebra.IsIntegral F₁ F₂] (P : Place k₂ F₂) : ramificationIdx F₀ P = ramificationIdx F₁ P * ramificationIdx F₀ (restrict k₁ F₁ P)

Ramification indices are multiplicative in towers (Stichtenoth, Proposition 3.1.6): e(P₂ / F₀) = e(P₂ / F₁) e(P₂|F₁ / F₀). Only F₂ / F₁ needs to be algebraic; the restrictions to F₀ may be trivial, in which case both corresponding indices vanish.

theorem TauCeti.Place.relativeDegree_restrict_mul {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₂] [Algebra.IsIntegral F₀ F₁] [Algebra.IsIntegral F₁ F₂] (P : Place k₂ F₂) : relativeDegree k₀ F₀ P = relativeDegree k₁ F₁ P * relativeDegree k₀ F₀ (restrict k₁ F₁ P)

Relative residue degrees are multiplicative in towers (Stichtenoth, Proposition 3.1.6): f(P₂ / P₀) = f(P₂ / P₁) f(P₁ / P₀) for the restrictions P₁ and P₀ of P₂.