The class of the extension ℤ/4 in H²(ℤ/2, 𝔽₂)

The extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1 of TauCeti/GroupTheory/GroupExtension/ZModFour.lean is an extension of finite discrete groups, hence a profinite extension of ℤ/2 by ℤ/2 inducing the trivial action (TauCeti.ProfiniteGroupExtension.zmodFour). Its class in H²(ℤ/2, 𝔽₂), read in Mathlib's continuous cohomology of the trivial 𝔽₂-representation through TauCeti.ProfiniteGroupExtension.cohomFpClass, is TauCeti.zmodFourExtensionClass. It is nonzero, because the extension has no homomorphic section at all, let alone a continuous one (TauCeti.isEmpty_splitting_zmodFourExtension).

The group H²(ℤ/2, 𝔽₂) is a line, so this nonzero class is the cup square of the generator of H¹(ℤ/2, 𝔽₂); that identification is TauCeti.cupFp_cyclicTwoClass_self_eq_zmodFourExtensionClass in TauCeti/Topology/Algebra/Group/Profinite/Demushkin/CyclicTwo.lean.

Main declarations

• TauCeti.ProfiniteGroupExtension.zmodFour: the profinite extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1 of ℤ/2 by ℤ/2 with the trivial action; its underlying extension is TauCeti.zmodFourExtension (TauCeti.ProfiniteGroupExtension.zmodFour_toGroupExtension).
• TauCeti.zmodFourExtensionClass: the class of the extension ℤ/4 in H²(ℤ/2, 𝔽₂), and TauCeti.zmodFourExtensionClass_ne_zero: it is nonzero.

References

• J.-P. Serre, Galois Cohomology, Springer (1997), Chapter I, §4.5.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), (3.9.10).

@[reducible, inline]

abbrev TauCeti.ProfiniteGroupExtension.zmodFour : ProfiniteGroupExtension (Multiplicative (ZMod 2)) (Multiplicative (ZMod 2))

The extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1 as a profinite extension of ℤ/2 by ℤ/2 inducing the trivial action: its total group ℤ/4 is finite and discrete, and abelian, so conjugation on the kernel is trivial. It is an abbreviation so that its total group and group structure remain definitionally those of Multiplicative (ZMod 4), as for TauCeti.ProfiniteGroupExtension.ofFactorSet.

@[simp]

theorem TauCeti.ProfiniteGroupExtension.zmodFour_toGroupExtension : zmodFour.toGroupExtension = zmodFourExtension

The underlying extension of the profinite extension ℤ/4 is TauCeti.zmodFourExtension.

noncomputable def TauCeti.zmodFourExtensionClass : ↑(cohomFp 2 (Multiplicative (ZMod 2)) 2).toModuleCat

The class of the extension ℤ/4 in H²(ℤ/2, 𝔽₂): the class of the profinite extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1 in Mathlib's continuous cohomology of the trivial 𝔽₂-representation of ℤ/2.

theorem TauCeti.zmodFourExtensionClass_def : zmodFourExtensionClass = ProfiniteGroupExtension.cohomFpClass ⋯ ProfiniteGroupExtension.zmodFour

theorem TauCeti.zmodFourExtensionClass_ne_zero : zmodFourExtensionClass ≠ 0

The class of the extension ℤ/4 in H²(ℤ/2, 𝔽₂) is nonzero: the extension has no homomorphic section.