Unit norm indices and the conductor in prime degree

For a Galois extension of prime degree with upper ramification break at a natural number t, the norm of the whole integer-unit group has index equal to the degree. More generally, the norm from U(L, ψℕ(v)) has that same index in U(K,v) at every depth v ≤ t.

The intersection with the full unit norm group is determined by the unit filtration up to the break. Together with norm surjectivity above the break, this gives the sharp conductor criterion: U(K,v) is contained in the field norm group exactly when t < v. Thus the least natural unit depth contained in the norm group is t + 1. This includes a tame break at zero.

Since a prime-degree upper break is -1 or a natural number by the prime-degree case of Hasse--Arf, the criterion extends to every prime-degree upper break u: U(K,v) lies in the norm group exactly when u < v. At the unramified break -1 the conductor is zero.

Main results

• TauCeti.LocalFieldsRamification.UpperJump.unitFiltration_le_normGroup_iff_of_finrank_prime: the conductor criterion at any prime-degree upper break, including the unramified break -1.

References

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

theorem TauCeti.map_normUnits_unitFiltration_zero_inf_of_le_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 0) ⊓ unitFiltration K v = Subgroup.map (Algebra.normUnits K) (unitFiltration L (LocalFieldsRamification.psiNat K L v))

Up to a prime-degree break, the norms of integer units that lie in U(K,v) are exactly norms from the Herbrand-shifted step U(L, ψℕ(v)).

theorem TauCeti.relIndex_normUnits_unitFiltration_of_le_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))).relIndex (unitFiltration K v) = Module.finrank K L

At every depth up to a prime-degree upper break, the full norm image of the Herbrand-shifted unit step has relative index equal to the extension degree.

theorem TauCeti.relIndex_normUnits_unitFiltration_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ℓ : Nat.Prime (Module.finrank K L)) {t : ℕ} (ht : LocalFieldsRamification.UpperJump K L ⟨↑t, ⋯⟩) : (Subgroup.map (Algebra.normUnits K) (unitFiltration L 0)).relIndex (unitFiltration K 0) = Module.finrank K L

The norm image of the entire integer-unit group has index equal to the degree in a prime-degree Galois extension with a natural upper break.

theorem TauCeti.LocalFieldsRamification.UpperJump.unitFiltration_le_normGroup_iff_of_finrank_prime {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] {u : ↑RamificationIndexDomain} (hu : UpperJump K L u) (hdegree : Nat.Prime (Module.finrank K L)) (v : ℕ) : unitFiltration K v ≤ normGroup K L ↔ ↑u < ↑v

At an upper break of a prime-degree Galois extension, a unit-filtration step lies in the norm group exactly when its depth is strictly above the break. Thus the conductor is one more than the unique break; this is zero when the break is -1 in the unramified case.