The different exponent in a fixed field #
For a finite Galois extension L/K, the coefficient of the different of a fixed field Lᴴ/K
at the prime below Q is determined by how many elements of each ramification group at Q
lie outside H. The ramification index of Q over that prime clears the denominator in this
formula. It follows from Hilbert's different formula and transitivity of the different.
References #
- J.-P. Serre, Local Fields, Chapter IV, §§1–2.
theorem
IsDedekindDomain.HeightOneSpectrum.ramificationIdx_mul_multiplicity_differentIdeal_fixedField
{K : Type u_1}
{L : Type u_2}
[Field K]
[NumberField K]
[Field L]
[NumberField L]
[Algebra K L]
[IsGalois K L]
(w : HeightOneSpectrum (NumberField.RingOfIntegers L))
(H : Subgroup Gal(L/K))
:
w.asIdeal.ramificationIdx (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H)) * multiplicity (under (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H)) w).asIdeal
(differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H))) = ∑ᶠ (i : ℕ), (Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i) - Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i ⊓ H))
The different exponent of a fixed field from its permutation action. The ramification
index over the selected prime of Lᴴ times its different exponent is the sum, over the lower
ramification groups at Q, of the numbers of elements outside H.