Parity of the rank of a Demushkin group

When every cup square on H¹(G, 𝔽_p) vanishes, the cup form of a Demushkin group (LinearMap.cupForm) is a nondegenerate alternating form, so the Demushkin rank is even. At an odd prime this is automatic by graded commutativity (LinearMap.isAlt_cupForm_of_ne_two); in particular the rank cannot be one there. This is the parity constraint on the odd-prime normal forms. At p = 2 the vanishing of the cup squares is decided by Labute's invariant q, in TauCeti.Topology.Algebra.Group.Profinite.Demushkin.CupSquare.

Main results

• TauCeti.IsDemushkin.even_demushkinRank_of_forall_cupFp_self_eq_zero: the rank is even when every cup square vanishes.
• TauCeti.IsDemushkin.even_demushkinRank_of_ne_two: the rank is even at an odd prime.
• TauCeti.IsDemushkin.demushkinRank_ne_one_of_ne_two: rank one occurs only at p = 2.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132.

theorem TauCeti.IsDemushkin.even_demushkinRank_of_forall_cupFp_self_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (h : ∀ (a : ↑(cohomFp p G 1).toModuleCat), ((cupFp p G) a) a = 0) : Even (demushkinRank hG)

A Demushkin group on which every cup square vanishes has even rank: the cup form is then a nondegenerate alternating form on H¹(G, 𝔽_p), whose dimension is the rank.

theorem TauCeti.IsDemushkin.even_demushkinRank_of_ne_two {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (hp : p ≠ 2) : Even (demushkinRank hG)

At an odd prime, the rank of a Demushkin group is even: every cup square vanishes, because the cup product is graded-commutative and 2 is invertible.

theorem TauCeti.IsDemushkin.demushkinRank_ne_one_of_ne_two {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (hp : p ≠ 2) : demushkinRank hG ≠ 1

A Demushkin group at an odd prime cannot have rank one.