Restriction of arithmetic Frobenius

An arithmetic Frobenius in a field extension remains an arithmetic Frobenius after restriction to a normal intermediate extension. More precisely, if L/M/K is a tower with M/K normal and σ ∈ Gal(L/K) is an arithmetic Frobenius at Q, then σ|_M is an arithmetic Frobenius at the contracted prime Q ∩ 𝓞 M.

This is the unpowered restriction law: both Frobenius elements are relative to the same base field K, so both act on residue fields by the cardinality of the residue field of the same base prime. The distinct tower law obtained by raising the base from K to M involves the inertia degree as an exponent and is not proved here.

The argument follows Jürgen Neukirch, Algebraic Number Theory, Chapter I, §9.

Main result

• IsArithFrobAt.restrictNormal: restriction to a normal intermediate extension preserves the arithmetic-Frobenius property at the contracted prime.

theorem IsArithFrobAt.restrictNormal {K : Type u_1} {M : Type u_2} {L : Type u_3} [Field K] [Field M] [Field L] [Algebra K M] [Algebra M L] [Algebra K L] [IsScalarTower K M L] [Normal K M] {Q : Ideal (NumberField.RingOfIntegers L)} {σ : Gal(L/K)} (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) : IsArithFrobAt (NumberField.RingOfIntegers K) (σ.restrictNormal M) (Ideal.under (NumberField.RingOfIntegers M) Q)

Arithmetic Frobenius restricts without a power along a normal subextension.

If σ ∈ Gal(L/K) is an arithmetic Frobenius at Q, its restriction to a normal intermediate extension M/K is an arithmetic Frobenius at Q ∩ 𝓞 M. The exponent on both sides is the cardinality of 𝓞 K modulo the contraction of Q; Ideal.under_under identifies the two contractions.