The Artin conductor exponent

Let L/K be a finite Galois extension of nonarchimedean local fields with group G and upper ramification groups G^v. The Artin conductor exponent f(χ) of a homomorphism χ : G → M is the least natural number n with G^n ⊆ ker χ. It is 0 exactly when χ is unramified, that is trivial on the inertia group G^0 = G_0.

For L/K abelian the Hasse–Arf theorem makes every upper break an integer. This turns the definition into Serre's formula for the conductor of a one-dimensional character in terms of the lower ramification groups G_i,

f(χ) · #G_0 = ∑_{i ≥ 0, χ(G_i) ≠ 1} #G_i,

since the last lower index t with χ(G_t) ≠ 1 sits at the upper index φ(t) = (#G_1 + ⋯ + #G_t) / #G_0, an integer by Hasse–Arf, and f(χ) = φ(t) + 1.

Main definitions

• TauCeti.LocalFieldsRamification.artinConductorExponent K L χ: the least n : ℕ such that χ is trivial on the upper ramification group G^n.

Main results

• TauCeti.LocalFieldsRamification.artinConductorExponent_le_iff: f(χ) ≤ n exactly when G^n ⊆ ker χ.
• TauCeti.LocalFieldsRamification.artinConductorExponent_eq_zero_iff: f(χ) = 0 exactly when χ is trivial on G_0.
• TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_eq_sum_range: Serre's formula for an abelian extension, as a sum over i < n for any n with χ(G_n) = 1.
• TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_lowerRamificationGroup_zero: Serre's formula f(χ) · #G_0 = ∑_{i ≥ 0, χ(G_i) ≠ 1} #G_i for an abelian extension.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §3, Chapter V, §7 and Chapter VI, §2.
• J. Neukirch, Algebraic Number Theory, Chapter VII, §11.

noncomputable def TauCeti.LocalFieldsRamification.artinConductorExponent (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) : ℕ

The Artin conductor exponent of a homomorphism χ on the Galois group of a finite Galois extension of local fields: the least natural number n such that χ is trivial on the upper ramification group G^n. The minimum is attained (upperRamificationGroup_artinConductorExponent_le_ker).

theorem TauCeti.LocalFieldsRamification.upperRamificationGroup_artinConductorExponent_le_ker (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) : upperRamificationGroup K L ⟨↑(artinConductorExponent K L χ), ⋯⟩ ≤ χ.ker

The Artin conductor exponent is attained: χ is trivial on G^{f(χ)}.

theorem TauCeti.LocalFieldsRamification.artinConductorExponent_le_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) {n : ℕ} : artinConductorExponent K L χ ≤ n ↔ upperRamificationGroup K L ⟨↑n, ⋯⟩ ≤ χ.ker

The characterizing property of the Artin conductor exponent: it is at most n exactly when χ is trivial on the upper ramification group G^n.

theorem TauCeti.LocalFieldsRamification.artinConductorExponent_le_iff_lowerRamificationGroup_psiNat_le (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) {n : ℕ} : artinConductorExponent K L χ ≤ n ↔ lowerRamificationGroup K L ↑(psiNat K L n) ≤ χ.ker

The Artin conductor exponent is at most n exactly when χ is trivial on the lower ramification group G_{ψ(n)}.

@[simp]

theorem TauCeti.LocalFieldsRamification.artinConductorExponent_eq_zero_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) : artinConductorExponent K L χ = 0 ↔ lowerRamificationGroup K L 0 ≤ χ.ker

A homomorphism has Artin conductor exponent 0 exactly when it is unramified, that is, trivial on the inertia group G_0.

Abelian extensions

theorem TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_eq_sum_range (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsAbelianGalois K L] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) {n : ℕ} (hn : lowerRamificationGroup K L ↑n ≤ χ.ker) [DecidablePred fun (i : ℕ) => lowerRamificationGroup K L ↑i ≤ χ.ker] : artinConductorExponent K L χ * Nat.card ↥(lowerRamificationGroup K L 0) = ∑ i ∈ Finset.range n, if lowerRamificationGroup K L ↑i ≤ χ.ker then 0 else Nat.card ↥(lowerRamificationGroup K L ↑i)

Serre's formula for the Artin conductor, truncated at any index n at which χ is trivial on G_n: for a finite abelian extension of local fields, f(χ) · #G_0 = ∑_{i < n, χ(G_i) ≠ 1} #G_i.

theorem TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_lowerRamificationGroup_zero (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsAbelianGalois K L] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) : artinConductorExponent K L χ * Nat.card ↥(lowerRamificationGroup K L 0) = ∑ᶠ (i : ℕ) (_ : ¬lowerRamificationGroup K L ↑i ≤ χ.ker), Nat.card ↥(lowerRamificationGroup K L ↑i)

Serre's formula for the Artin conductor of a homomorphism on the Galois group of a finite abelian extension of local fields: f(χ) · #G_0 = ∑_{i ≥ 0, χ(G_i) ≠ 1} #G_i.