The cup product with trivial 𝔽_p coefficients on the explicit models

The cup square cupFp p G : H¹(G, 𝔽_p) × H¹(G, 𝔽_p) → H²(G, 𝔽_p) is the canonical cup product of Mathlib's continuous cohomology at the multiplication pairing of the trivial coefficient object trivialFp p G, and the Demushkin condition on a pro-p group is stated against it. The explicit models H1 G (ZMod p) and H2 G (ZMod p) of the same groups, identified with cohomFp p G 1 and cohomFp p G 2 by TauCeti.cohomFpAddEquivH1 and TauCeti.cohomFpAddEquivH2, carry the explicit (1,1) cup product TauCeti.ContCohomology.explicitCup11 of multiplication, (a ⌣ b) (g, h) = a g * b h on continuous characters a, b : G → 𝔽_p. This file proves that the two agree: the cup square of two classes of H¹(G, 𝔽_p) is the class of the product cocycle of the corresponding characters.

This is what lets the cup product on cohomFp be computed on characters, for instance through a Heisenberg cochain and the transgression of a minimal presentation, which is how the cup matrix of a one-relator pro-p group is read off its relator.

Main results

• TauCeti.cohomFpAddEquivH2_cupFp: under the identifications of H¹(G, 𝔽_p) and H²(G, 𝔽_p) with their explicit models, cupFp p G is the explicit (1,1) cup product of multiplication.
• TauCeti.cupFp_cohomFpAddEquivH1_symm: the same identity read from the explicit side.
• TauCeti.cupFp_eq_zero_iff: the cup square of two classes vanishes exactly when the explicit cup product of the corresponding explicit classes does.
• TauCeti.explicitCup11_mul_bijective_iff: the explicit cup square is a perfect pairing exactly when cupFp p G is.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Chapter I, §4, for the inhomogeneous cup product formula.
• J.-P. Serre, Galois Cohomology, Springer (1997), Chapter I, §4.5.

theorem TauCeti.cohomFpAddEquivH2_cupFp (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (a b : ↑(cohomFp p G 1).toModuleCat) : (cohomFpAddEquivH2 p G htriv) (((cupFp p G) a) b) = ((ContCohomology.explicitCup11 G (ZMod p) (ZMod p) (ZMod p) AddMonoidHom.mul ⋯ ⋯) ((cohomFpAddEquivH1 p G htriv) a)) ((cohomFpAddEquivH1 p G htriv) b)

The cup square on the explicit models. Under the identifications TauCeti.cohomFpAddEquivH1 and TauCeti.cohomFpAddEquivH2 of H¹(G, 𝔽_p) and H²(G, 𝔽_p) with H1 G (ZMod p) and H2 G (ZMod p), for any trivial action of G on ZMod p, the cup square cupFp p G is the explicit (1,1) cup product of multiplication in ZMod p: the cup square of two classes is the class of the cocycle (g, h) ↦ a g * b h, for the corresponding characters a and b.

theorem TauCeti.cupFp_cohomFpAddEquivH1_symm (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (x y : ContCohomology.H1 G (ZMod p)) : ((cupFp p G) ((cohomFpAddEquivH1 p G htriv).symm x)) ((cohomFpAddEquivH1 p G htriv).symm y) = (cohomFpAddEquivH2 p G htriv).symm (((ContCohomology.explicitCup11 G (ZMod p) (ZMod p) (ZMod p) AddMonoidHom.mul ⋯ ⋯) x) y)

The cup square on the explicit models, read from the explicit side: the cup square of the classes corresponding to two explicit classes x, y corresponds to their explicit (1,1) cup product of multiplication.

theorem TauCeti.cupFp_eq_zero_iff (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (a b : ↑(cohomFp p G 1).toModuleCat) : ((cupFp p G) a) b = 0 ↔ ((ContCohomology.explicitCup11 G (ZMod p) (ZMod p) (ZMod p) AddMonoidHom.mul ⋯ ⋯) ((cohomFpAddEquivH1 p G htriv) a)) ((cohomFpAddEquivH1 p G htriv) b) = 0

The cup square of two classes of H¹(G, 𝔽_p) vanishes exactly when the explicit (1,1) cup product of the corresponding explicit classes vanishes.

theorem TauCeti.explicitCup11_mul_bijective_iff (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : Function.Bijective ⇑(ContCohomology.explicitCup11 G (ZMod p) (ZMod p) (ZMod p) AddMonoidHom.mul ⋯ ⋯) ↔ Function.Bijective ⇑(cupFp p G)

The explicit cup square is a perfect pairing exactly when the cup square is: under the identifications TauCeti.cohomFpAddEquivH1 and TauCeti.cohomFpAddEquivH2, the explicit (1,1) cup product of multiplication, x ↦ (y ↦ x ⌣ y), is a bijection from H1 G (ZMod p) onto the additive homomorphisms H1 G (ZMod p) →+ H2 G (ZMod p) exactly when cupFp p G is a bijection from H¹(G, 𝔽_p) onto the linear maps H¹(G, 𝔽_p) →ₗ H²(G, 𝔽_p).