The Galois-equivariant valuation sequence

For a finite extension of nonarchimedean local fields L/K, normalized valuation gives the short exact sequence 0 → U(L,0) → Lˣ → ℤ → 0 of integral Galois representations, with trivial action on ℤ. All multiplicative coefficient groups are read through Additive.

For a cyclic extension, Hilbert 90 and two-periodicity make degree minus one of Lˣ vanish. The valuation sequence then shows that degree minus one of U(L,0) is finite, and gives h(Lˣ) = [L : K] * h(U(L,0)) when the extension is Galois. Thus the local unit calculation h(U(L,0)) = 1 transfers to the multiplicative group without choosing a Galois-invariant uniformizer, which generally does not exist.

Together with the unit quotient calculation and cyclic two-periodicity, this relation gives the order of the relative Brauer group for a cyclic extension. That order calculation is an input to identifying the full Brauer group with its unramified classes, which in turn allows the unramified invariant to extend to the full local invariant.

The constructions reuse the kernel and surjectivity of TauCeti.normalizedValuation, and Mathlib's groupCohomology.H1ofAutOnUnitsUnique (Riccardo Brasca and Amelia Livingston).

References

• Romyar Sharifi, Algebraic Number Theory, proof of Theorem 9.1.13 and Definition 9.1.14: https://www.math.ucla.edu/~sharifi/notes/algnum-ch09.html

theorem TauCeti.coe_norm_unitFiltrationZero (K L : Type) [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] (x : ↑(Rep.ofMulDistribMulAction Gal(L/K) ↥(unitFiltration L 0))) : ↑↑(Additive.toMul (Rep.toAdditive ((Rep.Hom.hom (Rep.ofMulDistribMulAction Gal(L/K) ↥(unitFiltration L 0)).norm.asHom) x))) = (algebraMap K L) ((Algebra.norm K) ↑↑(Additive.toMul (Rep.toAdditive x)))

On the valuation-zero units of a Galois extension, the representation norm of Gal(L/K) is the field norm.

noncomputable def TauCeti.unitsValuationHom (K L : Type) [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] : Rep.ofMulDistribMulAction Gal(L/K) Lˣ ⟶ Rep.trivial ℤ Gal(L/K) ℤ

Normalized valuation as a morphism from the multiplicative Galois representation to the trivial integral representation.

@[simp]

theorem TauCeti.unitsValuationHom_apply (K L : Type) [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] (x : ↑(Rep.ofMulDistribMulAction Gal(L/K) Lˣ)) : (Rep.Hom.hom (unitsValuationHom K L)) x = Multiplicative.toAdd ((normalizedValuation L) (Additive.toMul (Rep.toAdditive x)))

The valuation morphism evaluates to the additive normalized valuation.

@[simp]

theorem TauCeti.unitsValuationHom_eq_zero_iff (K L : Type) [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] (x : ↑(Rep.ofMulDistribMulAction Gal(L/K) Lˣ)) : (Rep.Hom.hom (unitsValuationHom K L)) x = 0 ↔ Additive.toMul (Rep.toAdditive x) ∈ unitFiltration L 0

An element has valuation zero exactly when it lies in the zeroth unit-filtration group.

@[simp]

theorem TauCeti.unitFiltrationZeroIncl_comp_unitsValuationHom (K L : Type) [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] : CategoryTheory.CategoryStruct.comp (unitFiltrationZeroIncl K L) (unitsValuationHom K L) = 0

The inclusion of valuation-zero units followed by normalized valuation vanishes.

@[simp]

theorem TauCeti.unitFiltrationZeroIncl_comp_unitsValuationHom_assoc (K L : Type) [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] {Z : Rep.{0, 0, 0} ℤ Gal(L/K)} (h : Rep.trivial ℤ Gal(L/K) ℤ ⟶ Z) : CategoryTheory.CategoryStruct.comp (unitFiltrationZeroIncl K L) (CategoryTheory.CategoryStruct.comp (unitsValuationHom K L) h) = CategoryTheory.CategoryStruct.comp 0 h

The inclusion of valuation-zero units followed by normalized valuation vanishes.

noncomputable def TauCeti.unitsValuationSequence (K L : Type) [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] : CategoryTheory.ShortComplex (Rep.{0, 0, 0} ℤ Gal(L/K))

The canonical valuation short complex of integral Galois representations. The last term has trivial action; the sequence need not split as Galois representations. The body is exposed so that connecting maps can be formed at its stated coefficient objects.

@[simp]

theorem TauCeti.unitsValuationSequence_f (K L : Type) [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] : (unitsValuationSequence K L).f = unitFiltrationZeroIncl K L

The first map of the valuation sequence is the inclusion of U(L,0).

@[simp]

theorem TauCeti.unitsValuationSequence_g (K L : Type) [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] : (unitsValuationSequence K L).g = unitsValuationHom K L

The last map of the valuation sequence is normalized valuation.

theorem TauCeti.unitsValuationSequence_def (K L : Type) [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] : unitsValuationSequence K L = { X₁ := Rep.ofMulDistribMulAction Gal(L/K) ↥(unitFiltration L 0), X₂ := Rep.ofMulDistribMulAction Gal(L/K) Lˣ, X₃ := Rep.trivial ℤ Gal(L/K) ℤ, f := unitFiltrationZeroIncl K L, g := unitsValuationHom K L, zero := ⋯ }

The coefficient objects of the valuation sequence are U(L,0), Lˣ, and trivial ℤ.

theorem TauCeti.unitsValuationSequence_shortExact (K L : Type) [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] : (unitsValuationSequence K L).ShortExact

The valuation sequence 0 → U(L,0) → Lˣ → ℤ → 0 is short exact in integral Galois representations for every finite compatible extension of local fields.

instance TauCeti.finite_tateCohomology_negOne_unitFiltration_zero (K L : Type) [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] [IsCyclic Gal(L/K)] : Finite ↑(tateCohomology (Rep.ofMulDistribMulAction Gal(L/K) ↥(unitFiltration L 0)) (-1))

Degree-minus-one Tate cohomology of the valuation-zero units is finite.

theorem TauCeti.herbrandQuotient_units_eq_card_mul (K L : Type) [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] [IsCyclic Gal(L/K)] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) = ↑(Nat.card Gal(L/K)) * TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) ↥(unitFiltration L 0))

The valuation sequence transfers the Herbrand quotient of the unit group to the multiplicative group, with factor the order of the automorphism group.

theorem TauCeti.herbrandQuotient_units_eq_finrank_mul (K L : Type) [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] [IsCyclic Gal(L/K)] [IsGalois K L] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) = ↑(Module.finrank K L) * TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) ↥(unitFiltration L 0))

For a cyclic Galois extension, the multiplicative-group Herbrand quotient is the degree of the extension times the unit-group Herbrand quotient.