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).$ Using the fact that H¹(G, A) ≅ Ker(N_A)/(ρ(g) - 1)(A) for any finite cyclic group G with generator g, we deduce the original statement from Noether's generalization.

Noether's generalization also holds for infinite Galois extensions.

Main statements

• groupCohomology.isMulCoboundary₁_of_isMulCocycle₁_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.
• groupCohomology.exists_div_of_norm_eq_one: Hilbert's Theorem 90: given a finite cyclic Galois extension L/K, an element x : L such that N_{L/K}(x) = 1, and a generator g of Gal(L/K), there exists y : Lˣ such that y/g y = x.

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

• 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 : Gal(L/K) → 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 (φ : Gal(L/K)) => ⇑φ) (Finsupp.equivFunOnFinite.symm fun (φ : Gal(L/K)) => ↑(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 : Gal(L/K) → Lˣ) : aux f ≠ 0

theorem groupCohomology.isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (f : Gal(L/K) → Lˣ) (hf : IsMulCocycle₁ f) : IsMulCoboundary₁ 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] : 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 := ⋯ }

theorem groupCohomology.norm_ofAlgebraAutOnUnits_eq {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (x : Lˣ) : ↑(Additive.toMul (Rep.toAdditive ((CategoryTheory.ConcreteCategory.hom (Rep.ofAlgebraAutOnUnits K L).norm.hom) (Rep.toAdditive.symm (Additive.ofMul x))))) = (algebraMap K L) ((Algebra.norm K) ↑x)

Given L/K finite and Galois, and x : Lˣ, this essentially says (∏ σ) • x = N_{L/K}(x), where the product is over σ ∈ Gal(L/K).

theorem groupCohomology.exists_div_of_norm_eq_one {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {g : Gal(L/K)} (hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) {x : L} (hx : (Algebra.norm K) x = 1) : ∃ (y : Lˣ), ↑y / g ↑y = x

Hilbert's Theorem 90: given a finite cyclic Galois extension L/K, an element x : L such that N_{L/K}(x) = 1, and a generator g of Gal(L/K), there exists y : Lˣ such that y/g y = x.

theorem groupCohomology.exists_mul_galRestrict_of_norm_eq_one {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {g : Gal(L/K)} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K] [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsDomain A] [IsIntegralClosure B A L] (hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) {η : B} (hη : (Algebra.norm K) ((algebraMap B L) η) = 1) : ∃ (ε : B), ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε

The integral version of the classical formulation of Hilbert's theorem 90: in the ABKL setting, suppose that L/K is a finite Galois extension such that the Galois group is cyclic generated by g and let η : B be an element of norm 1 (when viewed as an element of L). Then there exists ε : B such that ε ≠ 0 and η * g ε = ε.