The places lying over a fixed place: the fundamental inequality

Let F' / k' be a finite extension of the field extension F / k. Every place of F' / k' restricts to a place of F / k (TauCeti.Place.restrict), and the places over a fixed place P of F / k form the fibre of that map. This file bounds that fibre: for any finite family of distinct places over P,

∑ e(P' ∣ P) · f(P' ∣ P) ≤ [F' : F],

the fundamental inequality, one half of Stichtenoth's fundamental identity. Since each summand is at least 1, the fibre is finite and has at most [F' : F] elements.

The bound at a single place, e · f ≤ [F' : F], is TauCeti.Place.ramificationIdx_mul_relativeDegree_le_finrank, proved by exhibiting e · f elements of F' independent over F. The passage to several places is weak approximation: the e · f witnesses attached to a place Q of the family are replaced by functions agreeing with them to first order at Q and vanishing to order [F' : F] at every other place of the family, so the blocks belonging to different places cannot interfere. Normalizing the coefficients of a hypothetical relation by one of least order at P — which is where the places of the fibre being restrictions of the same P is used — makes one block a unit multiple of a power of a prime element, hence of order less than its ramification index, while every other block has order at least [F' : F]; the strict triangle inequality then forbids the relation.

Main results

• TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_le_finrank: the fundamental inequality (Stichtenoth, Theorem 3.1.11).
• TauCeti.Place.finite_setOf_restrict_eq: a place of F / k has only finitely many extensions to F' / k' (Stichtenoth, Proposition 3.1.7).
• TauCeti.Place.ncard_setOf_restrict_eq_le_finrank: it has at most [F' : F] of them (Stichtenoth, Corollary 3.1.12).

References

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

theorem TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_le_finrank (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'] (P : Place k F) (s : Finset (Place k' F')) (hs : ∀ P' ∈ s, restrict k F P' = P) : ∑ P' ∈ s, ramificationIdx F P' * relativeDegree k F P' ≤ Module.finrank F F'

The fundamental inequality (Stichtenoth, Theorem 3.1.11): the ramification indices and relative degrees of finitely many distinct places of F' / k' lying over one place P of F / k satisfy ∑ e(P' ∣ P) · f(P' ∣ P) ≤ [F' : F].

The reverse inequality — the fundamental identity — is not proved here; it is the affine-model reconciliation with Ideal.sum_ramification_inertia.

theorem TauCeti.Place.finite_setOf_restrict_eq (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'] (P : Place k F) : {P' : Place k' F' | restrict k F P' = P}.Finite

A place has only finitely many extensions (Stichtenoth, Proposition 3.1.7): the fibre of TauCeti.Place.restrict over a place of F / k is finite, because each of its members contributes at least 1 to the fundamental inequality.

instance TauCeti.Place.finite_restrict_eq (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'] (P : Place k F) : Finite { P' : Place k' F' // restrict k F P' = P }

The subtype of places lying over a given place is finite, so a consumer may sum over it.

theorem TauCeti.Place.ncard_setOf_restrict_eq_le_finrank (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'] (P : Place k F) : {P' : Place k' F' | restrict k F P' = P}.ncard ≤ Module.finrank F F'

A place has at most [F' : F] extensions (Stichtenoth, Corollary 3.1.12).