Inertia indices in the invariant-ring double-coset law

Let a finite Galois group G act on a finite flat extension of domains B/A, and let C be the invariant ring of a subgroup H. For a maximal ideal Q of B with separable residue extension over A, the prime of C indexed by the double coset of σ has ramification index

[σ I(Q) σ⁻¹ : H ∩ σ I(Q) σ⁻¹].

This supplies the ramification-index component of the double-coset splitting law, expressing the index at every prime represented by a double coset in terms of its conjugate inertia group. It does not assume that the residue fields are finite or perfect.

Main results

• Ideal.ramificationIdx_doubleCosetQuotientEquivPrimesOverOfIsInvariant_eq_relIndex_inertia: the ramification-index formula for the prime attached to a double coset.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §9, page 55.
• G. J. Janusz, Algebraic Number Fields, Chapter I.

theorem Ideal.ramificationIdx_doubleCosetQuotientEquivPrimesOverOfIsInvariant_eq_relIndex_inertia {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [IsDomain A] [IsDomain B] [IsGaloisGroup G A B] [Module.Finite A B] [Module.Flat A B] [Finite G] (p : Ideal A) (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [IsDomain C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsGaloisGroup (↥H) C B] [Module.Flat C B] [Algebra.IsSeparable (A ⧸ under A Q) (B ⧸ Q)] (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer G Q)) : (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).ramificationIdx A = H.relIndex (MulAut.conj (Quotient.out q) • inertia G Q)

The ramification index of the prime attached to a double coset is the relative index of the corresponding conjugate inertia group. The representative q.out is immaterial because the left-hand side depends only on the double coset.