English
In Noether’s generalization of Hilbert 90, for field extensions K ⊆ L of finite dimension and a function f with a cocycle property, the auxiliary element aux f is nonzero. This is a key step in constructing a multiplicative coboundary.
Русский
В общем случае Ноттерской обобщения теоремы Гильберта 90 для полей K ⊆ L конечной размерности существует элемент-помощник aux f, не равный нулю, при удовлетворении соответствующего кокула.
LaTeX
$$$\text{aux}_f \neq 0$ for suitable f, i.e., auxiliary element is nonzero.$$
Lean4
theorem aux_ne_zero (f : (L ≃ₐ[K] L) → Lˣ) : aux f ≠ 0 :=
/- the set `Aut_K(L)` is linearly independent in the `L`-vector space `L → L`, by Dedekind's
linear independence of characters -/
have : LinearIndependent L (fun (f : L ≃ₐ[K] L) => (f : L → L)) :=
LinearIndependent.comp (ι' := L ≃ₐ[K] L) (linearIndependent_monoidHom L L) (fun f => f)
(fun x y h => by ext; exact DFunLike.ext_iff.1 h _)
have h := linearIndependent_iff.1 this (Finsupp.equivFunOnFinite.symm (fun φ => (f φ : L)))
fun H => Units.ne_zero (f 1) (DFunLike.ext_iff.1 (h H) 1)
