Hilbert 90 for infinite Galois extensions

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

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

Specialised to a separable closure this is Hilbert 90 for the absolute Galois group, H¹(G_K, (Kˢ)ˣ) = 0, which is what makes the Kummer map Kˣ → H¹(G_K, μₙ) surjective for n positive and invertible in K.

The proof passes to finite layers. An open normal subgroup U of Gal(L/K) has a fixed field F that is finite Galois over K; the infinite Galois correspondence identifies Gal(L/K) ⧸ U with Gal(F/K) (InfiniteGalois.normalAutEquivQuotient), and the units of L fixed by U are the units of F. Through these two identifications a 1-cocycle of the finite layer becomes a multiplicative 1-cocycle Gal(F/K) → Fˣ, which is a coboundary by Noether's form of Hilbert 90, groupCohomology.isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units. The vanishing then passes to Gal(L/K) because every continuous class is inflated from a finite layer, TauCeti.ContCohomology.subsingleton_H1_of_forall_openNormalSubgroup.

For a finite group H of automorphisms of L, embedded in Gal(L/K) by f, Artin's theorem identifies H with the Galois group of L over the fixed field of the image of f, so Noether's Hilbert 90 gives H¹(H, Lˣ) = 0 without any finiteness assumption on L/K.

Main results

• TauCeti.galEquivOfInjective: a finite group H embedded in Gal(L/K) is the Galois group of L over the fixed field of its image.
• TauCeti.groupCohomologyResUnitsIso: the induced isomorphism of the cohomology of Lˣ.
• TauCeti.isZero_groupCohomology_one_res_units: H¹(H, Lˣ) = 0 for such H.
• TauCeti.isCoboundary₁_of_isCocycle₁_of_quotient_to_fixedPoints: Hilbert 90 at a finite layer Gal(L/K) ⧸ U with coefficients (Lˣ)^U.
• TauCeti.subsingleton_H1_additive_units: H¹(Gal(L/K), Lˣ) = 0 for any Galois L/K.
• TauCeti.subsingleton_H1_unitsCoeff: H¹(G_K, (Kˢ)ˣ) = 0.
• TauCeti.subsingleton_H1_unitsCoeff_fixingSubgroup, TauCeti.subsingleton_H1_unitsCoeff_of_isClosed: H¹(N, (Kˢ)ˣ) = 0 for the subgroup N fixing a subextension, equivalently for every closed subgroup N of G_K.
• TauCeti.explicitInfl2_unitsCoeff_injective: consequently inflation from G_K ⧸ N into H²(G_K, (Kˢ)ˣ) is injective for every closed normal subgroup N.
• TauCeti.hilbert90: the preceding vanishing for Mathlib's canonical continuous cohomology.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.2.1).

theorem TauCeti.isCoboundary₁_of_isCocycle₁_of_quotient_to_fixedPoints {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) (Additive Lˣ))} (hf : groupCohomology.IsCocycle₁ f) : groupCohomology.IsCoboundary₁ f

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 invariant units (Lˣ)^U, written additively, 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).

noncomputable def TauCeti.galEquivOfInjective {K L : Type} [Field K] [Field L] [Algebra K L] {H : Type} [Group H] [Finite H] {f : H →* Gal(L/K)} (hf : Function.Injective ⇑f) : H ≃* Gal(L/↥(IntermediateField.fixedField f.range))

Artin's theorem for a finite group of automorphisms. An injective homomorphism f : H →* Gal(L/K) from a finite group identifies H with the Galois group of L over the fixed field of the image of f (FixedPoints.toAlgAutMulEquiv). No finiteness of L/K is needed.

Equations

• TauCeti.galEquivOfInjective hf = (MonoidHom.ofInjective hf).trans (FixedPoints.toAlgAutMulEquiv (↥f.range) L)

@[simp]

theorem TauCeti.galEquivOfInjective_apply {K L : Type} [Field K] [Field L] [Algebra K L] {H : Type} [Group H] [Finite H] {f : H →* Gal(L/K)} (hf : Function.Injective ⇑f) (h : H) (x : L) : ((galEquivOfInjective hf) h) x = (f h) x

noncomputable def TauCeti.groupCohomologyResUnitsIso {K L : Type} [Field K] [Field L] [Algebra K L] {H : Type} [Group H] [Finite H] {f : H →* Gal(L/K)} (hf : Function.Injective ⇑f) (n : ℕ) : groupCohomology (Rep.res f (Rep.ofMulDistribMulAction Gal(L/K) Lˣ)) n ≅ groupCohomology (Rep.ofMulDistribMulAction Gal(L/↥(IntermediateField.fixedField f.range)) Lˣ) n

The cohomology of a finite group H acting on Lˣ through an injective f : H →* Gal(L/K) is the cohomology of Gal(L/E) acting on Lˣ, for E the fixed field of the image of f.

Equations

• TauCeti.groupCohomologyResUnitsIso hf n = groupCohomology.mapIso (TauCeti.galEquivOfInjective hf) (LinearEquiv.refl ℤ ↑(Rep.res f (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) ⋯ n

theorem TauCeti.isZero_groupCohomology_one_res_units {K L : Type} [Field K] [Field L] [Algebra K L] {H : Type} [Group H] [Finite H] {f : H →* Gal(L/K)} (hf : Function.Injective ⇑f) : CategoryTheory.Limits.IsZero (groupCohomology (Rep.res f (Rep.ofMulDistribMulAction Gal(L/K) Lˣ)) 1)

Hilbert 90 for a finite group of automorphisms. If H is finite and f : H →* Gal(L/K) is injective, then H¹(H, Lˣ) = 0 for the action of H on Lˣ through f: the group H is the Galois group of L over the fixed field of its image, and Noether's Hilbert 90 applies to that finite extension.

theorem TauCeti.subsingleton_H1_additive_units {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] [TopologicalSpace (Additive Lˣ)] [DiscreteTopology (Additive Lˣ)] [ContinuousSMul Gal(L/K) (Additive Lˣ)] : Subsingleton (ContCohomology.H1 Gal(L/K) (Additive Lˣ))

Hilbert 90 for a Galois extension L/K, finite or not: the continuous H¹(Gal(L/K), Lˣ) vanishes, the units of L being written additively and carrying the discrete topology (NSW (6.2.1)). Every class is inflated from a finite layer, where it vanishes by TauCeti.isCoboundary₁_of_isCocycle₁_of_quotient_to_fixedPoints.

The continuity of the action is automatic for the discrete topology (TauCeti.stabilizer_isOpen_units) and is an instance argument only because H¹ is formed under it.

instance TauCeti.subsingleton_H1_unitsCoeff (K : Type u_1) [Field K] : Subsingleton (ContCohomology.H1 (AbsoluteGaloisGroup K) (UnitsCoeff K))

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

theorem TauCeti.subsingleton_H1_unitsCoeff_fixingSubgroup (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : Subsingleton (ContCohomology.H1 (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K))

Hilbert 90 for the subgroup of G_K fixing a subextension: for a K-embedding σ : L →ₐ[K] Kˢ, the continuous H¹(Gal(Kˢ/σ(L)), (Kˢ)ˣ) vanishes. The isomorphism G_L ≃ₜ* Gal(Kˢ/σ(L)) of TauCeti.absoluteGaloisGroupEquivFixingSubgroup, together with the matching identification (Kˢ)ˣ ≃ (Lˢ)ˣ of coefficients, carries it to Hilbert 90 for G_L.

theorem TauCeti.subsingleton_H1_unitsCoeff_of_isClosed (K : Type u_1) [Field K] (N : Subgroup (AbsoluteGaloisGroup K)) (hN : IsClosed ↑N) : Subsingleton (ContCohomology.H1 (↥N) (UnitsCoeff K))

Hilbert 90 for a closed subgroup of G_K: H¹(N, (Kˢ)ˣ) = 0 for every closed subgroup N, which is the subgroup fixing its fixed field (InfiniteGalois.fixingSubgroup_fixedField).

theorem TauCeti.explicitInfl2_unitsCoeff_injective (K : Type u_1) [Field K] (N : Subgroup (AbsoluteGaloisGroup K)) [N.Normal] (hN : IsClosed ↑N) [ContinuousSMul (AbsoluteGaloisGroup K ⧸ N) ↥(FixedPoints.addSubgroup (↥N) (UnitsCoeff K))] : Function.Injective ⇑(ContCohomology.explicitInfl2 (AbsoluteGaloisGroup K) (UnitsCoeff K) N)

Inflation into H²(G_K, (Kˢ)ˣ) is injective: for a closed normal subgroup N of G_K, inflation H²(G_K ⧸ N, ((Kˢ)ˣ)^N) → H²(G_K, (Kˢ)ˣ) is injective, since by Hilbert 90 for N the transgression out of H¹(N, (Kˢ)ˣ) vanishes. For the subgroup fixing a Galois subextension L/K this is the injectivity of H²(Gal(L/K), Lˣ) into the cohomological Brauer group.

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

Hilbert 90 for the absolute Galois group, stated for Mathlib's canonical continuous cohomology: H¹(G_K, (Kˢ)ˣ) = 0 (NSW (6.2.1)). This is the form in which the vanishing feeds the canonical all-degree theory, where it makes the Kummer map Kˣ → H¹(G_K, μₙ) surjective for n positive and invertible in K.