Frobenius under the decomposition-group equivalence

Let L/K be a Galois extension of number fields, and let w be a finite place of L above a finite place v of K. The decomposition-group equivalence identifies the stabilizer of w with the Galois group of the completed extension L_w/K_v. This file proves that the identification respects reduction to residue fields. Consequently it carries an arithmetic Frobenius at w to the Frobenius automorphism of an unramified local extension.

The residue compatibility is stated pointwise through the canonical equivalences R ⧸ v ≃ 𝓀[K_v] and S ⧸ w ≃ 𝓀[L_w]. This avoids choosing a second algebra structure on either residue extension.

Main results

• IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletion_stabilizerHom: reduction intertwines the global decomposition action with the action on the completed residue field.
• IsDedekindDomain.HeightOneSpectrum.decompositionHom_eq_frobeniusAlgEquiv: a global arithmetic Frobenius maps to the local Frobenius.

References

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

theorem IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletion_stabilizerHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (σ : ↥(MulAction.stabilizer Gal(L/K) w.asIdeal)) (x : NumberField.RingOfIntegers L ⧸ w.asIdeal) : w.residueFieldEquivAdicCompletion (((Ideal.Quotient.stabilizerHom w.asIdeal (Ideal.under (NumberField.RingOfIntegers K) w.asIdeal) Gal(L/K)) σ) x) = ((MulSemiringAction.toAlgAut Gal(adicCompletion L w/adicCompletion K v) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion K v)).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion L w)).integer)) ((v.decompositionHom w) σ)) (w.residueFieldEquivAdicCompletion x)

The global and local residue actions agree. Under the canonical identification of the residue field of w with the residue field of L_w, the action of an element of the global decomposition group is the residue action of its continuous extension to L_w.

theorem IsDedekindDomain.HeightOneSpectrum.decompositionHom_eq_frobeniusAlgEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsGalois (adicCompletion K v) (adicCompletion L w)] [TauCeti.IsUnramified (adicCompletion K v) (adicCompletion L w)] {σ : Gal(L/K)} (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ w.asIdeal) : (v.decompositionHom w) ⟨σ, ⋯⟩ = TauCeti.frobeniusAlgEquiv

The decomposition-group map carries global arithmetic Frobenius to local Frobenius. If the completed extension L_w/K_v is Galois and unramified, the continuous extension to L_w of an arithmetic Frobenius at w is its canonical Frobenius automorphism.