The absolute ramification index of a mixed-characteristic local field

Let p be prime and let K be a nonarchimedean local field carrying the structure of a finite compatible extension of ℚ_[p]. This file defines the absolute ramification index

TauCeti.absoluteRamificationIndex K p = e(K/ℚ_[p]).

For a compatible extension, its characteristic calculation identifies it with the normalized valuation of p in K. Consequently the index of ℚ_[p] itself is one, and in a tower over ℚ_[p] the absolute index is multiplied by the relative ramification index.

The definition is confined to mixed characteristic by requiring an algebra structure over ℚ_[p]; there is no artificial value for equal-characteristic local fields.

Main definitions

• TauCeti.FinitePadicExtension: a bundled finite compatible extension structure over ℚ_[p].
• TauCeti.absoluteRamificationIndex: the ramification index of K/ℚ_[p].

Main results

• TauCeti.FinitePadicExtension.charZero: a finite extension of ℚ_[p] has characteristic zero.
• TauCeti.absoluteRamificationIndex_pos: the absolute ramification index is positive.
• TauCeti.absoluteRamificationIndex_eq_natCastValuation: the absolute ramification index is the normalized valuation of p in K.
• TauCeti.natCastValuation_eq_absoluteRamificationIndex_mul_padicValNat: the valuation of a natural-number cast in a finite extension of ℚ_[p].
• TauCeti.valuation_natCast_eq_pow_mul_padicValNat: the same valuation, as a power of the valuation of a uniformizer.
• TauCeti.absoluteRamificationIndex_padic: the absolute ramification index of ℚ_[p] is one.
• TauCeti.residuePrime_mem_maximalIdeal: the residue prime lies in the maximal ideal of 𝒪[K].
• TauCeti.absoluteRamificationIndex_tower: the absolute index is multiplicative in a tower.

References

• J.-P. Serre, Corps Locaux, Chapter II, §1.
• J. Neukirch, Algebraic Number Theory, Chapter II, §6.

class TauCeti.FinitePadicExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] : Type u_1

A nonarchimedean local field equipped as a finite compatible extension of ℚ_[p].

The algebra structure is bundled so that the finiteness and compatibility conditions constrain the domain of absoluteRamificationIndex without becoming unused arguments of its definition.

• algebra : Algebra ℚ_[p] K

  The ℚ_[p]-algebra structure on the extension.

• toModuleFinite : Module.Finite ℚ_[p] K

  The extension has finite degree over ℚ_[p].

• toValuativeExtension : ValuativeExtension ℚ_[p] K

  The algebra map is compatible with the valuative relations.

@[instance_reducible]

instance TauCeti.FinitePadicExtension.toAlgebra (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [h : FinitePadicExtension K p] : Algebra ℚ_[p] K

Equations

• TauCeti.FinitePadicExtension.toAlgebra K p = TauCeti.FinitePadicExtension.algebra

@[instance_reducible]

instance TauCeti.FinitePadicExtension.ofInstances (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] : FinitePadicExtension K p

Package existing finite compatible extension instances as a FinitePadicExtension.

Equations

• TauCeti.FinitePadicExtension.ofInstances K p = { algebra := inferInstance, toModuleFinite := ⋯, toValuativeExtension := ⋯ }

theorem TauCeti.FinitePadicExtension.charZero (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] : CharZero K

A finite extension of ℚ_[p] has characteristic zero. This is not an instance: p is not determined by CharZero K.

instance TauCeti.FinitePadicExtension.neZero_natCast (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] : NeZero ↑p

The prime p is nonzero in a finite extension of ℚ_[p].

noncomputable def TauCeti.absoluteRamificationIndex (K : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] : ℕ

The absolute ramification index of a finite compatible extension of ℚ_[p].

Equations

• TauCeti.absoluteRamificationIndex K p = TauCeti.ramificationIndex ℚ_[p] K

theorem TauCeti.absoluteRamificationIndex_pos (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] : 0 < absoluteRamificationIndex K p

The absolute ramification index is positive.

theorem TauCeti.natCastValuation_eq_absoluteRamificationIndex_mul_padicValNat (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] (n : ℕ) (hn : n ≠ 0) : natCastValuation K n ⋯ = absoluteRamificationIndex K p * padicValNat p n

In a finite extension K/ℚ_[p], the normalized valuation of a nonzero natural number is the absolute ramification index times its p-adic valuation.

theorem TauCeti.valuation_natCast_eq_pow_mul_padicValNat {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) {n : ℕ} (hn : n ≠ 0) : (ValuativeRel.valuation K) ↑n = (ValuativeRel.valuation K) ↑π ^ (absoluteRamificationIndex K p * padicValNat p n)

In a finite extension K/ℚ_[p], the valuation of a nonzero natural number n is v(π) ^ (e * v_p(n)) for any uniformizer π, where e is the absolute ramification index.

@[simp]

theorem TauCeti.absoluteRamificationIndex_eq_natCastValuation (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] : absoluteRamificationIndex K p = natCastValuation K p ⋯

The absolute ramification index is the normalized valuation of the residue prime p in K.

theorem TauCeti.absoluteRamificationIndex_padic (p : ℕ) [Fact (Nat.Prime p)] : absoluteRamificationIndex ℚ_[p] p = 1

The absolute ramification index of ℚ_[p] is one.

theorem TauCeti.residuePrime_mem_maximalIdeal (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] : ↑p ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer

The residue prime p lies in the maximal ideal of 𝒪[K].

theorem TauCeti.absoluteRamificationIndex_tower (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [FinitePadicExtension L p] [Algebra K L] [IsScalarTower ℚ_[p] K L] [ValuativeExtension K L] : absoluteRamificationIndex L p = ramificationIndex K L * absoluteRamificationIndex K p

In a tower L/K/ℚ_[p], the absolute ramification index of L is the product of the relative ramification index of L/K and the absolute ramification index of K.