Positive ramification groups are p-groups

For a place in residue characteristic p, every successive quotient of the positive ramification filtration has exponent p. When the inertia group is finite, the filtration eventually reaches the trivial group. Iterating the quotient statement shows that every element of a positive ramification group has p-power order, so the whole group is a p-group. In particular, the first positive group is the wild inertia group.

This is the group-theoretic conclusion of Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 3.8.5. It uses no perfectness assumption on the residue field.

theorem TauCeti.Place.isPGroup_ramificationGroup_succ {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') (p i : ℕ) [CharP P.ResidueField p] [Finite ↥(ramificationGroup F P 0)] : IsPGroup p ↥(ramificationGroup F P (i + 1))

Every positive ramification group of a finite inertia group is a p-group in residue characteristic p. This includes the wild inertia group G₁.

theorem TauCeti.Place.ramificationGroup_succ_eq_bot_of_not_dvd_card_inertia {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') (p i : ℕ) [Fact (Nat.Prime p)] [CharP P.ResidueField p] [Finite ↥(ramificationGroup F P 0)] (hp : ¬p ∣ Nat.card ↥(ramificationGroup F P 0)) : ramificationGroup F P (i + 1) = ⊥

If the residue characteristic does not divide the order of inertia, every positive ramification group is trivial. In a finite Galois extension with separable residue extension, the order of inertia is the ramification index, so this is the tame case.

theorem TauCeti.Place.ramificationGroup_succ_eq_bot_of_tame {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') (p i : ℕ) [Fact (Nat.Prime p)] [CharP P.ResidueField p] [FiniteDimensional F F'] [IsGalois F F'] [Algebra.IsSeparable (restrict k F P).ResidueField P.ResidueField] (hp : ¬p ∣ ramificationIdx F P) : ramificationGroup F P (i + 1) = ⊥

Tame ramification has no wild inertia: in a finite Galois extension with separable residue extension, if the residue characteristic does not divide the ramification index, every positive ramification group is trivial.