The higher ramification groups of a place

Let F' / F be an extension of fields, k a subfield of F, and P a place of F' / k. An automorphism of F' over F fixing P acts on the valuation ring 𝒪_P, and the i-th ramification group of P collects those automorphisms whose action on 𝒪_P is the identity to order i + 1:

G_i(P) = {σ ∈ G_Z(P) | ord_P (σ z - z) ≥ i + 1 for every z ∈ 𝒪_P}.

At i = 0 this is the condition that σ act trivially on the residue field, so G_0(P) is the inertia group; the groups then decrease, are normal in the decomposition group, and meet in the trivial group. This is the lower numbering, and no completion is taken: the condition is read off the order filtration of F' at P built in TauCeti/FieldTheory/FunctionField/Place/Filtration.lean.

The structure of the successive quotients comes from a single map. Fix a uniformizer t at P. For σ ∈ G_{i+1}(P) the function z ↦ (σ z - z) / t^{i+2} takes values in 𝒪_P, and reducing it at P gives a function 𝒪_P → F'_P; the resulting TauCeti.Place.ramificationResidueHom is a group homomorphism from G_{i+1}(P) to the additive group of such functions, and its kernel is exactly G_{i+2}(P). Its being a homomorphism is where the hypothesis i + 1 ≥ 1 enters: an automorphism in G_1(P) moves t by a unit congruent to 1 at P, and one in G_0(P) does not move residues at all, so the two error terms produced by expanding (στ) z - z disappear on reduction.

Consequently every quotient G_{i+1}(P) / G_{i+2}(P) embeds in the additive group of functions from 𝒪_P to the residue field: it is abelian, and in characteristic p it is killed by p, while in characteristic zero it is torsion-free. When G_1(P) is finite the last statement forces G_{i+1}(P) = G_{i+2}(P) for every i, and hence — the groups meeting in 1 — G_1(P) is trivial.

This is Stichtenoth, Definition 3.8.4 and Proposition 3.8.5. Nothing here consumes perfectness of the residue fields; the complementary statement that G_0(P) / G_1(P) is cyclic of order prime to the characteristic needs the residue extension to be separable, and is proved in TauCeti/FieldTheory/FunctionField/Place/Extension/TameInertia.lean.

Main definitions

• TauCeti.Place.ramificationGroup: the i-th ramification group of a place, a subgroup of the decomposition group, with TauCeti.Place.mem_ramificationGroup_iff for its membership.
• TauCeti.Place.ramificationResidueHom: for a uniformizer t at P, the homomorphism σ ↦ (z ↦ ((σ z - z) / t^{i+2})(P)) from G_{i+1}(P) to the additive group of functions 𝒪_P → F'_P.

Main results

• TauCeti.Place.ramificationGroup_zero: the 0-th ramification group is the inertia group.
• TauCeti.Place.ramificationGroup_antitone, TauCeti.Place.normal_ramificationGroup: the ramification groups decrease and are normal in the decomposition group.
• TauCeti.Place.iInf_ramificationGroup_eq_bot and TauCeti.Place.exists_forall_ramificationGroup_eq_bot: the ramification groups meet in the trivial group, and, when G_0(P) is finite, are trivial from some index on.
• TauCeti.Place.ker_ramificationResidueHom: the kernel of the ramification residue is the next ramification group, so G_{i+1}(P) / G_{i+2}(P) embeds in an additive group of functions to the residue field.
• TauCeti.Place.commutator_ramificationGroup_le and TauCeti.Place.pow_mem_ramificationGroup_of_charP: the quotient G_{i+1}(P) / G_{i+2}(P) is abelian, and elementary abelian of exponent p in characteristic p.
• TauCeti.Place.ramificationGroup_one_eq_bot: in characteristic zero the first ramification group of a place is trivial when it is finite.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definition 3.8.4 and Proposition 3.8.5.

theorem TauCeti.Place.mem_filtration_decompositionSubgroup_apply {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') (g : ↥(ValuationSubring.decompositionSubgroup F P.integers)) {a : ℤ} {x : F'} : ↑g x ∈ P.filtration a ↔ x ∈ P.filtration a

An automorphism fixing P preserves every step of the order filtration at P.

def TauCeti.Place.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 : ℕ) : Subgroup ↥(ValuationSubring.decompositionSubgroup F P.integers)

The i-th ramification group of a place (Stichtenoth, Definition 3.8.4): the automorphisms in the decomposition group of P that move every function integral at P by something of order at least i + 1. This is the lower numbering.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Place.mem_ramificationGroup_iff {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 : ℕ} {g : ↥(ValuationSubring.decompositionSubgroup F P.integers)} : g ∈ ramificationGroup F P i ↔ ∀ x ∈ P.integers, ↑g x - x ∈ P.filtration (↑i + 1)

Membership in the i-th ramification group (Stichtenoth, Definition 3.8.4).

@[simp]

theorem TauCeti.Place.ramificationGroup_zero {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') : ramificationGroup F P 0 = ValuationSubring.inertiaSubgroup F P.integers

The 0-th ramification group is the inertia group (Stichtenoth, Definition 3.8.4): acting trivially on the residue field is acting trivially to order 1 on the valuation ring.

theorem TauCeti.Place.ramificationGroup_antitone {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') : Antitone (ramificationGroup F P)

The ramification groups decrease: vanishing to higher order is a stronger condition.

theorem TauCeti.Place.ramificationGroup_le_inertiaSubgroup {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 ≤ ValuationSubring.inertiaSubgroup F P.integers

Every ramification group sits inside the inertia group.

instance TauCeti.Place.normal_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).Normal

The ramification groups are normal in the decomposition group (Stichtenoth, Proposition 3.8.5).

theorem TauCeti.Place.iInf_ramificationGroup_eq_bot {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 = ⊥

The ramification groups meet in the trivial group (Stichtenoth, Proposition 3.8.5): an automorphism fixing every function integral at P to every order is the identity, because the valuation ring of P has F' for its field of fractions.

theorem TauCeti.Place.exists_forall_ramificationGroup_eq_bot {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') [Finite ↥(ramificationGroup F P 0)] : ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → ramificationGroup F P i = ⊥

The ramification groups of a place whose inertia group is finite are trivial from some index on (Stichtenoth, Proposition 3.8.5).

noncomputable def TauCeti.Place.ramificationResidueHom {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') {t : F'} (ht : P.ord t = 1) (i : ℕ) : ↥(ramificationGroup F P (i + 1)) →* Multiplicative (↥P.integers → P.ResidueField)

The ramification residue (Stichtenoth, Proposition 3.8.5): for a uniformizer t at P, the map sending an automorphism σ of G_{i+1}(P) to the function z ↦ ((σ z - z)/t^{i+2})(P) on 𝒪_P. It is a homomorphism into the additive group of functions 𝒪_P → F'_P, which is therefore written multiplicatively here. The map depends on the choice of t; its kernel, TauCeti.Place.ker_ramificationResidueHom, does not.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Place.toAdd_ramificationResidueHom_apply {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') {t : F'} (ht : P.ord t = 1) (i : ℕ) (g : ↥(ramificationGroup F P (i + 1))) (x y : ↥P.integers) (hy : ↑y = (t ^ (i + 2))⁻¹ * (↑↑g ↑x - ↑x)) : Multiplicative.toAdd ((ramificationResidueHom F P ht i) g) x = (IsLocalRing.residue ↥P.integers) y

The value of the ramification residue at a function x integral at P, computed on any representative y of (σ x - x)/t^{i+2} in 𝒪_P.

theorem TauCeti.Place.ker_ramificationResidueHom {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') {t : F'} (ht : P.ord t = 1) (i : ℕ) : (ramificationResidueHom F P ht i).ker = (ramificationGroup F P (i + 2)).subgroupOf (ramificationGroup F P (i + 1))

The kernel of the ramification residue is the next ramification group (Stichtenoth, Proposition 3.8.5): so G_{i+1}(P) / G_{i+2}(P) embeds into the additive group of functions from 𝒪_P to the residue field at P.

theorem TauCeti.Place.commutator_ramificationGroup_le {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 + 1), ramificationGroup F P (i + 1)⁆ ≤ ramificationGroup F P (i + 2)

The successive quotients of the ramification filtration are abelian (Stichtenoth, Proposition 3.8.5): a commutator of G_{i+1}(P) lies in G_{i+2}(P).

theorem TauCeti.Place.pow_mem_ramificationGroup_of_charP {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 : ℕ) [CharP P.ResidueField p] (i : ℕ) {g : ↥(ValuationSubring.decompositionSubgroup F P.integers)} (hg : g ∈ ramificationGroup F P (i + 1)) : g ^ p ∈ ramificationGroup F P (i + 2)

In characteristic p the successive quotients of the ramification filtration are killed by p (Stichtenoth, Proposition 3.8.5): the p-th power of an element of G_{i+1}(P) lies in G_{i+2}(P), so G_{i+1}(P) / G_{i+2}(P) is elementary abelian.

theorem TauCeti.Place.ramificationGroup_one_eq_bot {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') [Finite ↥(ramificationGroup F P 1)] [CharZero P.ResidueField] : ramificationGroup F P 1 = ⊥

In characteristic zero a finite first ramification group is trivial (Stichtenoth, Proposition 3.8.5): each successive quotient embeds in a torsion-free additive group, so the filtration is constant from 1 on and meets in 1.