Contracting a Frobenius fiber to the fixed field

Fix σ ∈ Gal(L/K) and let E = L ^ ⟨σ⟩. If σ is an arithmetic Frobenius at a prime Q of 𝓞 L unramified over 𝓞 K, then over E there is a relative Frobenius at Q restricting to σ. That is the direction a fixed-field count needs from this file.

The converse — recovering σ from a relative Frobenius at residue degree one — holds for any intermediate field, so it lives in Frobenius/Tower.lean as NumberField.isArithFrobAt_restrictScalars_of_inertiaDeg_eq_one. Injectivity of contraction comes from Ideal.eq_of_smul_eq_of_liesOver_under_fixedField.

Main results

• Ideal.exists_isArithFrobAt_and_restrictScalars_eq: a prime carrying σ has, over the fixed field, a relative Frobenius restricting to σ.
• Ideal.inertiaDeg_under_eq_one_and_isArithFrobAt_fixedField: a relative Frobenius τ over the fixed field restricting to a Frobenius over K gives residue degree one below and a relative Frobenius.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, §9.

theorem Ideal.exists_isArithFrobAt_and_restrictScalars_eq {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] (σ : Gal(L/K)) (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) : ∃ (τ : Gal(L/↥(IntermediateField.fixedField (Subgroup.zpowers σ)))), IsArithFrobAt (NumberField.RingOfIntegers ↥(IntermediateField.fixedField (Subgroup.zpowers σ))) τ Q ∧ AlgEquiv.restrictScalars K τ = σ

A Frobenius fiber has a relative Frobenius over the fixed field. If σ is an arithmetic Frobenius at an unramified prime Q, then over L ^ ⟨σ⟩ there is an arithmetic Frobenius at Q whose restriction to Gal(L/K) is σ itself.

theorem Ideal.inertiaDeg_under_eq_one_and_isArithFrobAt_fixedField {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] (σ : Gal(L/K)) (τ : Gal(L/↥(IntermediateField.fixedField (Subgroup.zpowers σ)))) (hQ : IsArithFrobAt (NumberField.RingOfIntegers K) (AlgEquiv.restrictScalars K τ) Q) : (under (NumberField.RingOfIntegers ↥(IntermediateField.fixedField (Subgroup.zpowers σ))) Q).inertiaDeg (NumberField.RingOfIntegers K) = 1 ∧ IsArithFrobAt (NumberField.RingOfIntegers ↥(IntermediateField.fixedField (Subgroup.zpowers σ))) τ Q

Below a prime Q of L unramified over K at which τ, read over K, is an arithmetic Frobenius lies a prime of E = L ^ ⟨σ⟩ of residue degree one over K, and τ is an arithmetic Frobenius at Q over E.