Norm indices around a prime-degree ramification break

For a finite Galois extension L/K, the cokernel of the graded norm at depth v measures the relative index

[U(K,v) : N(U(L, ψℕ(v))) · U(K,v+1)].

This file identifies these two indices, using the image of the norm in the successive unit quotient. For an extension of prime degree ℓ with an upper break at a natural number t, the relative index is 1 at every depth v ≠ t, and is ℓ at depth t, including the tame break at zero. These are the finite-step norm indices used in conductor computations.

The product of the two subgroups is written as their join: the unit group is commutative. The statements concern norms modulo the next unit step; they do not assert surjectivity of the norm onto an entire step of the unit filtration.

Main results

• TauCeti.relIndex_normUnits_unitFiltration_sup_eq_index_range_normGradedMap: the relative index is the index of the image of the graded norm.
• TauCeti.relIndex_normUnits_unitFiltration_sup_before_break: the index is 1 before a prime-degree break.
• TauCeti.relIndex_normUnits_unitFiltration_sup_at_break: the index at the break is the degree.
• TauCeti.relIndex_normUnits_unitFiltration_sup_after_break: the index is 1 above the break.

References

• J.-P. Serre, Corps Locaux, Chapter V, §3, Proposition 5 and its corollaries.

theorem TauCeti.range_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 : ℕ) : (normGradedMap K L v).range = Subgroup.map (QuotientGroup.mk' ((unitFiltration K (v + 1)).subgroupOf (unitFiltration K v))) ((Subgroup.map (Algebra.normUnits K) (unitFiltration L (LocalFieldsRamification.psiNat K L v))).subgroupOf (unitFiltration K v))

The image of the graded norm is the image, in the successive unit quotient, of the norm subgroup at the Herbrand-shifted depth.

theorem TauCeti.relIndex_normUnits_unitFiltration_sup_eq_index_range_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 : ℕ) : (Subgroup.map (Algebra.normUnits K) (unitFiltration L (LocalFieldsRamification.psiNat K L v)) ⊔ unitFiltration K (v + 1)).relIndex (unitFiltration K v) = (normGradedMap K L v).range.index

The cokernel index of the graded norm equals the index in U(K,v) of the product of N(U(L, ψℕ(v))) with U(K,v+1). This holds for every finite Galois extension.

theorem TauCeti.relIndex_normUnits_unitFiltration_sup_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, ⋯⟩) : (Subgroup.map (Algebra.normUnits K) (unitFiltration L (LocalFieldsRamification.psiNat K L v)) ⊔ unitFiltration K (v + 1)).relIndex (unitFiltration K v) = 1

In prime degree, before an upper break at t, every unit of depth v < t is congruent, modulo U(K,v+1), to a norm from depth ψℕ(v). Equivalently, the relative norm index is 1. This includes depth zero when the break is positive.

theorem TauCeti.relIndex_normUnits_unitFiltration_sup_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 : ℕ} (ht : LocalFieldsRamification.UpperJump K L ⟨↑t, ⋯⟩) : (Subgroup.map (Algebra.normUnits K) (unitFiltration L (LocalFieldsRamification.psiNat K L t)) ⊔ unitFiltration K (t + 1)).relIndex (unitFiltration K t) = Module.finrank K L

In a Galois extension of prime degree ℓ with an upper break at a natural number t, the norms from U(L, ψℕ(t)), together with U(K,t+1), have index ℓ in U(K,t). At the tame break t = 0 this is the residue-unit power map; at a positive break it is the additive polynomial on the residue field whose kernel and cokernel have order ℓ. Total ramification follows from the existence of the break.

theorem TauCeti.relIndex_normUnits_unitFiltration_sup_after_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 : t < v) (ht : LocalFieldsRamification.UpperJump K L ⟨↑t, ⋯⟩) : (Subgroup.map (Algebra.normUnits K) (unitFiltration L (LocalFieldsRamification.psiNat K L v)) ⊔ unitFiltration K (v + 1)).relIndex (unitFiltration K v) = 1

In prime degree, above an upper break at t, every unit of depth v > t is congruent, modulo U(K,v+1), to a norm from depth ψℕ(v). Equivalently, the relative norm index is 1.