The degree of a place over the place below it

Let F' / F be an algebraic extension of fields, both with the same field of constants k, and let P' be a place of F' / k lying over the place P = P'|_F of F / k. The residue fields then form a tower k ⊆ F_P ⊆ F'_{P'}, so the multiplicativity of Module.finrank reads

deg P' = deg P · f(P' ∣ P).

This is the same-constant-field case of Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Corollary 3.1.14, where the general form is cross-multiplied as [k' : k] · deg P' = deg P · f(P' ∣ P). The extra factor cannot be written here: the residue field of a place of F' / k' is a k'-algebra, and the k-algebra structure needed to speak of Module.finrank k F'_{P'} at all comes with the constant-field extension theory.

Main results

• TauCeti.Place.degree_eq_degree_restrict_mul_relativeDegree: deg P' = deg P · f(P' ∣ P).
• TauCeti.Place.degree_restrict_le: hence deg P ≤ deg P', the form consumed when a finiteness statement about places of F is transported to F'.
• TauCeti.Place.relativeDegree_eq_one_of_isSepClosed: a separable extension of a separably closed residue field has relative degree 1.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.1.

instance TauCeti.Place.instIsScalarTowerIntegers (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'] [Algebra.IsIntegral F F'] (P' : Place k F') : IsScalarTower k ↥(restrict k F P').integers ↥P'.integers

The constants act on the valuation ring of P' through the valuation ring of the place below it, so the residue fields inherit a tower over k.

theorem TauCeti.Place.degree_eq_degree_restrict_mul_relativeDegree (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'] [Algebra.IsIntegral F F'] (P' : Place k F') : P'.degree = (restrict k F P').degree * relativeDegree k F P'

The degree of a place over the place below it (Stichtenoth, Corollary 3.1.14 in the same-constant-field case): deg P' = deg P · f(P' ∣ P), by multiplicativity of finrank along the tower of residue fields k ⊆ F_P ⊆ F'_{P'}.

@[simp]

theorem TauCeti.Place.relativeDegree_eq_one_of_isSepClosed (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'] [Algebra.IsIntegral F F'] (P' : Place k F') [IsSepClosed (restrict k F P').ResidueField] [Algebra.IsSeparable (restrict k F P').ResidueField P'.ResidueField] : relativeDegree k F P' = 1

A separable extension of a separably closed residue field has relative degree 1.

theorem TauCeti.Place.degree_restrict_le (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'] [Algebra.IsIntegral F F'] (P' : Place k F') [FiniteDimensional F F'] : (restrict k F P').degree ≤ P'.degree

A place is at least as large as the place below it: deg P ≤ deg P'. Finiteness of the extension guards the junk value of the relative degree.