The third cohomology of a class formation vanishes

For a class formation with module A on a profinite group G, Tate's theorem TauCeti.ClassFieldTheory.ClassFormation.tateIso at degree 1 identifies the third cohomology of every finite normal layer V ◁ U with the first cohomology of its Galois group in trivial integral coefficients,

H³(U ⧸ V, A^V) ≅ H-hat^3(U ⧸ V, A^V) ≅ H-hat^1(U ⧸ V, ℤ) = Hom(U ⧸ V, ℤ) = 0,

which vanishes because the Galois group is finite (ClassFormation.subsingleton_H3). Continuous cohomology being the colimit of the cohomology of the finite quotients G ⧸ V, each of which is the cohomology of the layer V ◁ G, the continuous third cohomology H³(G, A) vanishes as well (ClassFormation.subsingleton_continuousCohomology_three). For the local class formation this is the vanishing of H³(G_K, (Kˢ)ˣ), the input to the cohomological dimension of the absolute Galois group of a local field.

Main results

• TauCeti.ClassFieldTheory.ClassFormation.subsingleton_H3: H³ of every layer of a class formation vanishes.
• TauCeti.ClassFieldTheory.ClassFormation.subsingleton_continuousCohomology_three: the continuous H³(G, A) of the module of a class formation vanishes.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.
• J.-P. Serre, Local Fields, Chapter XI, §3, and Galois Cohomology, Ch. II, §5.3.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (7.1.8).

The layer of an open normal subgroup as a finite level

theorem TauCeti.ClassFieldTheory.ClassFormation.subsingleton_H3 {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : Subsingleton ↑(L.H F 3)

The third cohomology of every layer of a class formation vanishes. Tate's isomorphism at degree 1 identifies H-hat^3(U ⧸ V, A^V), which is H³(U ⧸ V, A^V), with H-hat^1(U ⧸ V, ℤ) = Hom(U ⧸ V, ℤ), which is zero because U ⧸ V is finite.

theorem TauCeti.ClassFieldTheory.ClassFormation.subsingleton_continuousCohomology_three {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) : Subsingleton ↑(continuousCohomology 3 F.module).toModuleCat

The continuous third cohomology of a class formation vanishes: H³(G, A) = 0 for the module A of a class formation on G. Every class is inflated from a finite quotient G ⧸ V, whose third cohomology is that of the layer V ◁ G, zero by subsingleton_H3.