theorem · Class Field Theory

The cyclic Hasse norm theorem

For a cyclic number-field extension, local norm equations have a global solution.

The theorem makes a global multiplicative equation testable at every finite and infinite completion. Cyclicity is essential: for more general extensions, an obstruction can remain even when every local norm test succeeds. This is a classical example of the local-to-global principle, treated by Milne through cyclic cohomology and idèle classes together with the limitations of the noncyclic case.

ClassFieldTheory on GitHub ↗

Mathematical statement

Let $L/K$ be a finite cyclic Galois extension of number fields and let $a\in K^\times$. Then

$$a\in N_{L/K}(L^\times)\quad\Longleftrightarrow\quad a\in N_{L\otimes_K K_v\,/\,K_v}\bigl((L\otimes_K K_v)^\times\bigr)\ \text{for every place }v.$$

The right side includes every finite and every infinite completion. The norm after base change is the determinant norm of the resulting finite algebra.

Lean code

`ClassFieldTheory.cyclicHasseNormTheorem`

Published library source ↗Same source in NYLL ↗

theorem cyclicHasseNormTheorem
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    (x : Kˣ) :
    IsFieldNorm K L x ↔ IsEverywhereLocalNorm K L x

In-scope Lean context

open scoped NumberField

namespace ClassFieldTheory

Full declaration and proof

/-- For a finite cyclic number-field extension, a unit is a global norm if
and only if it is a norm at every completion. -/
theorem cyclicHasseNormTheorem
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    (x : Kˣ) :
    IsFieldNorm K L x ↔ IsEverywhereLocalNorm K L x := by
  exact GlobalClassFieldTheory.ClassFieldAxiom.cyclicHasseNormTheorem K L x

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

J. S. Milne. Class Field Theory, version 4.03. 2020. Author's notes, dated 6 August 2020. Chapters I, III, V, VII, and VIII give complementary formulations and historical notes.

Published source: 26f52ca8.

← All selected results in Class Field Theory