Absolute inertia and Frobenius lifts at finite level

Restriction to a finite Galois subextension L/K of the algebraic closure sends the absolute inertia subgroup onto the zeroth lower ramification group of L/K. Thus every finite inertia automorphism lifts to an automorphism fixing the entire maximal unramified extension. This surjectivity is needed to pass Sylow subgroups of absolute inertia to finite wild inertia.

The proof uses the unramifiedness criterion for fields fixed by absolute inertia, the identity e · f = [L : K], and the order formula #G₀ = e. The finite fixed field is embedded in the algebraic closure to apply the absolute inertia criterion; its degree is preserved by IntermediateField.liftAlgEquiv.

The restriction σ_L of an arithmetic Frobenius lift to L acts on the residue field of L as the q-th power map, so conjugation by σ_L raises the tame character of G_0(L/K) to the q-th power: θ_0(σ_L τ σ_L⁻¹) = θ_0(τ) ^ q. This is the finite-level form of the relation σ τ σ⁻¹ = τ ^ q in the tame quotient of the absolute Galois group.

Main results

• TauCeti.map_inertiaSubgroup_restrictNormalHom: the image of I_K in Gal(L/K) is G_0.
• TauCeti.exists_mem_inertiaSubgroup_restrictNormal_eq: every element of G_0 lifts to I_K.
• TauCeti.IsArithFrobeniusLift.tameCharacter_conj_restrictNormal: the finite-level Frobenius twist of the tame character.

References

• J.-P. Serre, Local Fields, Chapter I, §7 and Chapter IV, §§1–2.
• J. Neukirch, Algebraic Number Theory, Chapter II, §9.

@[simp]

theorem TauCeti.map_inertiaSubgroup_restrictNormalHom {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [Module.Finite K ↥L] [IsGalois K ↥L] [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] : Subgroup.map (AlgEquiv.restrictNormalHom ↥L) (inertiaSubgroup K) = LocalFieldsRamification.lowerRamificationGroup K (↥L) 0

Absolute inertia maps onto finite inertia. For every compatible local-field structure on a finite Galois subextension L/K, the image of I_K under restriction is G₀(L/K).

theorem TauCeti.exists_mem_inertiaSubgroup_restrictNormal_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [Module.Finite K ↥L] [IsGalois K ↥L] [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] {τ : Gal(↥L/K)} (hτ : τ ∈ LocalFieldsRamification.lowerRamificationGroup K (↥L) 0) : ∃ σ ∈ inertiaSubgroup K, AlgEquiv.restrictNormal σ ↥L = τ

Every element of finite inertia lifts to an element of absolute inertia.

theorem TauCeti.IsArithFrobeniusLift.tameCharacter_conj_restrictNormal {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [Module.Finite K ↥L] [IsGalois K ↥L] [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] {σ : Gal(AlgebraicClosure K/K)} (hσ : IsArithFrobeniusLift K σ) {π : ↥(ValuativeRel.valuation ↥L).integer} (hπ : Irreducible π) (τ : ↥(IsLocalRing.ramificationGroup Gal(↥L/K) (↥(ValuativeRel.valuation ↥L).integer) 0)) : (tameCharacter hπ) ((MulAut.conjNormal (σ.restrictNormal ↥L)) τ) = (tameCharacter hπ) τ ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The finite-level Frobenius twist. Let σ be an arithmetic Frobenius lift and σ_L its restriction to a finite Galois subextension L/K. For every τ in the inertia group G_0 of L/K, the tame character satisfies θ_0(σ_L τ σ_L⁻¹) = θ_0(τ) ^ q, where q is the cardinality of the residue field of K.