Hilbert's Theorem 90 for cyclic extensions in every universe

Let L/K be a finite Galois extension whose Galois group is generated by g. Hilbert's Theorem 90 says that an element x of L of norm one is g y / y for a unit y of L.

Mathlib proves this as groupCohomology.exists_div_of_norm_eq_one through the cohomology of finite cyclic groups, which is set up for fields in Type. This file deduces the statement for fields in an arbitrary universe from Noether's form of Hilbert 90, groupCohomology.isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units, which is universe-polymorphic: when x has norm one, the partial products x · g x ⋯ g^{i-1} x depend only on gⁱ and form a multiplicative 1-cocycle.

Main results

• TauCeti.exists_smul_div_eq_iff_norm_eq_one: Hilbert's Theorem 90 for a cyclic Galois extension, together with its converse.

References

• J.-P. Serre, Local Fields, Chapter X, §1.

theorem TauCeti.exists_smul_div_eq_iff_norm_eq_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) {x : Lˣ} : (∃ (y : Lˣ), g • y / y = x) ↔ (Algebra.norm K) ↑x = 1

Hilbert's Theorem 90 for cyclic extensions. If g generates Gal(L/K), then a unit x of L has norm one if and only if x = g y / y for a unit y of L.