The local conductor–discriminant formula

Let L/K be a finite abelian extension of nonarchimedean local fields with group G and lower ramification groups G_i, and let f(χ) be the Artin conductor exponent of a character χ of G (TauCeti.LocalFieldsRamification.artinConductorExponent). Serre's formula f(χ) · #G_0 = ∑_{i ≥ 0, χ(G_i) ≠ 1} #G_i expresses it through the lower ramification groups. Summing over the characters χ : G → Mˣ (with M having enough roots of unity, for instance M = ℂ) and counting, for each i, the #G - #G/#G_i characters that are nontrivial on G_i, Hilbert's formula d(L/K) = ∑_{i ≥ 0} (#G_i - 1) and #G = e f give the local conductor–discriminant formula

∑_χ f(χ) = f(L/K) d(L/K) = δ(L/K),

where δ(L/K) is the discriminant exponent. This is the local input to the conductor–discriminant formula for a global abelian extension, read at the completions.

Main results

• TauCeti.LocalFieldsRamification.finsum_artinConductorExponent_eq_discriminantExponent: the local conductor–discriminant formula ∑_χ f(χ) = δ(L/K) for an abelian extension.

References

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

theorem TauCeti.LocalFieldsRamification.finsum_artinConductorExponent_eq_discriminantExponent (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) [CommMonoid M] [HasEnoughRootsOfUnity M (Monoid.exponent Gal(L/K))] : ∑ᶠ (χ : Gal(L/K) →* Mˣ), artinConductorExponent K L χ = discriminantExponent K L

The local conductor–discriminant formula. For a finite abelian extension L/K of nonarchimedean local fields and a commutative monoid M with enough roots of unity (for instance M = ℂ), the Artin conductor exponents of the characters χ : Gal(L/K) →* Mˣ add up to the discriminant exponent: ∑_χ f(χ) = δ(L/K).