Function-field and local-ring ramification groups

The lower ramification groups of a place are the generic local-ring ramification filtration of its valuation ring. More precisely, for a place P of F' / k over F, this file identifies

Place.ramificationGroup F P i

with IsLocalRing.ramificationGroup (P.integers.decompositionSubgroup F) P.integers i. The comparison rests on the equality between the place filtration and powers of the maximal ideal of P.integers.

The decomposition group acts faithfully on the valuation ring: agreement there implies agreement on its fraction field. Consequently, after rewriting along the comparison, the generic lower index (IsLocalRing.mem_ramificationGroup_iff_le_lowerIndex) and Hilbert counting identity (IsLocalRing.sum_addVal_smul_sub_eq_finsum_card_ramificationGroup_sub_one) apply directly to the function-field groups.

Main results

• TauCeti.Place.ramificationGroup_eq_isLocalRing_ramificationGroup: the two lower ramification filtrations agree.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Theorem 3.8.7.
• J.-P. Serre, Local Fields, Chapter IV, Section 1.

theorem TauCeti.Place.ramificationGroup_eq_isLocalRing_ramificationGroup {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'] (P : Place k F') (i : ℕ) : ramificationGroup F P i = IsLocalRing.ramificationGroup ↥(ValuationSubring.decompositionSubgroup F P.integers) ↥P.integers ↑i

The lower ramification groups defined using the order filtration of the function field are the generic local-ring ramification groups of the valuation ring.