English
Noether–Hilbert 90 generalizes: the first cohomology H^1(Aut_K(L), L^×) is trivial; equivalently, the group of 1-cocycles modulo coboundaries is zero for the automorphism group acting on units of L.
Русский
Обобщение Ноттера–Гильберта 90: первая когомология H^1(Aut_K(L), L^×) тривиальна; то есть все 1‑кок cycles являются градиентами coboundary.
LaTeX
$$$H^1(\mathrm{Aut}_K(L), L^{\times}) = 0$ (trivial).$$
Lean4
/-- 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).` -/
theorem isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units (f : (L ≃ₐ[K] L) → Lˣ) (hf : IsMulCocycle₁ f) :
IsMulCoboundary₁ f := by
/- Let `z : L` be such that `∑ f(h) * h(z) ≠ 0`, for `h ∈ Aut_K(L)` -/
obtain ⟨z, hz⟩ : ∃ z, aux f z ≠ 0 := not_forall.1 (fun H => aux_ne_zero f <| funext <| fun x => H x)
have : aux f z = ∑ h, f h * h z := by
simp [aux, Finsupp.linearCombination, Finsupp.sum_fintype]
/- Let `β = (∑ f(h) * h(z))⁻¹.` -/
use (Units.mk0 (aux f z) hz)⁻¹
intro g
simp only [IsMulCocycle₁, AlgEquiv.smul_units_def, map_inv, div_inv_eq_mul, inv_mul_eq_iff_eq_mul, Units.ext_iff,
this, Units.val_mul, Units.coe_map, Units.val_mk0, MonoidHom.coe_coe] at hf ⊢
simp_rw [map_sum, map_mul, Finset.sum_mul, mul_assoc, mul_comm _ (f _ : L), ← mul_assoc, ← hf g]
exact eq_comm.1 (Fintype.sum_bijective (fun i => g * i) (Group.mulLeft_bijective g) _ _ (fun i => rfl))
