H1ofAutOnUnitsUnique — Mathlib

English

If f is a Mul-cocycle for Aut_K(L) with values in L^×, then f is a coboundary; i.e., there exists β ∈ L^× with f(g) = g(β)/β for all g.

Русский

Если f является муль кококycle на автоморфизмах, то существует β ∈ L^×: f(g) = g(β)/β для всех g.

LaTeX

$$$\exists \beta \in L^{\times}\text{ s.t. } f(g)=g(\beta)/\beta \;\forall g\in Aut_K(L).$$$

Lean4

/-- 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. -/
noncomputable instance H1ofAutOnUnitsUnique : Unique (H1 (Rep.ofAlgebraAutOnUnits K L))
    where
  default := 0
  uniq := fun a =>
    H1_induction_on a fun x =>
      (H1π_eq_zero_iff _).2 <| by
        refine (coboundariesOfIsMulCoboundary₁ ?_).2
        rcases isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units x.1 (isMulCocycle₁_of_mem_cocycles₁ _ x.2) with ⟨β, hβ⟩
        use β

Похожие утверждения