Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.CyclicTwo

The cyclic group of order two is a Demushkin group #

The cyclic group ℤ/p has H¹(ℤ/p, 𝔽_p) and H²(ℤ/p, 𝔽_p) both one-dimensional, the case d = 1 of the dimension counts for a finite elementary abelian p-group (TauCeti.finrank_cohomFp_one_multiplicative_zmod and TauCeti.finrank_cohomFp_two_multiplicative_zmod in TauCeti.Topology.Algebra.Group.Profinite.ProP.ElementaryAbelian). Whether it is a Demushkin group is therefore decided by the cup square of the nonzero class of H¹(ℤ/p, 𝔽_p). At an odd prime the cup square vanishes, because the cup pairing is alternating, so ℤ/p is not Demushkin; this is the rank-one case of TauCeti.IsDemushkin.demushkinRank_ne_one_of_ne_two. At p = 2 the cup square is nonzero, and ℤ/2 is a Demushkin group of rank one, the first example of the theory (Labute, p. 106).

The cup square is computed on Mathlib's homogeneous cochains. The nonzero class of H¹(ℤ/2, 𝔽₂) (TauCeti.cyclicTwoClass) is the class of the identity character ℤ/2 → 𝔽₂ under the identification TauCeti.cohomFpLinearEquivContinuousZModDual of H¹(ℤ/2, 𝔽₂) with the continuous 𝔽₂-dual of ℤ/2, represented by the homogeneous cocycle (g₀, g₁) ↦ g₀⁻¹ g₁ of that character (TauCeti.characterCocycle); the cup square of that cocycle is the homogeneous two-cochain (g₀, g₁, g₂) ↦ (g₀⁻¹ g₁) (g₁⁻¹ g₂), which takes the value 1 at (1, s, 1) and 0 at (1, 1, 1), where s is the generator. A homogeneous one-cochain b is invariant, so b s 1 = b 1 s, and its coboundary takes the value b 1 1 at both (1, s, 1) and (1, 1, 1); hence the cup square is not a coboundary.

Since H²(ℤ/2, 𝔽₂) is a line, the cup square is the unique nonzero class, and so it is the class of the extension 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1 (TauCeti.zmodFourExtensionClass), which is nonzero because that extension does not split. This is the classical description of the cup square on H¹(ℤ/2, 𝔽₂) as the Bockstein of the generator, the class of the extension ℤ/4.

Main results #

References #

ℤ/p at an odd prime #

source
theorem TauCeti.not_isDemushkin_multiplicative_zmod_of_ne_two (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) :
¬IsDemushkin p (Multiplicative (ZMod p))

At an odd prime, ℤ/p is not a Demushkin group: it has rank one, and the rank of a Demushkin group at an odd prime is even.

The cup square of the generator of H¹(ℤ/2, 𝔽₂) #

source
noncomputable def TauCeti.cyclicTwoClass :
↑(cohomFp 2 (Multiplicative (ZMod 2)) 1).toModuleCat

The generator of H¹(ℤ/2, 𝔽₂): the class of the identity character ℤ/2 → 𝔽₂, represented by the homogeneous cocycle (g₀, g₁) ↦ g₀⁻¹ g₁ (TauCeti.characterCocycle).

Instances For
    source
    @[simp]
    theorem TauCeti.cupFp_cyclicTwoClass_self_ne_zero :
    ((cupFp 2 (Multiplicative (ZMod 2))) cyclicTwoClass) cyclicTwoClass ≠ 0

    The cup square of the generator of H¹(ℤ/2, 𝔽₂) is nonzero. The cup square of the homogeneous cocycle (g₀, g₁) ↦ g₀⁻¹ g₁ is the two-cochain (g₀, g₁, g₂) ↦ (g₀⁻¹ g₁) (g₁⁻¹ g₂), which is not the coboundary of any invariant one-cochain.

    source
    @[simp]
    theorem TauCeti.cyclicTwoClass_ne_zero :
    cyclicTwoClass ≠ 0

    The generator of H¹(ℤ/2, 𝔽₂) is nonzero: its cup square is.

    source
    theorem TauCeti.cupFp_cyclicTwoClass_self_eq_zmodFourExtensionClass :
    ((cupFp 2 (Multiplicative (ZMod 2))) cyclicTwoClass) cyclicTwoClass = zmodFourExtensionClass

    The cup square of the generator of H¹(ℤ/2, 𝔽₂) is the class of the extension ℤ/4: both are nonzero, and H²(ℤ/2, 𝔽₂) is a line over 𝔽₂, whose only nonzero scalar is 1.

    ℤ/2 is Demushkin #

    source
    theorem TauCeti.isDemushkin_multiplicative_zmod_two :
    IsDemushkin 2 (Multiplicative (ZMod 2))

    The cyclic group ℤ/2 is a Demushkin group at p = 2: H¹(ℤ/2, 𝔽₂) and H²(ℤ/2, 𝔽₂) are one-dimensional, and the cup square of the generator of H¹(ℤ/2, 𝔽₂) is nonzero.

    source
    @[simp]
    theorem TauCeti.demushkinRank_multiplicative_zmod_two :
    demushkinRank isDemushkin_multiplicative_zmod_two = 1

    ℤ/2 is a Demushkin group of rank one.