Ramification indices and the fundamental identity in the double coset law

Let M / K be a finite Galois extension of number fields with group G, let H be a subgroup of G with fixed field E = M ^ H, and let Q be a prime of 𝓞 M above a prime p of 𝓞 K, with decomposition group D and inertia group I. The double coset law (Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant) indexes the primes of 𝓞 E above p by H \ G / D, the class of σ corresponding to 𝔮_σ = σ Q ∩ 𝓞 E. This file reads the ramification index of 𝔮_σ over p off the conjugate inertia group and expresses the fundamental identity Σ e(𝔮_σ / p) f(𝔮_σ / p) = [E : K] in these double-coset coordinates:

e(𝔮_σ / p) = [σIσ⁻¹ : H ∩ σIσ⁻¹].

The conjugate σIσ⁻¹ is written MulAut.conj σ • I. The residue degree is not obtained by the same recipe with D/I in place of D: the image of H ∩ σDσ⁻¹ in D/I need not be the intersection of the image of H with σ(D/I)σ⁻¹.

The local degrees e(𝔮_σ / p) f(𝔮_σ / p) = |HσD| / |H| are read off the double coset by the invariant-ring results in TauCeti.NumberTheory.RamificationInertia.DoubleCoset.Invariant.Basic, which apply directly to the canonical invariant-ring equivalence for these rings of integers. Summed over H \ G / D they give the field degree [E : K].

Main results

• Ideal.ramificationIdx_under_fixedField_smul_eq_relIndex: e(𝔮_σ) = [σIσ⁻¹ : H ∩ σIσ⁻¹].
• Ideal.sum_ramificationIdx_mul_inertiaDeg_doubleCoset_eq_finrank: the fundamental identity Σ_{H \ G / D} e(𝔮_σ) f(𝔮_σ) = [E : K] in double-coset coordinates.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, §9, page 55, where the double coset law is recorded and its proof left to the reader.
• G. J. Janusz, Algebraic Number Fields, Chapter I.

theorem Ideal.ramificationIdx_under_fixedField_smul_eq_relIndex {K : Type u_1} {M : Type u_2} [Field K] [NumberField K] [Field M] [NumberField M] [Algebra K M] [IsGalois K M] (Q : Ideal (NumberField.RingOfIntegers M)) [Q.IsPrime] (H : Subgroup Gal(M/K)) (σ : Gal(M/K)) : (under (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H)) (σ • Q)).ramificationIdx (NumberField.RingOfIntegers K) = H.relIndex (MulAut.conj σ • inertia Gal(M/K) Q)

The ramification index of σ Q ∩ 𝓞 (M ^ H) is an index of inertia groups: e = [σIσ⁻¹ : H ∩ σIσ⁻¹], where I is the inertia group of Q.

theorem Ideal.sum_ramificationIdx_mul_inertiaDeg_doubleCoset_eq_finrank {K : Type u_1} {M : Type u_2} [Field K] [NumberField K] [Field M] [NumberField M] [Algebra K M] [IsGalois K M] (p : Ideal (NumberField.RingOfIntegers K)) (Q : Ideal (NumberField.RingOfIntegers M)) [Q.IsPrime] [Q.LiesOver p] (H : Subgroup Gal(M/K)) : ∑ᶠ (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer Gal(M/K) Q)), (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H))) q)).ramificationIdx (NumberField.RingOfIntegers K) * (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H))) q)).inertiaDeg (NumberField.RingOfIntegers K) = Module.finrank K ↥(IntermediateField.fixedField H)

The fundamental identity in double-coset coordinates. The primes of the fixed field M ^ H above p are indexed by H \ Gal(M/K) / D(Q); their ramification indices times their residue degrees sum to the degree of M ^ H over K.