The tame character of a place

Let F' / F be an extension of fields, k a subfield of F, and P a place of F' / k, and fix a uniformizer t at P. An automorphism σ in the inertia group G_0(P) moves t by a unit, σ t = u_σ t, and the value of u_σ at P is the tame character TauCeti.Place.tameCharacter : G_0(P) →* (F'_P)ˣ. Because σ acts trivially on the residue field, σ ↦ u_σ(P) is a homomorphism, and it does not depend on t. Its kernel consists of the automorphisms with σ t ≡ t modulo 𝔪_P², so it contains the first ramification group G_1(P).

When the residue extension F'_P / F_{P ∩ F} is separable, the kernel is exactly G_1(P): the value at P of a function z integral at P is a simple root of a polynomial over 𝒪_{P ∩ F}, and Taylor expansion of that polynomial at z shows that σ z ≡ z modulo 𝔪_P² as soon as σ t ≡ t. Then G_0(P) / G_1(P) embeds in the multiplicative group of the residue field, so when the inertia group is finite it is cyclic of order prime to the residue characteristic p. Since G_1(P) is a p-group (TauCeti.Place.isPGroup_ramificationGroup_succ), the place has no wild inertia exactly when p does not divide |G_0(P)|, which in a finite Galois extension is the ramification index.

This is part of Stichtenoth, Proposition 3.8.5, which is stated over a perfect constant field, so that all residue fields are perfect; here the only hypothesis is that the residue extension is separable. Without it the kernel of the tame character can be strictly larger than G_1(P). The analogous statements for nonarchimedean local fields are in TauCeti/NumberTheory/LocalField/UnitFiltration/RamificationGroup.lean.

Main definitions

• TauCeti.Place.tameCharacter: for a uniformizer t at P, the homomorphism σ ↦ (σ t / t)(P) from G_0(P) to the units of the residue field.
• TauCeti.Place.tameCharacterGraded: the induced homomorphism on G_0(P) / G_1(P).

Main results

• TauCeti.Place.tameCharacter_eq_of_ord_eq_one: the tame character does not depend on the uniformizer.
• TauCeti.Place.tameCharacter_eq_one_iff: σ lies in the kernel exactly when σ t ≡ t modulo 𝔪_P².
• TauCeti.Place.mem_ramificationGroup_one_iff: for a separable residue extension, an element of G_0(P) lies in G_1(P) exactly when it fixes a uniformizer modulo 𝔪_P².
• TauCeti.Place.ker_tameCharacter: for a separable residue extension, the kernel of the tame character is G_1(P).
• TauCeti.Place.tameCharacterGraded_injective: for a separable residue extension, the induced tame character on G_0(P) / G_1(P) is injective.
• TauCeti.Place.isCyclic_quotient_ramificationGroup_one and TauCeti.Place.not_dvd_index_ramificationGroup_one: for finite inertia and a separable residue extension, G_0(P) / G_1(P) is cyclic of order prime to the residue characteristic.
• TauCeti.Place.ramificationGroup_one_eq_bot_iff_not_dvd_card_ramificationGroup_zero: for finite inertia and a separable residue extension, the first ramification group is trivial exactly when the residue characteristic does not divide the order of the inertia group, and TauCeti.Place.ramificationGroup_one_eq_bot_iff_not_dvd_ramificationIdx its form for a finite Galois extension: no wild inertia exactly in the tame case.

References

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

noncomputable def TauCeti.Place.tameCharacter {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) : ↥(ramificationGroup F P 0) →* P.ResidueFieldˣ

The tame character (Stichtenoth, Proposition 3.8.5): for a uniformizer t at P, the homomorphism from the inertia group G_0(P) to the units of the residue field sending σ to the value at P of the unit σ t / t. It does not depend on t (TauCeti.Place.tameCharacter_eq_of_ord_eq_one), and its kernel contains G_1(P), with equality when the residue extension is separable (TauCeti.Place.ker_tameCharacter).

Equations

• TauCeti.Place.tameCharacter F P ht = MonoidHom.mk' (fun (g : ↥(TauCeti.Place.ramificationGroup F P 0)) => Units.mk0 ((IsLocalRing.residue ↥P.integers) ⟨↑↑g t * t⁻¹, ⋯⟩) ⋯) ⋯

theorem TauCeti.Place.coe_tameCharacter_of_eq {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) (g : ↥(ramificationGroup F P 0)) {y : ↥P.integers} (hy : ↑y = ↑↑g t * t⁻¹) : ↑((tameCharacter F P ht) g) = (IsLocalRing.residue ↥P.integers) y

The value of the tame character at σ, computed on any representative y of σ t / t in 𝒪_P.

theorem TauCeti.Place.tameCharacter_eq_one_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') {t : F'} (ht : P.ord t = 1) (g : ↥(ramificationGroup F P 0)) : (tameCharacter F P ht) g = 1 ↔ ↑↑g t - t ∈ P.filtration 2

The kernel of the tame character (Stichtenoth, Proposition 3.8.5): σ has trivial tame character exactly when it fixes the uniformizer t modulo 𝔪_P².

theorem TauCeti.Place.tameCharacter_eq_of_ord_eq_one {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 t' : F'} (ht : P.ord t = 1) (ht' : P.ord t' = 1) : tameCharacter F P ht = tameCharacter F P ht'

The tame character does not depend on the uniformizer.

theorem TauCeti.Place.ramificationGroup_one_subgroupOf_le_ker_tameCharacter {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) : (ramificationGroup F P 1).subgroupOf (ramificationGroup F P 0) ≤ (tameCharacter F P ht).ker

The tame character is trivial on the first ramification group: an automorphism moving every function integral at P by an element of 𝔪_P² in particular fixes t modulo 𝔪_P².

noncomputable def TauCeti.Place.tameCharacterGraded {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) : ↥(ramificationGroup F P 0) ⧸ (ramificationGroup F P 1).subgroupOf (ramificationGroup F P 0) →* P.ResidueFieldˣ

The tame character induced on G_0(P) / G_1(P). It is injective when the residue extension is separable (TauCeti.Place.tameCharacterGraded_injective).

Equations

• TauCeti.Place.tameCharacterGraded F P ht = QuotientGroup.lift ((TauCeti.Place.ramificationGroup F P 1).subgroupOf (TauCeti.Place.ramificationGroup F P 0)) (TauCeti.Place.tameCharacter F P ht) ⋯

@[simp]

theorem TauCeti.Place.tameCharacterGraded_mk {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) (g : ↥(ramificationGroup F P 0)) : (tameCharacterGraded F P ht) ↑g = (tameCharacter F P ht) g

The induced tame character evaluated on the class of an inertia automorphism.

theorem TauCeti.Place.tameCharacterGraded_eq_of_ord_eq_one {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 t' : F'} (ht : P.ord t = 1) (ht' : P.ord t' = 1) : tameCharacterGraded F P ht = tameCharacterGraded F P ht'

The induced tame character does not depend on the choice of uniformizer.

theorem TauCeti.Place.mem_ramificationGroup_one_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'] [Algebra.IsIntegral F F'] (P : Place k F') {t : F'} [Algebra.IsSeparable (restrict k F P).ResidueField P.ResidueField] (ht : P.ord t = 1) {g : ↥(ValuationSubring.decompositionSubgroup F P.integers)} (hg : g ∈ ramificationGroup F P 0) : g ∈ ramificationGroup F P 1 ↔ ↑g t - t ∈ P.filtration 2

Membership in the first ramification group is decided at a uniformizer, when the residue extension is separable (Stichtenoth, Proposition 3.8.5): an element of G_0(P) lies in G_1(P) exactly when it fixes t modulo 𝔪_P².

theorem TauCeti.Place.ker_tameCharacter {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'] [Algebra.IsIntegral F F'] (P : Place k F') {t : F'} [Algebra.IsSeparable (restrict k F P).ResidueField P.ResidueField] (ht : P.ord t = 1) : (tameCharacter F P ht).ker = (ramificationGroup F P 1).subgroupOf (ramificationGroup F P 0)

The kernel of the tame character is the first ramification group, when the residue extension is separable (Stichtenoth, Proposition 3.8.5): so G_0(P) / G_1(P) embeds in the multiplicative group of the residue field.

theorem TauCeti.Place.tameCharacterGraded_injective {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'] [Algebra.IsIntegral F F'] (P : Place k F') {t : F'} [Algebra.IsSeparable (restrict k F P).ResidueField P.ResidueField] (ht : P.ord t = 1) : Function.Injective ⇑(tameCharacterGraded F P ht)

The induced tame character is injective when the residue extension is separable.

theorem TauCeti.Place.isCyclic_quotient_ramificationGroup_one {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'] [Algebra.IsIntegral F F'] (P : Place k F') [Algebra.IsSeparable (restrict k F P).ResidueField P.ResidueField] [Finite ↥(ramificationGroup F P 0)] : IsCyclic (↥(ramificationGroup F P 0) ⧸ (ramificationGroup F P 1).subgroupOf (ramificationGroup F P 0))

The tame quotient G_0(P) / G_1(P) is cyclic when the inertia group is finite and the residue extension is separable (Stichtenoth, Proposition 3.8.5): it embeds in the multiplicative group of the residue field, whose finite subgroups are cyclic.

theorem TauCeti.Place.not_dvd_index_ramificationGroup_one {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'] [Algebra.IsIntegral F F'] (P : Place k F') (p : ℕ) [Fact (Nat.Prime p)] [CharP P.ResidueField p] [Algebra.IsSeparable (restrict k F P).ResidueField P.ResidueField] [Finite ↥(ramificationGroup F P 0)] : ¬p ∣ ((ramificationGroup F P 1).subgroupOf (ramificationGroup F P 0)).index

The index of G_1(P) in G_0(P) is prime to the residue characteristic p, when the inertia group is finite and the residue extension is separable (Stichtenoth, Proposition 3.8.5): G_0(P) / G_1(P) embeds in the multiplicative group of a field of characteristic p, which has no element of order p.

theorem TauCeti.Place.ramificationGroup_one_eq_bot_iff_not_dvd_card_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'] [Algebra.IsIntegral F F'] (P : Place k F') (p : ℕ) [Fact (Nat.Prime p)] [CharP P.ResidueField p] [Algebra.IsSeparable (restrict k F P).ResidueField P.ResidueField] [Finite ↥(ramificationGroup F P 0)] : ramificationGroup F P 1 = ⊥ ↔ ¬p ∣ Nat.card ↥(ramificationGroup F P 0)

A place has no wild inertia exactly when the residue characteristic p does not divide the order of its inertia group, when that group is finite and the residue extension is separable: G_1(P) is a p-group (TauCeti.Place.isPGroup_ramificationGroup_succ) of index prime to p.

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

A place of a finite Galois extension is tamely ramified exactly when it has no wild inertia, when the residue extension is separable: the first ramification group is trivial if and only if the residue characteristic p does not divide the ramification index.