The ramification index of an extension of local fields

Let L/K be an extension of nonarchimedean local fields whose valuations are compatible, in the sense of ValuativeExtension K L. Restricting the normalized valuation v_L of L along the algebra map gives a homomorphism Kˣ →* Multiplicative ℤ, and this file defines

TauCeti.ramificationIndex K L : ℕ

as the index of its image in the normalized value group Multiplicative ℤ of L. No uniformizer is chosen in the definition. The characteristic property is TauCeti.normalizedValuation_algebraMap: v_L(x) = e · v_K(x) for every x : Kˣ, written multiplicatively as normalizedValuation L x = normalizedValuation K x ^ e. In particular the image in L of every uniformizer of K has normalized valuation e, so later statements never have to fix one.

The ramification index is the valuation-theoretic half of the pair (e, f) attached to a finite extension of local fields; together with the residue degree it enters the fundamental identity e · f = [L : K], and it is the factor by which the algebra map scales the depth of the unit filtration.

Main definitions

• TauCeti.ramificationIndex: the ramification index e(L/K) of an extension of nonarchimedean local fields.
• TauCeti.IsTamelyRamified, TauCeti.IsWildlyRamified: the residue characteristic does not divide, respectively divides, the ramification index.
• TauCeti.IsTotallyRamified: the ramification index equals the degree, e(L/K) = [L : K].

Main results

• TauCeti.normalizedValuation_algebraMap and TauCeti.toAdd_normalizedValuation_algebraMap: the characteristic property v_L(x) = e · v_K(x) on Kˣ, multiplicatively and additively.
• TauCeti.natCastValuation_eq_ramificationIndex_mul: the same identity for the valuation of a natural-number cast.
• TauCeti.normalizedValuationWithZero_algebraMap: the same identity on all of K.
• TauCeti.addVal_algebraMap: the corresponding scaling formula on the integer rings.
• TauCeti.addVal_sum_algebraMap_mul_pow_of_irreducible: the first e(L/K) powers of a uniformizer of L are orthogonal, so an 𝒪[K]-linear combination of them has the least term valuation.
• TauCeti.ramificationIndex_eq_iff: e is the only natural number with that property.
• TauCeti.ramificationIndex_pos: the ramification index is positive.
• TauCeti.normalizedValuation_algebraMap_irreducible and TauCeti.valuation_algebraMap_irreducible: a uniformizer of K has normalized valuation e in L, that is, its valuation is the e-th power of that of a uniformizer of L.
• TauCeti.map_maximalIdeal_eq_maximalIdeal_pow: the maximal ideal of 𝒪[K] generates 𝓂[L] ^ e(L/K).
• TauCeti.ramificationIndex_eq_ramificationIdx: the intrinsic ramification index agrees with Ideal.ramificationIdx of 𝓂[L] over 𝒪[K].
• TauCeti.ramificationIndex_tower: multiplicativity e(M/K) = e(L/K) · e(M/L) in a tower.
• TauCeti.isTamelyRamified_tower_iff: a tower is tame exactly when both steps are tame.
• TauCeti.isTamelyRamified_iff_natCast_ne_zero: L/K is tamely ramified exactly when e(L/K) is nonzero in the residue field of K.
• TauCeti.isTamelyRamified_iff_isUnit_natCast: L/K is tamely ramified exactly when e(L/K) is a unit in 𝒪[L].

Implementation notes

The definition only uses the algebra map and the two normalized valuations, so it does not carry the compatibility hypothesis ValuativeExtension K L. Apart from the unfolding lemma ramificationIndex_def and the reformulations of tame and wild ramification, every public theorem about it assumes compatibility, which makes the restricted valuation trivial on the units of 𝒪[K] and hence a power of v_K. Finiteness of L/K is used by no statement in this file.

References

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

noncomputable def TauCeti.ramificationIndex (K : Type u_1) (L : Type u_2) [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : ℕ

The ramification index e(L/K) of an extension of nonarchimedean local fields: the index in Multiplicative ℤ of the image of Kˣ under the normalized valuation of L. For a compatible extension this image is the subgroup of multiples of e, and e is characterized by normalizedValuation_algebraMap.

Equations

• TauCeti.ramificationIndex K L = ((TauCeti.normalizedValuation L).comp (Units.map ↑(algebraMap K L))).range.index

theorem TauCeti.ramificationIndex_def {K : Type u_1} {L : Type u_2} [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : ramificationIndex K L = ((normalizedValuation L).comp (Units.map ↑(algebraMap K L))).range.index

The defining formula of ramificationIndex: the index of the image of Kˣ in the normalized value group of L.

def TauCeti.IsTamelyRamified (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : Prop

An extension of nonarchimedean local fields is tamely ramified when the residue characteristic does not divide its ramification index. For a general valued field tameness also asks for a separable residue extension; that condition is automatic here, the residue fields of nonarchimedean local fields being finite.

Equations

• TauCeti.IsTamelyRamified K L = ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ TauCeti.ramificationIndex K L

def TauCeti.IsWildlyRamified (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : Prop

An extension of nonarchimedean local fields is wildly ramified when the residue characteristic divides its ramification index.

Equations

• TauCeti.IsWildlyRamified K L = (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ TauCeti.ramificationIndex K L)

theorem TauCeti.isTamelyRamified_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : IsTamelyRamified K L ↔ ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ ramificationIndex K L

The defining condition of tame ramification.

theorem TauCeti.isWildlyRamified_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : IsWildlyRamified K L ↔ ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ ramificationIndex K L

The defining condition of wild ramification.

@[simp]

theorem TauCeti.not_isTamelyRamified_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : ¬IsTamelyRamified K L ↔ IsWildlyRamified K L

An extension is wildly ramified exactly when it is not tamely ramified.

@[simp]

theorem TauCeti.not_isWildlyRamified_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : ¬IsWildlyRamified K L ↔ IsTamelyRamified K L

An extension is tamely ramified exactly when it is not wildly ramified.

theorem TauCeti.isTamelyRamified_iff_natCast_ne_zero (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : IsTamelyRamified K L ↔ ↑(ramificationIndex K L) ≠ 0

An extension is tamely ramified exactly when its ramification index is nonzero in the residue field of K.

def TauCeti.IsTotallyRamified (K : Type u_1) (L : Type u_2) [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : Prop

A finite extension of nonarchimedean local fields is totally ramified when its ramification index equals its degree.

Equations

• TauCeti.IsTotallyRamified K L = (TauCeti.ramificationIndex K L = Module.finrank K L)

theorem TauCeti.isTotallyRamified_iff_ramificationIndex_eq_finrank (K : Type u_1) (L : Type u_2) [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] : IsTotallyRamified K L ↔ ramificationIndex K L = Module.finrank K L

Total ramification unfolds to its defining equality e(L/K) = [L : K].

theorem TauCeti.normalizedValuation_algebraMap_eq_one_iff {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (x : Kˣ) : (normalizedValuation L) ((Units.map ↑(algebraMap K L)) x) = 1 ↔ (normalizedValuation K) x = 1

The normalized valuation of L vanishes on the image of x : Kˣ exactly when the normalized valuation of K vanishes on x: the algebra map of a compatible extension carries the units of 𝒪[K], and only those, to units of 𝒪[L].

theorem TauCeti.ramificationIndex_pos {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : 0 < ramificationIndex K L

The ramification index is positive.

@[simp]

theorem TauCeti.normalizedValuation_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (x : Kˣ) : (normalizedValuation L) ((Units.map ↑(algebraMap K L)) x) = (normalizedValuation K) x ^ ramificationIndex K L

The characteristic property of the ramification index: the normalized valuation of L restricted to Kˣ is the e-th power of the normalized valuation of K, that is v_L(x) = e · v_K(x).

theorem TauCeti.toAdd_normalizedValuation_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (x : Kˣ) : Multiplicative.toAdd ((normalizedValuation L) ((Units.map ↑(algebraMap K L)) x)) = ↑(ramificationIndex K L) * Multiplicative.toAdd ((normalizedValuation K) x)

The characteristic property of the ramification index in additive form: v_L(x) = e · v_K(x) for x : Kˣ.

theorem TauCeti.natCastValuation_eq_ramificationIndex_mul {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (n : ℕ) (hn : ↑n ≠ 0) : natCastValuation L n ⋯ = ramificationIndex K L * natCastValuation K n hn

The characteristic property of the ramification index on natural numbers: the normalized valuation of a natural number in L is e(L/K) times its normalized valuation in K.

@[simp]

theorem TauCeti.normalizedValuationWithZero_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (x : K) : (normalizedValuationWithZero L) ((algebraMap K L) x) = (normalizedValuationWithZero K) x ^ ramificationIndex K L

The characteristic property of the ramification index for the zero-preserving normalized valuations, on all of K.

theorem TauCeti.ramificationIndex_eq_iff {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {n : ℕ} : ramificationIndex K L = n ↔ ∀ (x : Kˣ), (normalizedValuation L) ((Units.map ↑(algebraMap K L)) x) = (normalizedValuation K) x ^ n

The ramification index is the only natural number n with v_L(x) = n · v_K(x) for all x : Kˣ.

theorem TauCeti.normalizedValuation_algebraMap_irreducible {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) : (normalizedValuation L) ((Units.map ↑(algebraMap K L)) (Units.mk0 ↑π ⋯)) = Multiplicative.ofAdd ↑(ramificationIndex K L)

The image in L of any uniformizer of K has normalized valuation e(L/K).

theorem TauCeti.valuation_algebraMap_irreducible {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {πK : ↥(ValuativeRel.valuation K).integer} (hπK : Irreducible πK) {πL : ↥(ValuativeRel.valuation L).integer} (hπL : Irreducible πL) : (ValuativeRel.valuation L) ((algebraMap K L) ↑πK) = (ValuativeRel.valuation L) ↑πL ^ ramificationIndex K L

The valuation in L of a uniformizer π_K of K is the e(L/K)-th power of the valuation of a uniformizer π_L of L.

@[simp]

theorem TauCeti.addVal_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (a : ↥(ValuativeRel.valuation K).integer) : (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) ((algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) a) = ramificationIndex K L • (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) a

The additive valuation on the integer ring scales under the algebra map by the ramification index.

theorem TauCeti.addVal_sum_algebraMap_mul_pow_of_irreducible {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) {n : ℕ} (hn : n ≤ ramificationIndex K L) (c : Fin n → ↥(ValuativeRel.valuation K).integer) : (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (∑ i : Fin n, (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) (c i) * ϖ ^ ↑i) = ⨅ (i : Fin n), ramificationIndex K L • (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) (c i) + ↑↑i

Orthogonality of the powers of a uniformizer. For a uniformizer ϖ of L and coefficients c i ∈ 𝒪[K] indexed by i < n ≤ e(L/K), the terms c i * ϖ ^ i have additive valuations e(L/K) v_K(c i) + i in distinct classes modulo e(L/K), so the additive valuation of their sum is the least term valuation.

theorem TauCeti.map_maximalIdeal_eq_maximalIdeal_pow (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Ideal.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ ramificationIndex K L

The maximal ideal of 𝒪[K] generates the e(L/K)-th power of the maximal ideal of 𝒪[L]. This is the ideal-theoretic form of the characteristic property of the ramification index.

theorem TauCeti.ramificationIndex_eq_ramificationIdx (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : ramificationIndex K L = (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer).ramificationIdx ↥(ValuativeRel.valuation K).integer

The intrinsic ramification index is the ideal-theoretic one: the index of the image of the normalized value group is the ramification index of 𝓂[L] over 𝒪[K].

theorem TauCeti.ramificationIndex_tower {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] : ramificationIndex K M = ramificationIndex K L * ramificationIndex L M

Multiplicativity of the ramification index in a tower M/L/K: e(M/K) = e(L/K) · e(M/L).

theorem TauCeti.isTamelyRamified_tower_iff {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] : IsTamelyRamified K M ↔ IsTamelyRamified K L ∧ IsTamelyRamified L M

A tower of nonarchimedean local fields is tamely ramified exactly when each of its two steps is tamely ramified. The residue characteristics of K and L agree, and their ramification indices multiply.

theorem TauCeti.isTamelyRamified_iff_isUnit_natCast (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsTamelyRamified K L ↔ IsUnit ↑(ramificationIndex K L)

An extension is tamely ramified exactly when its ramification index is a unit in the integer ring 𝒪[L], the form in which tameness enters Hensel-type arguments in L.