The additive Hilbert 90

For a Galois extension L/K, finite or infinite, the first continuous cohomology of Gal(L/K) with coefficients in the additive group of L, carrying the discrete topology, vanishes:

H¹(Gal(L/K), L) = 0.

For a separable closure this is H¹(G_K, Kˢ) = 0. It is the additive companion of Hilbert 90, H¹(G_K, (Kˢ)ˣ) = 0 (TauCeti/FieldTheory/GaloisCohomology/Hilbert90.lean). The two vanishing theorems, in their form for explicit locally constant cocycles, are the inputs to the vanishing of the first Galois cohomology of the admissible changes of variables (u, r, s, t) of Weierstrass equations: the scaling u is a unit, and the changes with u = 1 are built from three copies of the additive group, one for each of r, s and t. That vanishing, which lets a Galois cocycle of changes of variables descend a Weierstrass equation, is WeierstrassCurve.VariableChange.exists_eq_mul_map_inv.

The finite case is Noether's argument with the sum over all K-automorphisms in place of a norm. For a finite extension L/K the automorphisms of L/K are linearly independent over L (Dedekind), so their sum is not identically zero: some z ∈ L has c = ∑_τ τ z ≠ 0, and c is fixed by every automorphism. For a 1-cocycle f, the cocycle identity f (σ τ) = σ (f τ) + f σ gives σ (∑_τ f τ · τ z) = ∑_τ f τ · τ z - f σ · c, so x = -(∑_τ f τ · τ z) / c satisfies σ x - x = f σ. The infinite case passes to finite layers, exactly as for Hilbert 90: every continuous class is inflated from a finite quotient Gal(L/K) ⧸ U, which is the Galois group of the finite Galois subextension fixed by U.

Main results

• TauCeti.isCoboundary₁_of_isCocycle₁_of_aut: for a finite extension L/K, every 1-cocycle Gal(L/K) → L is a coboundary.
• TauCeti.H1ofAutUnique: for a finite extension L/K, H¹(Gal(L/K), L) = 0 in Mathlib's group cohomology.
• TauCeti.isCoboundary₁_of_isCocycle₁_of_quotient_to_fixedPoints_forcedDiscrete: the additive Hilbert 90 at a finite layer Gal(L/K) ⧸ U, with coefficients in L^U.
• TauCeti.subsingleton_H1_forcedDiscrete: H¹(Gal(L/K), L) = 0 for any Galois L/K.
• TauCeti.isCoboundary₁_of_isCocycle₁_of_isLocallyConstant: the same for an explicit locally constant cocycle Gal(L/K) → L.
• TauCeti.subsingleton_H1_forcedDiscrete_separableClosure and TauCeti.additiveHilbert90: H¹(G_K, Kˢ) = 0, for the explicit and for Mathlib's canonical continuous cohomology.

References

• J.-P. Serre, Local Fields, X, §1, Proposition 1.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter VI, §1.

theorem TauCeti.isCoboundary₁_of_isCocycle₁_of_aut {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (f : Gal(L/K) → L) (hf : groupCohomology.IsCocycle₁ f) : groupCohomology.IsCoboundary₁ f

The additive Hilbert 90 for a finite extension. For a finite extension L/K, every function f : Gal(L/K) → L satisfying the 1-cocycle condition f (σ τ) = σ (f τ) + f σ is a coboundary: there is x : L with σ x - x = f σ for every σ. No separability is assumed: the group is the group of all automorphisms of L/K.

@[instance_reducible]

noncomputable instance TauCeti.H1ofAutUnique (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : Unique ↑(groupCohomology.H1 (Rep.ofAlgebraAut K L))

The additive Hilbert 90 for a finite extension, in Mathlib's group cohomology: the first group cohomology H¹(Gal(L/K), L) of the automorphism group of a finite extension L/K, acting on the additive group of L, is trivial.

theorem TauCeti.isCoboundary₁_of_isCocycle₁_of_quotient_to_fixedPoints_forcedDiscrete {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (U : OpenNormalSubgroup Gal(L/K)) {f : Gal(L/K) ⧸ ↑U.toOpenSubgroup → ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) (ForcedDiscrete L))} (hf : groupCohomology.IsCocycle₁ f) : groupCohomology.IsCoboundary₁ f

The additive Hilbert 90 at a finite layer of a Galois extension. For an open normal subgroup U of Gal(L/K), every 1-cocycle of the finite group Gal(L/K) ⧸ U with values in the invariants L^U is a coboundary. No continuity is assumed: the quotient is finite, and this is the finite-level vanishing of H¹(Gal(L/K) ⧸ U, L^U).

theorem TauCeti.subsingleton_H1_forcedDiscrete {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] : Subsingleton (ContCohomology.H1 Gal(L/K) (ForcedDiscrete L))

The additive Hilbert 90 for a Galois extension L/K, finite or not: the continuous H¹(Gal(L/K), L) vanishes, the additive group of L carrying the discrete topology. Every class is inflated from a finite layer, where it vanishes by TauCeti.isCoboundary₁_of_isCocycle₁_of_quotient_to_fixedPoints_forcedDiscrete.

theorem TauCeti.isCoboundary₁_of_isCocycle₁_of_isLocallyConstant {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] {f : Gal(L/K) → L} (hf : groupCohomology.IsCocycle₁ f) (hc : IsLocallyConstant f) : groupCohomology.IsCoboundary₁ f

The additive Hilbert 90 for explicit cocycles. For a Galois extension L/K, finite or not, every locally constant 1-cocycle f : Gal(L/K) → L, that is f (σ * τ) = σ (f τ) + f σ, is a coboundary: f σ = σ x - x for some x : L.

instance TauCeti.subsingleton_H1_forcedDiscrete_separableClosure (K : Type u_1) [Field K] : Subsingleton (ContCohomology.H1 (AbsoluteGaloisGroup K) (ForcedDiscrete (SeparableClosure K)))

The additive Hilbert 90 for the absolute Galois group: H¹(G_K, Kˢ) = 0.

theorem TauCeti.additiveHilbert90 (K : Type u_1) [Field K] : CategoryTheory.Limits.IsZero (continuousCohomology 1 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (ForcedDiscrete (SeparableClosure K))))

The additive Hilbert 90 for the absolute Galois group, stated for Mathlib's canonical continuous cohomology: H¹(G_K, Kˢ) = 0.