Relative discriminant coefficients from double cosets

Let L/K be a Galois extension of number fields, H ≤ Gal(L/K), and E = Lᴴ. Fix a prime Q of L over a prime p of K. The double cosets H \ Gal(L/K) / D(Q) index the primes of E over p. This file computes the coefficient of p in the relative discriminant of E/K entirely from the decomposition, inertia, and lower ramification groups at Q and their conjugates.

For a representative σ, put Dσ = σD(Q)σ⁻¹, Iσ = σI(Q)σ⁻¹, and Gσ,i = σG_i(Q)σ⁻¹. Its contribution is

([Dσ : Dσ ∩ H] / [Iσ : Iσ ∩ H]) * (Σ_i (|G_i(Q)| - |Gσ,i ∩ H|) / |Iσ ∩ H|).

The first quotient is the residue degree of σQ ∩ E; the second is its different exponent. Both divisions are exact and their denominators are positive. The infinite sum has only finitely many nonzero terms, since the lower ramification groups are eventually trivial. No unramified or tame hypothesis is imposed. Representatives may be chosen arbitrarily, and the formula also shows that each contribution depends only on its double coset.

The local input is IsDedekindDomain.HeightOneSpectrum.ramificationIdx_mul_multiplicity_differentIdeal_fixedField. The global step combines TauCeti.multiplicity_relDiscr with Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant to sum these local contributions.

References

• J.-P. Serre, Local Fields, Chapter IV, §§1–2.
• J. Neukirch, Algebraic Number Theory, Chapter I, §9 and Chapter III, §2.

theorem TauCeti.NumberField.inertiaDeg_mul_multiplicity_differentIdeal_under_fixedField_eq (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (H : Subgroup Gal(L/K)) : (Ideal.under (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H)) w.asIdeal).inertiaDeg (NumberField.RingOfIntegers K) * multiplicity (Ideal.under (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H)) w.asIdeal) (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H))) = H.relIndex (MulAction.stabilizer Gal(L/K) w.asIdeal) / H.relIndex (Ideal.inertia Gal(L/K) w.asIdeal) * ((∑ᶠ (i : ℕ), (Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i) - Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i ⊓ H))) / Nat.card ↥(Ideal.inertia Gal(L/K) w.asIdeal ⊓ H))

The residue-degree-weighted different exponent below Q in Lᴴ, expressed using only subgroup indices and ramification groups. The two natural-number divisions are exact: their numerators are respectively e * f and e(Q / Q∩Lᴴ) * v(𝔇).

theorem TauCeti.NumberField.inertiaDeg_mul_multiplicity_differentIdeal_under_fixedField_smul_eq (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (H : Subgroup Gal(L/K)) (σ : Gal(L/K)) : (Ideal.under (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H)) (σ • w.asIdeal)).inertiaDeg (NumberField.RingOfIntegers K) * multiplicity (Ideal.under (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H)) (σ • w.asIdeal)) (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H))) = H.relIndex (MulAut.conj σ • MulAction.stabilizer Gal(L/K) w.asIdeal) / H.relIndex (MulAut.conj σ • Ideal.inertia Gal(L/K) w.asIdeal) * ((∑ᶠ (i : ℕ), (Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i) - Nat.card ↥(MulAut.conj σ • Ideal.ramificationGroup Gal(L/K) w.asIdeal i ⊓ H))) / Nat.card ↥(MulAut.conj σ • Ideal.inertia Gal(L/K) w.asIdeal ⊓ H))

The discriminant contribution of a double coset representative is the residue-degree-weighted different exponent of its associated prime. In particular it is unchanged when the representative is replaced by another element of the same double coset.

theorem TauCeti.NumberField.multiplicity_relDiscr_fixedField_eq_sum (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (H : Subgroup Gal(L/K)) (r : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer Gal(L/K) w.asIdeal) → Gal(L/K)) (hr : ∀ (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer Gal(L/K) w.asIdeal)), DoubleCoset.mk H (MulAction.stabilizer Gal(L/K) w.asIdeal) (r q) = q) : multiplicity v.asIdeal (relDiscr (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H))) = ∑ᶠ (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer Gal(L/K) w.asIdeal)), H.relIndex (MulAut.conj (r q) • MulAction.stabilizer Gal(L/K) w.asIdeal) / H.relIndex (MulAut.conj (r q) • Ideal.inertia Gal(L/K) w.asIdeal) * ((∑ᶠ (i : ℕ), (Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i) - Nat.card ↥(MulAut.conj (r q) • Ideal.ramificationGroup Gal(L/K) w.asIdeal i ⊓ H))) / Nat.card ↥(MulAut.conj (r q) • Ideal.inertia Gal(L/K) w.asIdeal ⊓ H))

The relative discriminant coefficient of a fixed field from double cosets. Sum the group-theoretic contributions over H \ Gal(L/K) / D(Q), using any choice of representatives. The formula holds at ramified primes as well as unramified ones, including wild ramification.