Heisenberg cochains: continuous primitives of a cup product

Let G be a topological group, let M, A and P be topological G-modules with an equivariant pairing μ : M →+ A →+ P, and let a and b be continuous 1-cocycles with values in M and A. A Heisenberg cochain for (a, b) is a continuous h : G → P with

h (g * g') = h g + g • h g' + μ (a g) (g • b g'),

that is, a continuous 1-cochain whose coboundary is -(a ⌣ b), for the explicit (1,1) cup product (a ⌣ b) (g, g') = μ (a g) (g • b g'). For trivial actions and μ the multiplication of 𝔽_p, the triple (a, b, h) is a homomorphism from G to the Heisenberg group of unipotent upper triangular 3 × 3 matrices over 𝔽_p, with a and b on the superdiagonal and h in the corner, which is where the name comes from. Such a cochain exists exactly when the cup product a ⌣ b vanishes in H²(G, P) (TauCeti.ContCohomology.explicitCup11_eq_zero_iff), in particular whenever H²(G, P) = 0, for instance for a free pro-p group and 𝔽_p-coefficients.

The values of h on commutators and on powers are recorded for trivial actions, h ⁅g, g'⁆ = μ (a g) (b g') - μ (a g') (b g) and h (g ^ n) = n • h g + (n.choose 2) • μ (a g) (b g). Together with the transgression formula of TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.Transgression, these are what evaluates the cup product on a relator of a minimal presentation written as a product of p-th powers and commutators of the generators, as in Labute's Proposition 3.

Main definitions

• TauCeti.ContCohomology.IsHeisenbergCochain: h is a Heisenberg cochain for (a, b) and μ.

Main results

• TauCeti.ContCohomology.explicitCup11_eq_zero_iff: the (1,1) cup product of two cocycles vanishes exactly when they admit a Heisenberg cochain (TauCeti.ContCohomology.IsHeisenbergCochain.of_d1_eq and TauCeti.ContCohomology.IsHeisenbergCochain.d1_neg are the two directions on cochains), and TauCeti.ContCohomology.exists_isHeisenbergCochain_of_subsingleton_H2: it exists when H²(G, P) = 0.
• TauCeti.ContCohomology.IsHeisenbergCochain.apply_conj: the conjugation formula g • h (g⁻¹ * n * g) = h n + n • h g - h g for n in a normal subgroup on which a and b vanish.
• TauCeti.ContCohomology.IsHeisenbergCochain.apply_commutatorElement_of_smul_eq_self, TauCeti.ContCohomology.IsHeisenbergCochain.apply_pow_of_smul_eq_self: the values of a Heisenberg cochain on commutators and on powers, for trivial actions.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §1.4 and Proposition 3.
• W. G. Dwyer, Homology, Massey products and maps between groups, J. Pure Appl. Algebra 6 (1975), 177–190, for the lifting of a pair of characters with vanishing cup product to the Heisenberg group.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter III, §9.

structure TauCeti.ContCohomology.IsHeisenbergCochain {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] (μ : M →+ A →+ P) (a : ↥(Z1 G M)) (b : ↥(Z1 G A)) (h : G → P) : Prop

A Heisenberg cochain for the continuous 1-cocycles a : G → M and b : G → A and the pairing μ : M →+ A →+ P: a continuous h : G → P with h (g * g') = h g + g • h g' + μ (a g) (g • b g'). Equivalently, the coboundary of -h is the explicit (1,1) cup product (a ⌣ b) (g, g') = μ (a g) (g • b g') (TauCeti.ContCohomology.IsHeisenbergCochain.d1_neg); for trivial actions, (a, b, h) is a homomorphism to the Heisenberg group with a and b on the superdiagonal and h in the corner.

• continuous : Continuous h

  the cochain h is continuous

• apply_mul (g g' : G) : h (g * g') = h g + g • h g' + (μ (↑a g)) (g • ↑b g')

  the Heisenberg multiplication law h (g * g') = h g + g • h g' + μ (a g) (g • b g')

theorem TauCeti.ContCohomology.IsHeisenbergCochain.of_d1_eq {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} [IsTopologicalAddGroup P] {f : G → P} (hf : Continuous f) (hd : (d1 G P) f = fun (q : G × G) => (μ (↑a q.1)) (q.1 • ↑b q.2)) : IsHeisenbergCochain μ a b fun (g : G) => -f g

A continuous primitive of the cup cochain gives a Heisenberg cochain: if f is continuous with d¹ f = ((g, g') ↦ μ (a g) (g • b g')), then -f is a Heisenberg cochain for (a, b).

theorem TauCeti.ContCohomology.IsHeisenbergCochain.d1_neg {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) : ((d1 G P) fun (g : G) => -h g) = fun (q : G × G) => (μ (↑a q.1)) (q.1 • ↑b q.2)

The coboundary of -h is the (1,1) cup cochain (g, g') ↦ μ (a g) (g • b g').

theorem TauCeti.ContCohomology.IsHeisenbergCochain.apply_one {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) : h 1 = 0

A Heisenberg cochain vanishes at 1.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.apply_conj {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) {N : Subgroup G} [N.Normal] (haN : ∀ (n : ↥N), ↑a ↑n = 0) (hbN : ∀ (n : ↥N), ↑b ↑n = 0) (g : G) (n : ↥N) : g • h (g⁻¹ * ↑n * g) = h ↑n + ↑n • h g - h g

Conjugation formula. If a and b vanish on the normal subgroup N, then for n ∈ N g • h (g⁻¹ * n * g) = h n + n • h g - h g.

theorem TauCeti.ContCohomology.explicitCup11_eq_zero_iff {G : Type uG} [Group G] [TopologicalSpace G] [ContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] {μ : M →+ A →+ P} (hμ : Continuous fun (p : M × A) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (x : A), (μ (g • m)) (g • x) = g • (μ m) x) (a : ↥(Z1 G M)) (b : ↥(Z1 G A)) : ((explicitCup11 G M A P μ hμ hequiv) ↑a) ↑b = 0 ↔ ∃ (h : G → P), IsHeisenbergCochain μ a b h

A Heisenberg cochain exists exactly when the cup product vanishes: the explicit (1,1) cup product of the classes of a and b is zero in H²(G, P) if and only if (a, b) admits a Heisenberg cochain.

theorem TauCeti.ContCohomology.exists_isHeisenbergCochain_of_subsingleton_H2 {G : Type uG} [Group G] [TopologicalSpace G] [ContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] {μ : M →+ A →+ P} (hμ : Continuous fun (p : M × A) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (x : A), (μ (g • m)) (g • x) = g • (μ m) x) [Subsingleton (H2 G P)] (a : ↥(Z1 G M)) (b : ↥(Z1 G A)) : ∃ (h : G → P), IsHeisenbergCochain μ a b h

Heisenberg cochains exist when H²(G, P) vanishes, for instance on a free pro-p group with 𝔽_p-coefficients.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.apply_mul_of_smul_eq_self {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivA : ∀ (g : G) (x : A), g • x = x) (htrivP : ∀ (g : G) (x : P), g • x = x) (g g' : G) : h (g * g') = h g + h g' + (μ (↑a g)) (↑b g')

For trivial actions the Heisenberg law reads h (g * g') = h g + h g' + μ (a g) (b g').

theorem TauCeti.ContCohomology.IsHeisenbergCochain.apply_inv_of_smul_eq_self {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivA : ∀ (g : G) (x : A), g • x = x) (htrivP : ∀ (g : G) (x : P), g • x = x) (g : G) : h g⁻¹ = -h g + (μ (↑a g)) (↑b g)

For trivial actions, h g⁻¹ = -h g + μ (a g) (b g).

theorem TauCeti.ContCohomology.IsHeisenbergCochain.apply_commutatorElement_of_smul_eq_self {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivM : ∀ (g : G) (m : M), g • m = m) (htrivA : ∀ (g : G) (x : A), g • x = x) (htrivP : ∀ (g : G) (x : P), g • x = x) (g g' : G) : h ⁅g, g'⁆ = (μ (↑a g)) (↑b g') - (μ (↑a g')) (↑b g)

The value of a Heisenberg cochain on a commutator, for trivial actions: h ⁅g, g'⁆ = μ (a g) (b g') - μ (a g') (b g). This is the antisymmetric part of the cup pairing, read on the commutator g * g' * g⁻¹ * g'⁻¹.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.apply_pow_of_smul_eq_self {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivM : ∀ (g : G) (m : M), g • m = m) (htrivA : ∀ (g : G) (x : A), g • x = x) (htrivP : ∀ (g : G) (x : P), g • x = x) (g : G) (n : ℕ) : h (g ^ n) = n • h g + n.choose 2 • (μ (↑a g)) (↑b g)

The value of a Heisenberg cochain on a power, for trivial actions: h (g ^ n) = n • h g + (n.choose 2) • μ (a g) (b g). Besides the linear term n • h g, the n-th power picks up the diagonal value μ (a g) (b g) of the cup pairing, once for each of the n.choose 2 pairs of factors.