The extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1

The cyclic group of order four is a non-split extension of ℤ/2 by ℤ/2: the kernel is the subgroup 2ℤ/4ℤ, included by the doubling map ZMod.mulCastHom 2, and the projection is reduction modulo two. Written multiplicatively, as the extension dictionary of TauCeti/GroupTheory/GroupExtension requires, this is TauCeti.zmodFourExtension. It has no homomorphic section (TauCeti.isEmpty_splitting_zmodFourExtension): a section would send the generator of ℤ/2 to an element of order dividing two with odd residue, and the elements of order dividing two in ℤ/4 are 0 and 2.

This is the extension whose class in H²(ℤ/2, 𝔽₂) is the cup square of the generator of H¹(ℤ/2, 𝔽₂), the first nonzero cup square of the theory of Demushkin groups; the profinite extension it defines and its class are the subject of TauCeti/Topology/Algebra/GroupExtension/ZModFour.lean.

Main declarations

• TauCeti.zmodFourExtension: the extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1, with its inclusion and projection TauCeti.zmodFourExtension_inl and TauCeti.zmodFourExtension_rightHom.
• TauCeti.isEmpty_splitting_zmodFourExtension: it has no homomorphic section.

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).

def TauCeti.zmodFourExtension : GroupExtension (Multiplicative (ZMod 2)) (Multiplicative (ZMod 4)) (Multiplicative (ZMod 2))

The extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1, written multiplicatively: the kernel ℤ/2 is included as 2ℤ/4ℤ by the doubling map, and the projection is reduction modulo two.

@[simp]

theorem TauCeti.zmodFourExtension_inl : zmodFourExtension.inl = AddMonoidHom.toMultiplicative (ZMod.mulCastHom 2 ⋯)

The kernel of 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1 is included by the doubling map.

@[simp]

theorem TauCeti.zmodFourExtension_rightHom : zmodFourExtension.rightHom = AddMonoidHom.toMultiplicative (ZMod.castHom zmodFourExtension_rightHom._proof_1 (ZMod 2)).toAddMonoidHom

The projection of 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1 is reduction modulo two.

theorem TauCeti.isEmpty_splitting_zmodFourExtension : IsEmpty zmodFourExtension.Splitting

The extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1 has no homomorphic section: a section would send the generator of ℤ/2 to an element of ℤ/4 of order dividing two with odd residue, and the only elements of ℤ/4 of order dividing two are 0 and 2.