Hilbert's Theorem 90

Let L/K be a finite extension of fields. Then this file proves Noether's generalization of Hilbert's Theorem 90: that the 1st group cohomology $H^1(Aut_K(L), L^\times)$ is trivial. We state it both in terms of $H^1$ and in terms of cocycles being coboundaries.

Hilbert's original statement was that if $L/K$ is Galois, and $Gal(L/K)$ is cyclic, generated by an element σ, then for every x : L such that $N_{L/K}(x) = 1,$ there exists y : L such that $x = y/σ(y).$ This can be deduced from the fact that the function $Gal(L/K) → L^\times$ sending $σ^i \mapsto xσ(x)σ^2(x)...σ^{i-1}(x)$ is a 1-cocycle. Alternatively, we can derive it by analyzing the cohomology of finite cyclic groups in general.

Noether's generalization also holds for infinite Galois extensions.

Main statements

• groupCohomology.isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units: Noether's generalization of Hilbert's Theorem 90: for all $f: Aut_K(L) \to L^\times$ satisfying the 1-cocycle condition, there exists β : Lˣ such that $g(β)/β = f(g)$ for all g : Aut_K(L).
• groupCohomology.H1ofAutOnUnitsUnique: Noether's generalization of Hilbert's Theorem 90: $H^1(Aut_K(L), L^\times)$ is trivial.

Implementation notes

Given a commutative ring k and a group G, group cohomology is developed in terms of k-linear G-representations on k-modules. Therefore stating Noether's generalization of Hilbert 90 in terms of H¹ requires us to turn the natural action of Aut_K(L) on Lˣ into a morphism Aut_K(L) →* (Additive Lˣ →ₗ[ℤ] Additive Lˣ). Thus we provide the non-H¹ version too, as its statement is clearer.

TODO

• The original Hilbert's Theorem 90, deduced from the cohomology of general finite cyclic groups.
• Develop Galois cohomology to extend Noether's result to infinite Galois extensions.
• "Additive Hilbert 90": let L/K be a finite Galois extension. Then $H^n(Gal(L/K), L)$ is trivial for all $1 ≤ n.$

noncomputable def groupCohomology.Hilbert90.aux {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (f : (L ≃ₐ[K] L) → Lˣ) : L → L

Given f : Aut_K(L) → Lˣ, the sum ∑ f(φ) • φ for φ ∈ Aut_K(L), as a function L → L.

Equations

• groupCohomology.Hilbert90.aux f = (Finsupp.linearCombination L fun (φ : L ≃ₐ[K] L) => ⇑φ) (Finsupp.equivFunOnFinite.symm fun (φ : L ≃ₐ[K] L) => ↑(f φ))

theorem groupCohomology.Hilbert90.aux_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (f : (L ≃ₐ[K] L) → Lˣ) : aux f ≠ 0

theorem groupCohomology.isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (f : (L ≃ₐ[K] L) → Lˣ) (hf : IsMulOneCocycle f) : IsMulOneCoboundary f

Noether's generalization of Hilbert's Theorem 90: given a finite extension of fields and a function f : Aut_K(L) → Lˣ satisfying f(gh) = g(f(h)) * f(g) for all g, h : Aut_K(L), there exists β : Lˣ such that g(β)/β = f(g) for all g : Aut_K(L).

noncomputable instance groupCohomology.H1ofAutOnUnitsUnique (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [DecidableEq (L ≃ₐ[K] L)] : Unique ↑(H1 (Rep.ofAlgebraAutOnUnits K L))

Noether's generalization of Hilbert's Theorem 90: given a finite extension of fields L/K, the first group cohomology H¹(Aut_K(L), Lˣ) is trivial.

Equations

• groupCohomology.H1ofAutOnUnitsUnique K L = { default := 0, uniq := ⋯ }