Frobenius cycle lengths and splitting in a fixed field

Let L/K be a finite Galois extension of number fields and H any subgroup of its Galois group. At a prime unramified in L, the full cycle type of an arithmetic Frobenius acting on Gal(L/K) ⧸ H is the multiset of residue degrees of the primes of L ^ H above it. Repeated degrees are retained, and fixed cosets contribute parts equal to one. No normality of H is required.

The arithmetic input is Ideal.map_card_orbit_stabilizer_eq_map_ramificationIdx_mul_inertiaDeg, the decomposition-orbit form of the double coset law. Unramifiedness removes its ramification indices, and Ideal.zpowers_eq_stabilizer_of_isArithFrobAt identifies the decomposition group with the cyclic group generated by Frobenius. This dictionary allows prime splitting conditions in nonnormal extensions to be read as conjugacy-invariant conditions on their Galois closure.

References

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

theorem Ideal.fullCycleType_toPerm_quotient_eq_map_inertiaDeg {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver p] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] (H : Subgroup Gal(L/K)) {σ : Gal(L/K)} (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) : (MulAction.toPerm σ).fullCycleType = Multiset.map (fun (P : ↑(p.primesOver (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H)))) => (↑P).inertiaDeg (NumberField.RingOfIntegers K)) Finset.univ.val

The full cycle type of Frobenius on Galois cosets is the multiset of residue degrees in the fixed field. This includes fixed points and counts repeated degrees with multiplicity.