The fundamental identity at an arbitrary place

Let F' / k' be an extension of the field extension F / k in which F' / F is finite; of the constant fields only integrality of k' / k is asked. This file proves the fundamental identity

∑_{P' ∣ P} e(P' ∣ P) · f(P' ∣ P) = [F' : F]

at every place P of F / k, upgrading the inequality of TauCeti/FieldTheory/FunctionField/Place/Extension/Fibre.lean and removing the restriction of TauCeti/FieldTheory/FunctionField/AffineModel/Extension.lean to the places of a chosen finite chart. It is proved in two forms, with incomparable hypotheses: for F' / F separable, and for F / k an algebraic function field with no separability.

Both reduce to the affine-model identity, which needs an affine model of F carrying P whose integral closure in F' is a finite module over it — the hypothesis of Mathlib's Ideal.sum_ramification_inertia_eq_finrank.

• For F' / F separable, the model is the valuation ring 𝒪_P itself, a discrete valuation ring with fraction field F: separability makes its integral closure in F' a finite 𝒪_P-module, by Mathlib's IsIntegralClosure.finite. No hypothesis on F / k is used. The local model is the one set up in TauCeti/FieldTheory/FunctionField/Place/Extension/Basic.lean; the action of 𝒪_P on F' and the scalar tower it sits in are not global instances, so they are reinstalled here.
• For F / k a function field, the model is the integral closure R_t of k[t] in F for a uniformizer t at P. As t has no pole at P, the place P lies on the finite chart of R_t; as t is transcendental, the integral closure of k[t] in the finite extension F' of k(t) is a finite k[t]-module with no separability hypothesis (TauCeti.IsIntegralClosure.finite_adjoin_of_transcendental), hence a finite R_t-module. The valuation ring 𝒪_P is not used as the model in this case: the integral closure of a discrete valuation ring in an inseparable extension need not be finite in general, and it is the finiteness of the normalization of k[t] that supplies finiteness here.

Main results

• TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isSeparable: the fundamental identity at an arbitrary place, for a separable extension (Stichtenoth, Theorem 3.1.11).
• TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isFunctionField: the fundamental identity at an arbitrary place of an algebraic function field, for any finite extension (Stichtenoth, Theorem 3.1.11, which assumes no separability).

References

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

theorem TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isSeparable (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.IsIntegral k k'] [Algebra.IsSeparable F F'] (P : Place k F) {s : Finset (Place k' F')} (hs : ∀ (P' : Place k' F'), P' ∈ s ↔ restrict k F P' = P) : ∑ P' ∈ s, ramificationIdx F P' * relativeDegree k F P' = Module.finrank F F'

The fundamental identity (Stichtenoth, Theorem 3.1.11) at an arbitrary place P of F / k, for an extension F' / k' whose extension of function fields F' / F is finite and separable: the ramification indices and relative degrees of the places of F' / k' lying over P satisfy ∑_{P' ∣ P} e(P' ∣ P) · f(P' ∣ P) = [F' : F].

The finite set s is the fibre of TauCeti.Place.restrict over P, which is finite by TauCeti.Place.finite_setOf_restrict_eq.

Separability is the hypothesis of Mathlib's finiteness theorem for integral closures, and is used only there. When F / k is an algebraic function field the identity holds for every finite extension; that is TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isFunctionField.

theorem TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isFunctionField (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.IsIntegral k k'] (hF : IsFunctionField k F) (P : Place k F) {s : Finset (Place k' F')} (hs : ∀ (P' : Place k' F'), P' ∈ s ↔ restrict k F P' = P) : ∑ P' ∈ s, ramificationIdx F P' * relativeDegree k F P' = Module.finrank F F'

The fundamental identity (Stichtenoth, Theorem 3.1.11) at an arbitrary place P of an algebraic function field F / k, for an extension F' / k' whose extension of function fields F' / F is finite, with no separability hypothesis: the ramification indices and relative degrees of the places of F' / k' lying over P satisfy ∑_{P' ∣ P} e(P' ∣ P) · f(P' ∣ P) = [F' : F].

The finite set s is the fibre of TauCeti.Place.restrict over P, which is finite by TauCeti.Place.finite_setOf_restrict_eq.

For a separable F' / F the identity holds without assuming that F / k is a function field; that is TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isSeparable.