Tame ramification and the global different exponent

At a finite prime w over v of a number-field extension, the coefficient of the different equals e(w/v) - 1 exactly when the canonical completed extension L_w / K_v is tamely ramified, and it is at least e(w/v) exactly when L_w / K_v is wildly ramified. These criteria read tame and wild ramification of the completed extension directly from the global different exponent. For L/K Galois, the tame criterion is also read on the global wild inertia group: the first ramification group G_1 of w is trivial exactly when the different exponent at w is e(w/v) - 1.

References

• J. Neukirch, Algebraic Number Theory, Chapter III, Theorem 2.6.
• J.-P. Serre, Local Fields, Chapter III, §6, Proposition 13.

theorem IsDedekindDomain.HeightOneSpectrum.multiplicity_differentIdeal_eq_ramificationIdx_sub_one_iff_isTamelyRamified {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : multiplicity w.asIdeal (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) = w.asIdeal.ramificationIdx (NumberField.RingOfIntegers K) - 1 ↔ TauCeti.IsTamelyRamified (adicCompletion K v) (adicCompletion L w)

The global different exponent at w is e(w/v) - 1 precisely when the canonical completed extension is tamely ramified.

theorem IsDedekindDomain.HeightOneSpectrum.ramificationIdx_le_multiplicity_differentIdeal_iff_isWildlyRamified {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : w.asIdeal.ramificationIdx (NumberField.RingOfIntegers K) ≤ multiplicity w.asIdeal (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) ↔ TauCeti.IsWildlyRamified (adicCompletion K v) (adicCompletion L w)

The global different exponent at w is at least e(w/v) precisely when the canonical completed extension is wildly ramified.

theorem IsDedekindDomain.HeightOneSpectrum.ramificationGroup_one_eq_bot_iff_multiplicity_differentIdeal_eq {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsGalois K L] : Ideal.ramificationGroup Gal(L/K) w.asIdeal 1 = ⊥ ↔ multiplicity w.asIdeal (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) = w.asIdeal.ramificationIdx (NumberField.RingOfIntegers K) - 1

For L/K Galois, the first ramification group G_1 of w is trivial if and only if the different exponent at w is e(w/v) - 1, the tame value of Dedekind's different theorem.