Conjugation on ramification quotients

Let a group G act on a nonarchimedean local field L, preserving its ring of integers. Conjugation by an element σ of inertia acts on every ramification quotient G_i/G_{i+1}. At depth zero this action is trivial. At positive depth, the embedding into the additive residue field transforms by the ith power of the tame character:

theta_i(σ τ σ⁻¹) = theta_0(σ)^i * theta_i(τ).

Here the positive-depth maps are read in the residue coordinate associated to a uniformizer. The exponent is forced by changing from the uniformizer π to σ⁻¹ π. This formula supplies the constant appearing in ramification-theoretic norm computations.

Conjugation by an arbitrary element g ∈ G, which need not act trivially on the residue field, transports the tame character through the residue-field automorphism induced by g:

theta_0(g σ g⁻¹) = g • theta_0(σ).

When g acts on the residue field as x ↦ x ^ q, as an arithmetic Frobenius does, this reads theta_0(g σ g⁻¹) = theta_0(σ) ^ q, the finite-level form of the Frobenius twist on tame inertia.

Main results

• TauCeti.ramificationGroupGradedConj_zero: inertia acts trivially on G_0/G_1.
• TauCeti.ramificationGroupGradedToResidueField_conj: at depth i > 0, conjugation scales the residue coordinate by the ith power of the tame character.
• TauCeti.tameCharacter_conj and TauCeti.tameCharacterGraded_ramificationGroupGradedConj: the tame character is equivariant for conjugation by G and the action of G on the residue field.
• TauCeti.tameCharacter_conj_of_smul_eq_pow and TauCeti.tameCharacterGraded_ramificationGroupGradedConj_of_smul_eq_pow: conjugation by an element acting on the residue field as the q-th power map raises the tame character to the q-th power.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §2, Proposition 9.

@[simp]

theorem TauCeti.ramificationGroupGradedConj_zero {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] {G : Type u_2} [Group G] [MulSemiringAction G L] [IsInvariantSubring G (ValuativeRel.valuation L).integer] (σ : ↥(IsLocalRing.ramificationGroup G (↥(ValuativeRel.valuation L).integer) 0)) (τ : IsLocalRing.RamificationGroupGraded G (↥(ValuativeRel.valuation L).integer) 0) : (IsLocalRing.ramificationGroupGradedConj G (↥(ValuativeRel.valuation L).integer) (↑σ) 0) τ = τ

Conjugation by inertia acts trivially on the tame quotient G_0/G_1.

@[simp]

theorem TauCeti.ramificationGroupGradedToResidueField_conj {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] {G : Type u_2} [Group G] [MulSemiringAction G L] [IsInvariantSubring G (ValuativeRel.valuation L).integer] (n : ℕ) (π : ↥(ValuativeRel.valuation L).integer) (hπ : Irreducible π) (σ : ↥(IsLocalRing.ramificationGroup G (↥(ValuativeRel.valuation L).integer) 0)) (τ : IsLocalRing.RamificationGroupGraded G (↥(ValuativeRel.valuation L).integer) (↑n + 1)) : (ramificationGroupGradedToResidueField L G n π hπ) (Additive.ofMul ((IsLocalRing.ramificationGroupGradedConj G (↥(ValuativeRel.valuation L).integer) (↑σ) (↑n + 1)) τ)) = ↑((tameCharacter hπ) σ) ^ (n + 1) * (ramificationGroupGradedToResidueField L G n π hπ) (Additive.ofMul τ)

The conjugation action formula on positive ramification quotients. In the residue coordinate determined by π, conjugation by σ ∈ G_0 acts on G_i/G_{i+1} as multiplication by theta_0(σ)^i, where theta_0 is the tame character.

Equivariance of the tame character

@[simp]

theorem TauCeti.tameCharacter_conj {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] {G : Type u_2} [Group G] [MulSemiringAction G L] [IsInvariantSubring G (ValuativeRel.valuation L).integer] {π : ↥(ValuativeRel.valuation L).integer} (hπ : Irreducible π) (g : G) (σ : ↥(IsLocalRing.ramificationGroup G (↥(ValuativeRel.valuation L).integer) 0)) : ↑((tameCharacter hπ) ((MulAut.conjNormal g) σ)) = g • ↑((tameCharacter hπ) σ)

The tame character is equivariant. For g ∈ G and σ ∈ G_0, the tame character of g σ g⁻¹ is the image of the tame character of σ under the automorphism of the residue field induced by g: theta_0(g σ g⁻¹) = g • theta_0(σ).

theorem TauCeti.tameCharacter_conj_of_smul_eq_pow {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] {G : Type u_2} [Group G] [MulSemiringAction G L] [IsInvariantSubring G (ValuativeRel.valuation L).integer] {π : ↥(ValuativeRel.valuation L).integer} (hπ : Irreducible π) {g : G} {q : ℕ} (hg : ∀ (x : IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer), g • x = x ^ q) (σ : ↥(IsLocalRing.ramificationGroup G (↥(ValuativeRel.valuation L).integer) 0)) : (tameCharacter hπ) ((MulAut.conjNormal g) σ) = (tameCharacter hπ) σ ^ q

The tame character twisted by a power map. If g ∈ G acts on the residue field as the q-th power map, then theta_0(g σ g⁻¹) = theta_0(σ) ^ q for every σ ∈ G_0. This applies with q the cardinality of the residue field of a base field to any automorphism of a finite extension inducing the arithmetic Frobenius on residue fields.

@[simp]

theorem TauCeti.tameCharacterGraded_ramificationGroupGradedConj {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] {G : Type u_2} [Group G] [MulSemiringAction G L] [IsInvariantSubring G (ValuativeRel.valuation L).integer] {π : ↥(ValuativeRel.valuation L).integer} (hπ : Irreducible π) (g : G) (τ : IsLocalRing.RamificationGroupGraded G (↥(ValuativeRel.valuation L).integer) 0) : ↑((tameCharacterGraded hπ) ((IsLocalRing.ramificationGroupGradedConj G (↥(ValuativeRel.valuation L).integer) g 0) τ)) = g • ↑((tameCharacterGraded hπ) τ)

The equivariance of the tame character, read on the tame quotient G_0/G_1.

theorem TauCeti.tameCharacterGraded_ramificationGroupGradedConj_of_smul_eq_pow {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] {G : Type u_2} [Group G] [MulSemiringAction G L] [IsInvariantSubring G (ValuativeRel.valuation L).integer] {π : ↥(ValuativeRel.valuation L).integer} (hπ : Irreducible π) {g : G} {q : ℕ} (hg : ∀ (x : IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer), g • x = x ^ q) (τ : IsLocalRing.RamificationGroupGraded G (↥(ValuativeRel.valuation L).integer) 0) : (tameCharacterGraded hπ) ((IsLocalRing.ramificationGroupGradedConj G (↥(ValuativeRel.valuation L).integer) g 0) τ) = (tameCharacterGraded hπ) τ ^ q

The power-map twist of the tame character, read on the tame quotient G_0/G_1.