The norm on the graded pieces of the unit filtration

Let L/K be a finite Galois extension of nonarchimedean local fields, and let ψℕ_{L/K} : ℕ → ℕ be its integral inverse Herbrand function. The norm carries U(L, ψℕ_{L/K}(v)) into U(K, v) and U(L, ψℕ_{L/K}(v) + 1) into U(K, v + 1), so it induces a homomorphism of graded pieces

normGradedMap K L v : U(L, ψℕ_{L/K}(v)) / U(L, ψℕ_{L/K}(v) + 1) →* U(K, v) / U(K, v + 1).

For a Galois extension of prime degree these maps compare the unit filtrations of L and K step by step, and the orders of their kernels and cokernels are what the conductor and the Hasse–Arf theorem are computed from. This file computes them away from the break and at a positive break.

Depth zero. For a totally ramified Galois extension of degree n, ψℕ_{L/K}(0) = 0, both graded pieces are the multiplicative groups of the residue fields, and these residue fields coincide. Every element of the Galois group lies in the inertia group, so it acts trivially on the residue field, and the norm N(u) = ∏_σ σ(u) of a unit u reduces to ū ^ n. Thus normGradedMap K L 0 is the n-th power map of the cyclic group 𝓀ˣ of order q - 1, and its kernel and cokernel both have order gcd(q - 1, n). If L/K is tamely ramified, then n divides q - 1, because the inertia group, of order n, embeds into 𝓀ˣ through the tame character; so the kernel and the cokernel have order n. If instead G_1 = Gal(L/K), then n is a power of the residue characteristic p, which is prime to q - 1, and the map is bijective.

Before the break. Let L/K have prime degree and let v > 0 satisfy G_{v+1} = Gal(L/K). Then ψℕ_{L/K}(v) = v, and Hilbert's formula gives d(L/K) ≥ (v + 2)([L : K] - 1), so the trace carries 𝓂[L] ^ v into 𝓂[K] ^ (v + 1). In the expansion N(1 + z) = 1 + Tr(z) + Tr(y) + N(z) of TauCeti.exists_norm_one_add_eq_of_mem_maximalIdeal_pow only N(z) survives modulo 𝓂[K] ^ (v + 1), and the norm preserves valuations in a totally ramified extension. So normGradedMap K L v is injective, and it is bijective because both graded pieces have q elements.

At the break. Let L/K have prime degree ℓ, let t > 0 satisfy G_t = Gal(L/K), and let σ ∉ G_{t+1}, so that σ π - π = γ π ^ (t + 1) for a uniformizer π of L and an integer γ whose residue c is nonzero. Coordinatize U(L, t) / U(L, t + 1) by π and U(K, t) / U(K, t + 1) by N(π). Here ψℕ_{L/K}(t) = t, and the trace carries 𝓂[L] ^ (t + 1) into 𝓂[K] ^ (t + 1), so the expansion of N(1 + a π ^ t) gives the class of a ^ ℓ + β a for a constant β, the residue of Tr(π ^ t) / N(π) ^ t. The unit σ π / π has coordinate c and norm 1, so c ^ ℓ + β c = 0, which forces β = -c ^ (ℓ - 1): the graded norm is y ↦ y ^ ℓ - c ^ (ℓ - 1) y. When t is the break of the filtration, the Galois group is G_1, a p-group of order ℓ, so ℓ = p, and the kernel of this map is the line 𝔽_ℓ c. Hence the kernel and the cokernel of normGradedMap K L t both have order ℓ.

Main definitions

• TauCeti.normGradedMap: the homomorphism of graded pieces induced by the norm.

Main results

• TauCeti.algebraMap_residue_norm_of_isTotallyRamified: in a totally ramified Galois extension of degree n, the norm of an integer z reduces to the n-th power of the residue of z.
• TauCeti.algebraMap_unitFiltrationGradedZeroEquivResidueFieldUnits_normGradedMap_mk: the depth-zero graded norm is the n-th power map on residue units.
• TauCeti.natCard_ker_normGradedMap_zero and TauCeti.index_range_normGradedMap_zero: its kernel and its cokernel have order gcd(q - 1, n); TauCeti.normGradedMap_zero_bijective_iff: it is bijective exactly when n is prime to q - 1.
• TauCeti.normGradedMap_tame_break_zero: in the tame case both have order n.
• TauCeti.normGradedMap_zero_bijective_of_lowerRamificationGroup_one_eq_top: if G_1 = Gal(L/K), the depth-zero graded norm is bijective.
• TauCeti.normGradedMap_bijective_of_lowerRamificationGroup_eq_top: in prime degree, the graded norm at depth v is bijective whenever G_{v+1} = Gal(L/K).
• TauCeti.normGradedMap_zero_before_break and TauCeti.normGradedMap_positive_before_break: in prime degree with an upper break at a natural number t, the graded norm is bijective at every depth v < t.
• TauCeti.algebraMap_residue_eq_of_norm_one_add_mul_pow_eq and TauCeti.algebraMap_unitFiltrationGradedSuccEquivResidueFieldOfUniformizer_normGradedMap_mk: in prime degree, at a positive depth t with G_t = Gal(L/K) and for σ ∉ G_{t+1}, the graded norm is y ↦ y ^ ℓ - c ^ (ℓ - 1) y, where c is the coordinate of σ π / π.
• TauCeti.normGradedMap_at_break: in prime degree ℓ with an upper break at a natural number t > 0, the kernel and the cokernel of the graded norm at depth t both have order ℓ.

References

• J.-P. Serre, Corps Locaux, Chapter V, §3 (Lemmas 4 and 5, Proposition 5).

The graded norm map

noncomputable def TauCeti.normGradedMap (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] [Module.Finite K L] [IsGalois K L] (v : ℕ) : UnitFiltrationGraded L (LocalFieldsRamification.psiNat K L v) →* UnitFiltrationGraded K v

The norm on the Herbrand-shifted graded pieces of the unit filtration. For a finite Galois extension L/K of nonarchimedean local fields, the norm induces a homomorphism U(L, ψℕ_{L/K}(v)) / U(L, ψℕ_{L/K}(v) + 1) →* U(K, v) / U(K, v + 1), by the Herbrand-shifted inclusions TauCeti.map_normUnits_unitFiltration_psiNat_le and TauCeti.map_normUnits_unitFiltration_psiNat_add_one_le.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.normGradedMap_mk {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] [Module.Finite K L] [IsGalois K L] {v : ℕ} (x : ↥(unitFiltration L (LocalFieldsRamification.psiNat K L v))) : (normGradedMap K L v) ↑x = ↑⟨(Algebra.normUnits K) ↑x, ⋯⟩

The graded norm map sends the class of x to the class of its norm.

The norm modulo the maximal ideal in a totally ramified extension

theorem TauCeti.algebraMap_residue_norm_of_isTotallyRamified {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] [Module.Finite K L] [IsGalois K L] (h : IsTotallyRamified K L) (z : ↥(ValuativeRel.valuation L).integer) : (algebraMap (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)) ((IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) ((Algebra.norm ↥(ValuativeRel.valuation K).integer) z)) = (IsLocalRing.residue ↥(ValuativeRel.valuation L).integer) z ^ Module.finrank K L

The norm modulo the maximal ideal in a totally ramified extension. If L/K is a totally ramified Galois extension of nonarchimedean local fields, the norm of an integer z of L reduces to the [L : K]-th power of the residue of z: every conjugate of z has the residue of z.

The graded norm at depth zero

theorem TauCeti.algebraMap_unitFiltrationGradedZeroEquivResidueFieldUnits_normGradedMap_mk {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] [Module.Finite K L] [IsGalois K L] (h : IsTotallyRamified K L) (x : ↥(unitFiltration L (LocalFieldsRamification.psiNat K L 0))) : (algebraMap (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)) ↑(unitFiltrationGradedZeroEquivResidueFieldUnits ((normGradedMap K L 0) ↑x)) = (IsLocalRing.residue ↥(ValuativeRel.valuation L).integer) ↑((unitFiltrationToIntegerUnits (LocalFieldsRamification.psiNat K L 0)) x) ^ Module.finrank K L

The graded norm at depth zero is the [L : K]-th power map. For a totally ramified Galois extension L/K of nonarchimedean local fields, read through the identifications of the depth-zero graded pieces with the residue units, the norm sends the class of a unit x of 𝒪[L] to the [L : K]-th power of its residue.

theorem TauCeti.natCard_ker_normGradedMap_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] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] (h : IsTotallyRamified K L) : Nat.card ↥(normGradedMap K L 0).ker = (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) - 1).gcd (Module.finrank K L)

The kernel of the graded norm at depth zero. For a totally ramified Galois extension L/K of nonarchimedean local fields, with residue field of cardinality q, the kernel of normGradedMap K L 0 has order gcd(q - 1, [L : K]).

theorem TauCeti.index_range_normGradedMap_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] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] (h : IsTotallyRamified K L) : (normGradedMap K L 0).range.index = (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) - 1).gcd (Module.finrank K L)

The cokernel of the graded norm at depth zero. For a totally ramified Galois extension L/K of nonarchimedean local fields, with residue field of cardinality q, the image of normGradedMap K L 0 has index gcd(q - 1, [L : K]).

theorem TauCeti.normGradedMap_zero_bijective_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] [Module.Finite K L] [IsGalois K L] (h : IsTotallyRamified K L) : Function.Bijective ⇑(normGradedMap K L 0) ↔ (Module.finrank K L).Coprime (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) - 1)

The graded norm at depth zero is bijective exactly in the coprime case. For a totally ramified Galois extension L/K of nonarchimedean local fields, with residue field of cardinality q, the map normGradedMap K L 0 is bijective if and only if [L : K] is prime to q - 1.

The tame case

theorem TauCeti.normGradedMap_tame_break_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] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] (h : IsTotallyRamified K L) (ht : IsTamelyRamified K L) : Nat.card ↥(normGradedMap K L 0).ker = Module.finrank K L ∧ (normGradedMap K L 0).range.index = Module.finrank K L

The tame break at zero. For a totally and tamely ramified Galois extension L/K of nonarchimedean local fields, the kernel of the graded norm normGradedMap K L 0 has order [L : K], and its image has index [L : K]. In prime degree this is the regime v = t = 0, the tame case, in which the unique break t of the ramification filtration is 0.

Before the break

theorem TauCeti.normGradedMap_zero_bijective_of_lowerRamificationGroup_one_eq_top {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] [Module.Finite K L] [IsGalois K L] (hG : LocalFieldsRamification.lowerRamificationGroup K L 1 = ⊤) : Function.Bijective ⇑(normGradedMap K L 0)

Depth zero in a totally wildly ramified extension. If the first ramification group of a finite Galois extension L/K of nonarchimedean local fields is the whole Galois group, G_1 = Gal(L/K), then the graded norm normGradedMap K L 0 is bijective: L/K is then totally ramified of degree a power of the residue characteristic p, which is prime to q - 1.

theorem TauCeti.normGradedMap_bijective_of_lowerRamificationGroup_eq_top {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] [Module.Finite K L] [IsGalois K L] (hℓ : Nat.Prime (Module.finrank K L)) {v : ℕ} (hG : LocalFieldsRamification.lowerRamificationGroup K L (↑v + 1) = ⊤) : Function.Bijective ⇑(normGradedMap K L v)

Before the break, the graded norm is bijective. Let L/K be a Galois extension of nonarchimedean local fields of prime degree, and let v : ℕ lie strictly before the break of its lower ramification filtration, G_{v+1} = Gal(L/K). Then the graded norm normGradedMap K L v is bijective.

Before a positive break, in prime degree

theorem TauCeti.normGradedMap_zero_before_break {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] [Module.Finite K L] [IsGalois K L] (hℓ : Nat.Prime (Module.finrank K L)) {t : ℕ} (ht0 : 0 < t) (ht : LocalFieldsRamification.UpperJump K L ⟨↑t, ⋯⟩) : Function.Bijective ⇑(normGradedMap K L 0)

Depth zero before a positive break. Let L/K be a Galois extension of nonarchimedean local fields of prime degree whose upper ramification filtration breaks at a natural number t > 0. Then the graded norm normGradedMap K L 0 is bijective. This is the regime v = 0 < t, in which L/K is totally ramified of degree the residue characteristic p.

theorem TauCeti.normGradedMap_positive_before_break {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] [Module.Finite K L] [IsGalois K L] (hℓ : Nat.Prime (Module.finrank K L)) {v t : ℕ} (hvt : v < t) (ht : LocalFieldsRamification.UpperJump K L ⟨↑t, ⋯⟩) : Function.Bijective ⇑(normGradedMap K L v)

Before the break, the graded norm is bijective. Let L/K be a Galois extension of nonarchimedean local fields of prime degree whose upper ramification filtration breaks at a natural number t. Then the graded norm normGradedMap K L v is bijective at every depth v < t. The regime 0 < v < t is the one this result is named for; the depth v = 0 is also TauCeti.normGradedMap_zero_before_break.

At a positive break, in prime degree

theorem TauCeti.algebraMap_residue_eq_of_norm_one_add_mul_pow_eq {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] [Module.Finite K L] [IsGalois K L] (hℓ : Nat.Prime (Module.finrank K L)) {t : ℕ} (ht0 : 0 < t) (hG : LocalFieldsRamification.lowerRamificationGroup K L ↑t = ⊤) {π : ↥(ValuativeRel.valuation L).integer} (hπ : Irreducible π) {σ : Gal(L/K)} (hσ : σ ∉ LocalFieldsRamification.lowerRamificationGroup K L (↑t + 1)) {γ : ↥(ValuativeRel.valuation L).integer} (hγ : σ • π - π = γ * π ^ (t + 1)) {a : ↥(ValuativeRel.valuation L).integer} {b : ↥(ValuativeRel.valuation K).integer} (hab : (Algebra.norm ↥(ValuativeRel.valuation K).integer) (1 + a * π ^ t) = 1 + b * (Algebra.norm ↥(ValuativeRel.valuation K).integer) π ^ t) : (algebraMap (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)) ((IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) b) = (IsLocalRing.residue ↥(ValuativeRel.valuation L).integer) a ^ Module.finrank K L - (IsLocalRing.residue ↥(ValuativeRel.valuation L).integer) γ ^ (Module.finrank K L - 1) * (IsLocalRing.residue ↥(ValuativeRel.valuation L).integer) a

The norm at the break. Let L/K be a Galois extension of nonarchimedean local fields of prime degree ℓ, let t > 0 satisfy G_t = Gal(L/K), and let σ ∉ G_{t+1}, so that σ π - π = γ π ^ (t + 1) for a uniformizer π of L. If N(1 + a π ^ t) = 1 + b N(π) ^ t, then the residue of b is y ^ ℓ - c ^ (ℓ - 1) y, where y and c are the residues of a and γ.

theorem TauCeti.algebraMap_unitFiltrationGradedSuccEquivResidueFieldOfUniformizer_normGradedMap_mk {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] [Module.Finite K L] [IsGalois K L] (hℓ : Nat.Prime (Module.finrank K L)) {t : ℕ} (hG : LocalFieldsRamification.lowerRamificationGroup K L (↑t + 1) = ⊤) {π : ↥(ValuativeRel.valuation L).integer} (hπ : Irreducible π) (hπK : Irreducible ((Algebra.norm ↥(ValuativeRel.valuation K).integer) π)) {σ : Gal(L/K)} (hσ : σ ∉ LocalFieldsRamification.lowerRamificationGroup K L (↑t + 2)) {γ : ↥(ValuativeRel.valuation L).integer} (hγ : σ • π - π = γ * π ^ (t + 2)) (x : ↥(unitFiltration L (LocalFieldsRamification.psiNat K L (t + 1)))) {a : ↥(ValuativeRel.valuation L).integer} (hxa : ↑↑x = 1 + ↑a * ↑π ^ (t + 1)) : (algebraMap (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)) ((unitFiltrationGradedSuccEquivResidueFieldOfUniformizer t ((Algebra.norm ↥(ValuativeRel.valuation K).integer) π) hπK) (Additive.ofMul ((normGradedMap K L (t + 1)) ↑x))) = (IsLocalRing.residue ↥(ValuativeRel.valuation L).integer) a ^ Module.finrank K L - (IsLocalRing.residue ↥(ValuativeRel.valuation L).integer) γ ^ (Module.finrank K L - 1) * (IsLocalRing.residue ↥(ValuativeRel.valuation L).integer) a

The graded norm at the break, in coordinates. Let L/K be a Galois extension of nonarchimedean local fields of prime degree ℓ with G_{t+1} = Gal(L/K), and let σ ∉ G_{t+2}, so that σ π - π = γ π ^ (t + 2) for a uniformizer π of L. Coordinatize U(L, t + 1) / U(L, t + 2) by π and U(K, t + 1) / U(K, t + 2) by the uniformizer N(π) of K. Then normGradedMap K L (t + 1) is y ↦ y ^ ℓ - c ^ (ℓ - 1) y, where c is the residue of γ, the coordinate of σ π / π.

theorem TauCeti.normGradedMap_at_break {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] [Module.Finite K L] [IsGalois K L] (hℓ : Nat.Prime (Module.finrank K L)) {t : ℕ} (ht0 : 0 < t) (ht : LocalFieldsRamification.UpperJump K L ⟨↑t, ⋯⟩) : Nat.card ↥(normGradedMap K L t).ker = Module.finrank K L ∧ (normGradedMap K L t).range.index = Module.finrank K L

The graded norm at a positive break. Let L/K be a Galois extension of nonarchimedean local fields of prime degree ℓ whose upper ramification filtration breaks at a natural number t > 0. Then the kernel of the graded norm normGradedMap K L t has order ℓ, and its image has index ℓ. This is the regime v = t > 0, in which L/K is totally ramified and ℓ is the residue characteristic.