Local ramification data and weighted partitions

For a finite extension of fields, TauCeti.Place.localData records the pair consisting of the ramification index and the relative residue degree at each place above a fixed place. For an algebraic function field, repeating each index by its residue degree gives a partition of the extension degree. If all residue degrees are one, its parts are the unweighted ramification indices; this applies in particular over algebraically closed constants. The local data depend only on the fibre with its ramification indices and relative degrees, so a bijection of fibres preserving both identifies them (TauCeti.Place.localData_eq_of_equiv).

The finite fibre and the sum of products are supplied by TauCeti.Place.finite_setOf_restrict_eq and TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isFunctionField. The partition uses Mathlib's Nat.Partition without discarding residue degrees.

References

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

noncomputable def TauCeti.Place.localData (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) : Multiset (ℕ × ℕ)

The local pairs (e, f) at the places above P, with one entry per place, retaining multiplicity when different places have the same invariants.

theorem TauCeti.Place.localData_def (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) : localData k F P = Multiset.map (fun (P' : Place k' F') => (ramificationIdx F P', relativeDegree k F P')) ⋯.toFinset.val

The local data are the ramification and relative residue degrees on the finite fibre.

@[simp]

theorem TauCeti.Place.mem_localData (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} {ef : ℕ × ℕ} : ef ∈ localData k F P ↔ ∃ (P' : Place k' F'), restrict k F P' = P ∧ (ramificationIdx F P', relativeDegree k F P') = ef

A pair occurs exactly when it is realized by a place above P.

@[simp]

theorem TauCeti.Place.card_localData (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) : (localData k F P).card = {P' : Place k' F' | restrict k F P' = P}.ncard

The number of local-data entries is the number of places above P.

theorem TauCeti.Place.localData_eq_of_equiv {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'] {l : Type u_1} {l' : Type u_2} {L : Type u_3} {L' : Type u_4} [Field l] [Field l'] [Field L] [Field L'] [Algebra l l'] [Algebra l L] [Algebra l' L'] [Algebra L L'] [Algebra l L'] [IsScalarTower l l' L'] [IsScalarTower l L L'] [FiniteDimensional L L'] (P : Place k F) (Q : Place l L) (Φ : Place k' F' ≃ Place l' L') (hΦ : ∀ (P' : Place k' F'), restrict l L (Φ P') = Q ↔ restrict k F P' = P) (he : ∀ (P' : Place k' F'), restrict k F P' = P → ramificationIdx L (Φ P') = ramificationIdx F P') (hf : ∀ (P' : Place k' F'), restrict k F P' = P → relativeDegree l L (Φ P') = relativeDegree k F P') : localData l L Q = localData k F P

Local data are invariant under a matching of fibres: a bijection between the places of F' and those of L' carrying the places above P onto the places above Q, with the same ramification indices and relative degrees, identifies the local data at Q with those at P. Transport along an isomorphism of extensions, or along a substitution of the base field, provides such a bijection.

theorem TauCeti.Place.sum_mul_localData (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) : (Multiset.map (fun (ef : ℕ × ℕ) => ef.1 * ef.2) (localData k F P)).sum = Module.finrank F F'

The fundamental identity expressed in the local-data multiset.

noncomputable def TauCeti.Place.weightedRamificationPartition (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) : (Module.finrank F F').Partition

The partition of [F' : F] in which the ramification index at a place above P occurs as many times as its relative residue degree. Unlike the unweighted indices, these parts sum to the extension degree without any rationality assumption on the places.

theorem TauCeti.Place.parts_weightedRamificationPartition (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) : (weightedRamificationPartition k F hF P).parts = (localData k F P).bind fun (ef : ℕ × ℕ) => Multiset.replicate ef.2 ef.1

The parts are obtained by repeating each ramification index by its relative residue degree.

@[simp]

theorem TauCeti.Place.mem_parts_weightedRamificationPartition (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} {e : ℕ} : e ∈ (weightedRamificationPartition k F hF P).parts ↔ ∃ (P' : Place k' F'), restrict k F P' = P ∧ ramificationIdx F P' = e

A part is precisely a ramification index realized above P. Multiplicities are specified by parts_weightedRamificationPartition, not by this membership statement.

theorem TauCeti.Place.card_parts_weightedRamificationPartition (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) : (weightedRamificationPartition k F hF P).parts.card = (Multiset.map Prod.snd (localData k F P)).sum

The number of weighted parts is the sum of the relative residue degrees.

theorem TauCeti.Place.parts_weightedRamificationPartition_of_relativeDegree_eq_one (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) (hf : ∀ (P' : Place k' F'), restrict k F P' = P → relativeDegree k F P' = 1) : (weightedRamificationPartition k F hF P).parts = Multiset.map Prod.fst (localData k F P)

When every place above P has relative residue degree one, the partition consists of the unweighted ramification indices, one per place.

theorem TauCeti.Place.parts_weightedRamificationPartition_of_isAlgClosed (k : Type u) (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [IsAlgClosed k] (hF : IsFunctionField k F) (P : Place k F) : (weightedRamificationPartition k F hF P).parts = Multiset.map Prod.fst (localData k F P)

Over algebraically closed constants the weighted partition is the unweighted multiset of ramification indices.