The cup form of a Demushkin group and its normal forms

For a Demushkin group G, H²(G, 𝔽_p) is one-dimensional, so a nonzero linear functional φ : H²(G, 𝔽_p) →ₗ 𝔽_p is an isomorphism, and the cup form φ.cupForm, the bilinear form (a, b) ↦ φ (a ⌣ b) on H¹(G, 𝔽_p), is nondegenerate: this is Labute's definition of a Demushkin group, and the predicate IsDemushkin is characterized here by it. The choice of φ is unique up to a nonzero scalar, and the statements below do not depend on it.

The normal forms of nondegenerate bilinear forms then describe the cup product of a Demushkin group completely. At an odd prime the cup form is alternating, so H¹(G, 𝔽_p) has a symplectic basis, in which the matrix of the form is the standard block matrix J, and the rank of G is even. At p = 2 the form is symmetric, and there are two cases: if it is alternating there is again a symplectic basis and the rank is even; if it is not, H¹(G, 𝔽₂) has an orthonormal basis, in which the matrix of the form is the identity, and the rank may be odd. Transporting such a basis to a change of generators of the free pro-p group, which produces the normal forms of the Demushkin relator, is not treated in this file.

Main results

• TauCeti.IsDemushkin.nondegenerate_cupForm, TauCeti.IsDemushkin.nondegenerate_cupForm_of_ne_zero: the cup form of a Demushkin group is nondegenerate, for every injective, equivalently nonzero, functional on H²(G, 𝔽_p).
• TauCeti.IsDemushkin.cupFp_bijective: the cup square is a perfect pairing, a ↦ (a ⌣ ·) being a bijection from H¹(G, 𝔽_p) onto the linear maps H¹(G, 𝔽_p) →ₗ H²(G, 𝔽_p).
• TauCeti.IsDemushkin.of_nondegenerate_cupForm, TauCeti.isDemushkin_iff_nondegenerate_cupForm: Labute's definition: a pro-p group with finite-dimensional H¹(G, 𝔽_p) is Demushkin exactly when its cup form is nondegenerate for an isomorphism H²(G, 𝔽_p) ≅ 𝔽_p.
• TauCeti.IsDemushkin.of_cupFp_injective: a pro-p group with finite-dimensional H¹(G, 𝔽_p), one-dimensional H²(G, 𝔽_p) and injective a ↦ (a ⌣ ·) is Demushkin.
• TauCeti.IsDemushkin.exists_basis_toMatrix_cupForm_eq_J_of_isAlt, TauCeti.IsDemushkin.exists_basis_toMatrix_cupForm_eq_J_of_ne_two: when the cup form is alternating, in particular at an odd prime, H¹(G, 𝔽_p) has a basis in which its matrix is J.
• TauCeti.IsDemushkin.even_demushkinRank_of_isAlt: an alternating cup form forces even rank.
• TauCeti.IsDemushkin.exists_basis_toMatrix_cupForm_eq_one_of_not_isAlt, TauCeti.IsDemushkin.exists_basis_toMatrix_cupForm_eq_J_or_eq_one: at p = 2, a non-alternating cup form has an orthonormal basis, and every Demushkin group at p = 2 falls into exactly one of the two cases.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, p. 106 and Proposition 3.
• J.-P. Serre, Galois Cohomology, Chapter I, §4.5.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.9.9).

theorem TauCeti.IsDemushkin.nonempty_linearEquiv_cohomFp_two {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) : Nonempty (↑(cohomFp p G 2).toModuleCat ≃ₗ[ZMod p] ZMod p)

H²(G, 𝔽_p) of a Demushkin group is isomorphic to 𝔽_p.

theorem TauCeti.IsDemushkin.injective_of_ne_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) {φ : ↑(cohomFp p G 2).toModuleCat →ₗ[ZMod p] ZMod p} (hφ : φ ≠ 0) : Function.Injective ⇑φ

A nonzero linear functional on the one-dimensional H²(G, 𝔽_p) of a Demushkin group is injective.

theorem TauCeti.IsDemushkin.nondegenerate_cupForm {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) {φ : ↑(cohomFp p G 2).toModuleCat →ₗ[ZMod p] ZMod p} (hφ : Function.Injective ⇑φ) : φ.cupForm.Nondegenerate

The cup form of a Demushkin group is nondegenerate, for every injective functional φ : H²(G, 𝔽_p) →ₗ 𝔽_p.

theorem TauCeti.IsDemushkin.nondegenerate_cupForm_of_ne_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) {φ : ↑(cohomFp p G 2).toModuleCat →ₗ[ZMod p] ZMod p} (hφ : φ ≠ 0) : φ.cupForm.Nondegenerate

The cup form of a Demushkin group is nondegenerate for every nonzero functional on H²(G, 𝔽_p).

theorem TauCeti.IsDemushkin.cupFp_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) : Function.Bijective ⇑(cupFp p G)

The cup square of a Demushkin group is a perfect pairing: a ↦ (a ⌣ ·) is a bijection from H¹(G, 𝔽_p) onto the linear maps H¹(G, 𝔽_p) →ₗ H²(G, 𝔽_p). Injectivity is the left-separating clause of the definition; surjectivity is nondegeneracy of the cup form for an isomorphism H²(G, 𝔽_p) ≅ 𝔽_p, through the duality LinearMap.BilinForm.toDual.

theorem TauCeti.IsDemushkin.exists_basis_toMatrix_cupForm_eq_J_of_isAlt {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) {φ : ↑(cohomFp p G 2).toModuleCat →ₗ[ZMod p] ZMod p} (hφ : φ ≠ 0) (halt : φ.cupForm.IsAlt) : ∃ (m : ℕ) (b : Module.Basis (Fin m ⊕ Fin m) (ZMod p) ↑(cohomFp p G 1).toModuleCat), (LinearMap.BilinForm.toMatrix b) φ.cupForm = Matrix.J (Fin m) (ZMod p)

An alternating cup form has a symplectic basis: when the cup form of a Demushkin group is alternating, H¹(G, 𝔽_p) has a basis indexed by Fin m ⊕ Fin m in which its matrix is the standard block matrix J.

theorem TauCeti.IsDemushkin.exists_basis_toMatrix_cupForm_eq_J_of_ne_two {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) (hp : p ≠ 2) {φ : ↑(cohomFp p G 2).toModuleCat →ₗ[ZMod p] ZMod p} (hφ : φ ≠ 0) : ∃ (m : ℕ) (b : Module.Basis (Fin m ⊕ Fin m) (ZMod p) ↑(cohomFp p G 1).toModuleCat), (LinearMap.BilinForm.toMatrix b) φ.cupForm = Matrix.J (Fin m) (ZMod p)

At an odd prime the cup form has a symplectic basis: H¹(G, 𝔽_p) has a basis indexed by Fin m ⊕ Fin m in which the matrix of the cup form is J.

theorem TauCeti.IsDemushkin.even_demushkinRank_of_isAlt {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) [CompactSpace G] [TotallyDisconnectedSpace G] {φ : ↑(cohomFp p G 2).toModuleCat →ₗ[ZMod p] ZMod p} (hφ : φ ≠ 0) (halt : φ.cupForm.IsAlt) : Even (demushkinRank hG)

An alternating cup form forces even rank.

theorem TauCeti.IsDemushkin.of_nondegenerate_cupForm {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hP : IsProP p G) (hfin : Module.Finite (ZMod p) ↑(cohomFp p G 1).toModuleCat) (e : ↑(cohomFp p G 2).toModuleCat ≃ₗ[ZMod p] ZMod p) (hnd : (↑e).cupForm.Nondegenerate) : IsDemushkin p G

Labute's definition of a Demushkin group: a pro-p group G with finite-dimensional H¹(G, 𝔽_p), an isomorphism e : H²(G, 𝔽_p) ≅ 𝔽_p and nondegenerate cup form (a, b) ↦ e (a ⌣ b) is Demushkin. The right-separating clause of IsDemushkin follows from the left one by graded commutativity.

theorem TauCeti.IsDemushkin.of_cupFp_injective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hP : IsProP p G) (hfin : Module.Finite (ZMod p) ↑(cohomFp p G 1).toModuleCat) (h2 : Module.finrank (ZMod p) ↑(cohomFp p G 2).toModuleCat = 1) (hcup : Function.Injective ⇑(cupFp p G)) : IsDemushkin p G

A perfect cup-product pairing makes a Demushkin group: a pro-p group G with finite-dimensional H¹(G, 𝔽_p) and one-dimensional H²(G, 𝔽_p) on which a ↦ (a ⌣ ·) is injective is Demushkin. Injectivity is the left-separating clause, and the right-separating clause follows by graded commutativity. With IsDemushkin.cupFp_bijective, this characterizes Demushkin groups among the pro-p groups with finite H¹(G, 𝔽_p) and one-dimensional H²(G, 𝔽_p).

theorem TauCeti.isDemushkin_iff_nondegenerate_cupForm {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsDemushkin p G ↔ IsProP p G ∧ Module.Finite (ZMod p) ↑(cohomFp p G 1).toModuleCat ∧ ∃ (e : ↑(cohomFp p G 2).toModuleCat ≃ₗ[ZMod p] ZMod p), (↑e).cupForm.Nondegenerate

The Demushkin predicate is Labute's definition: G is Demushkin exactly when it is pro-p with finite-dimensional H¹(G, 𝔽_p) and its cup form is nondegenerate for some isomorphism H²(G, 𝔽_p) ≅ 𝔽_p; the choice of isomorphism is immaterial by LinearMap.nondegenerate_cupForm_iff_of_injective.

The dyadic case

At p = 2 the cup form is symmetric, and a symmetric nondegenerate form over 𝔽₂ is either alternating, with a symplectic basis, or has an orthonormal basis.

theorem TauCeti.IsDemushkin.exists_basis_toMatrix_cupForm_eq_one_of_not_isAlt {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin 2 G) {φ : ↑(cohomFp 2 G 2).toModuleCat →ₗ[ZMod 2] ZMod 2} (hφ : φ ≠ 0) (h : ¬φ.cupForm.IsAlt) : ∃ (b : Module.Basis (Fin (Module.finrank (ZMod 2) ↑(cohomFp 2 G 1).toModuleCat)) (ZMod 2) ↑(cohomFp 2 G 1).toModuleCat), (LinearMap.BilinForm.toMatrix b) φ.cupForm = 1

A non-alternating cup form at p = 2 has an orthonormal basis: H¹(G, 𝔽₂) has a basis in which the matrix of the cup form is the identity.

theorem TauCeti.IsDemushkin.exists_basis_toMatrix_cupForm_eq_J_or_eq_one {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin 2 G) {φ : ↑(cohomFp 2 G 2).toModuleCat →ₗ[ZMod 2] ZMod 2} (hφ : φ ≠ 0) : (φ.cupForm.IsAlt ∧ ∃ (m : ℕ) (b : Module.Basis (Fin m ⊕ Fin m) (ZMod 2) ↑(cohomFp 2 G 1).toModuleCat), (LinearMap.BilinForm.toMatrix b) φ.cupForm = Matrix.J (Fin m) (ZMod 2)) ∨ ¬φ.cupForm.IsAlt ∧ ∃ (b : Module.Basis (Fin (Module.finrank (ZMod 2) ↑(cohomFp 2 G 1).toModuleCat)) (ZMod 2) ↑(cohomFp 2 G 1).toModuleCat), (LinearMap.BilinForm.toMatrix b) φ.cupForm = 1

The two shapes of the cup form at p = 2: the cup form of a Demushkin group at p = 2 is either alternating, with a symplectic basis in which its matrix is J, or not alternating, with an orthonormal basis in which its matrix is the identity.