The cyclotomic character on inertia and on Frobenius lifts

Let K be a nonarchimedean local field whose residue field has q elements, and let p be a prime different from the residue characteristic. The roots of unity of p-power order of K^{alg} lie in the maximal unramified extension of K, so the p-adic cyclotomic character of G_K = Gal(K^{alg}/K) factors through the unramified quotient G_K ⧸ I_K: it is trivial on the inertia subgroup, and it takes the value q on every arithmetic Frobenius lift.

Main results

• TauCeti.localCyclotomicCharacter_eq_one_of_mem_inertiaSubgroup: the p-adic cyclotomic character is trivial on inertia.
• TauCeti.IsArithFrobeniusLift.coe_localCyclotomicCharacter: the p-adic cyclotomic character of an arithmetic Frobenius lift is q.

References

• J.-P. Serre, Local Fields, Chapter IV, §4.
• J. Neukirch, Algebraic Number Theory, Chapter II, §9.

theorem TauCeti.localCyclotomicCharacter_eq_one_of_mem_inertiaSubgroup {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] (hp : p.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) {σ : Field.absoluteGaloisGroup K} (hσ : σ ∈ inertiaSubgroup K) : (localCyclotomicCharacter p K) σ = 1

The cyclotomic character is unramified away from the residue characteristic: for a prime p different from the residue characteristic of K, the p-adic cyclotomic character is trivial on the inertia subgroup.

theorem TauCeti.IsArithFrobeniusLift.coe_localCyclotomicCharacter {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] (hp : p.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) : ↑((localCyclotomicCharacter p K) σ) = ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))

The cyclotomic character of a Frobenius lift: for a prime p different from the residue characteristic of K, the p-adic cyclotomic character of an arithmetic Frobenius lift is the cardinality q of the residue field.