The ℓ-adic tame character

Let K be a nonarchimedean local field with residue characteristic p and residue field of order q, and let I_K be its inertia group. The tame character I_K → ℤ̂^{(p')}(1) = lim_{p ∤ m} μ_m(K^{alg}), σ ↦ (σ(π^{1/m})/π^{1/m})_m, identifies the tame inertia group I_K/P_K with ℤ̂^{(p')}(1), which as a profinite group is ∏_{ℓ ≠ p} ℤ_ℓ. This file specializes it at a single ℓ prime to p: keeping only the components at the powers ℓ ^ n gives the ℓ-adic tame character

t_ℓ : I_K →ₜ* ℤ_ℓ(1) = lim_n μ_{ℓ ^ n}(K^{alg}), σ ↦ (σ(π^{1/ℓ^n})/π^{1/ℓ^n})_n.

It inherits from the tame character:

• its independence of the uniformizer π and of the chosen roots π^{1/ℓ^n};
• surjectivity, since the tame character is onto at every finite level and I_K is compact;
• triviality on wild inertia; more precisely, σ ∈ I_K has trivial ℓ-adic tame character exactly when it fixes every ℓ ^ n-th root of π;
• the twist: conjugation by g ∈ G_K acts on ℤ_ℓ(1) through the action of g on the ℓ-power roots of unity, so that conjugation by an arithmetic Frobenius lift is x ↦ x ^ q.

Main definitions

• TauCeti.inertiaPadicTameCharacter K hℓ: the ℓ-adic tame character I_K →ₜ* ℤ_ℓ(1), written multiplicatively, for ℓ prime to p.

Main results

• TauCeti.coe_proj_inertiaPadicTameCharacter_apply: its level-n component at σ is σ(α)/α for every root α of X ^ (ℓ ^ n) − π, for any uniformizer π.
• TauCeti.inertiaPadicTameCharacter_surjective: it is surjective.
• TauCeti.inertiaPadicTameCharacter_eq_one_iff: its kernel consists of the elements of inertia fixing every ℓ ^ n-th root of a uniformizer.
• TauCeti.inertiaPadicTameCharacter_eq_one_of_mem_wildInertiaSubgroup: it is trivial on wild inertia.
• TauCeti.inertiaPadicTameCharacter_conj: it is equivariant for conjugation by G_K and the Galois action on ℤ_ℓ(1), for a prime ℓ.
• TauCeti.IsArithFrobeniusLift.inertiaPadicTameCharacter_conj: conjugation by an arithmetic Frobenius lift raises it to the q-th power.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (7.5.2).
• J.-P. Serre, Corps Locaux, Chapter IV, §2.

noncomputable def TauCeti.inertiaPadicTameCharacter (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} (hℓ : ℓ.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) : ↥(inertiaSubgroup K) →ₜ* Multiplicative (PadicTateTwist ℓ (AlgebraicClosure K))

The ℓ-adic tame character of K, for ℓ prime to the residue characteristic p: the continuous homomorphism I_K →ₜ* ℤ_ℓ(1), written multiplicatively, sending σ to (σ(π^{1/ℓ^n})/π^{1/ℓ^n})_n for a uniformizer π and any ℓ ^ n-th roots π^{1/ℓ^n} of it (TauCeti.coe_proj_inertiaPadicTameCharacter_apply). It is the specialization at ℓ of the tame character I_K →ₜ* ℤ̂^{(p')}(1).

Equations

• TauCeti.inertiaPadicTameCharacter K hℓ = (TauCeti.PrimeToPTateModule.toPadicTateTwist ℓ hℓ).comp (TauCeti.inertiaTameCharacter K)

theorem TauCeti.inertiaPadicTameCharacter_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} {hℓ : ℓ.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))} [NeZero ℓ] (σ : ↥(inertiaSubgroup K)) : (inertiaPadicTameCharacter K hℓ) σ = (PrimeToPTateModule.toPadicTateTwist ℓ hℓ) ((inertiaTameCharacter K) σ)

The ℓ-adic tame character is the ℓ-adic component of the tame character.

theorem TauCeti.coe_proj_inertiaPadicTameCharacter_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} {hℓ : ℓ.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))} {σ : Gal(AlgebraicClosure K/K)} (hσ : σ ∈ inertiaSubgroup K) {π : Kˣ} (hπ : IsUniformizer K π) (n : ℕ) {α : AlgebraicClosure K} (hα : α ^ ℓ ^ n = (algebraMap K (AlgebraicClosure K)) ↑π) : ↑↑(Additive.toMul ((PadicTateTwist.proj n) (Multiplicative.toAdd ((inertiaPadicTameCharacter K hℓ) ⟨σ, hσ⟩)))) = σ α / α

The ℓ-adic tame character at level n. For a uniformizer π of K and any root α of X ^ (ℓ ^ n) − π, the ℓ ^ n-th roots-of-unity component of the ℓ-adic tame character at σ ∈ I_K is σ(α)/α.

theorem TauCeti.inertiaPadicTameCharacter_surjective (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} (hℓ : ℓ.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) : Function.Surjective ⇑(inertiaPadicTameCharacter K hℓ)

The ℓ-adic tame character is surjective: it is onto at each finite level, because the tame character is (TauCeti.proj_inertiaTameCharacter_surjective), and I_K is compact.

theorem TauCeti.inertiaPadicTameCharacter_eq_one_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} {hℓ : ℓ.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))} {σ : Gal(AlgebraicClosure K/K)} (hσ : σ ∈ inertiaSubgroup K) {π : Kˣ} (hπ : IsUniformizer K π) : (inertiaPadicTameCharacter K hℓ) ⟨σ, hσ⟩ = 1 ↔ ∀ (n : ℕ) (α : AlgebraicClosure K), α ^ ℓ ^ n = (algebraMap K (AlgebraicClosure K)) ↑π → σ α = α

The kernel of the ℓ-adic tame character: σ ∈ I_K has trivial ℓ-adic tame character exactly when it fixes every ℓ ^ n-th root of a uniformizer π, for every n.

theorem TauCeti.inertiaPadicTameCharacter_eq_one_of_mem_wildInertiaSubgroup {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} {hℓ : ℓ.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))} {σ : Gal(AlgebraicClosure K/K)} (hσ : σ ∈ inertiaSubgroup K) (hσ' : σ ∈ wildInertiaSubgroup K) : (inertiaPadicTameCharacter K hℓ) ⟨σ, hσ⟩ = 1

The ℓ-adic tame character is trivial on wild inertia, as the tame character is (TauCeti.inertiaTameCharacter_eq_one_iff).

theorem TauCeti.inertiaPadicTameCharacter_conj {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} {hℓ : ℓ.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))} [Fact (Nat.Prime ℓ)] (g : Gal(AlgebraicClosure K/K)) {σ : Gal(AlgebraicClosure K/K)} (hσ : σ ∈ inertiaSubgroup K) : (inertiaPadicTameCharacter K hℓ) ⟨g * σ * g⁻¹, ⋯⟩ = Multiplicative.ofAdd ((PadicTateTwist.galoisRepresentation g) (Multiplicative.toAdd ((inertiaPadicTameCharacter K hℓ) ⟨σ, hσ⟩)))

The ℓ-adic tame character is G_K-equivariant, for a prime ℓ: conjugating an element of inertia by g ∈ G_K applies to its ℓ-adic tame character the Galois representation of g on ℤ_ℓ(1), that is, g acting on the ℓ-power roots of unity. This is the twist (1) in ℤ_ℓ(1).

theorem TauCeti.IsArithFrobeniusLift.inertiaPadicTameCharacter_conj {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} {hℓ : ℓ.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))} {φ : Gal(AlgebraicClosure K/K)} (hφ : IsArithFrobeniusLift K φ) {σ : Gal(AlgebraicClosure K/K)} (hσ : σ ∈ inertiaSubgroup K) : (inertiaPadicTameCharacter K hℓ) ⟨φ * σ * φ⁻¹, ⋯⟩ = (inertiaPadicTameCharacter K hℓ) ⟨σ, hσ⟩ ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

Conjugation by a Frobenius lift is the q-th power on the ℓ-adic tame character: for an arithmetic Frobenius lift φ and σ ∈ I_K, t_ℓ(φ σ φ⁻¹) = t_ℓ(σ) ^ q, since φ raises every root of unity of order prime to p to the q-th power.