The transgression of a cup product through a Heisenberg cochain

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

The main theorem is the computation of the transgression through h. Let N be a closed normal subgroup of a profinite group G on which a and b vanish, so that they descend to cocycles a' and b' on G ⧸ N with values in the N-invariants. Then -h is a transgression lift of its restriction -h|_N, which is a conjugation-invariant continuous 1-cocycle on N, and

tg [-h|_N] = a' ⌣ b'   in H²(G ⧸ N, P ^ N).

When the transgression is bijective, for instance for a minimal presentation 1 → R → F → G → 1 of a pro-p group by a free pro-p group F and 𝔽_p-coefficients, this identifies the cup product a' ⌣ b' ∈ H²(G, 𝔽_p) with the character r ↦ -h r of R ⧸ Rᵖ[R, F]; so the value of the cup product on a relator r ∈ R ⊆ Fᵖ[F, F] is -h r, which the commutator and power formulas of TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.Heisenberg evaluate once r is written as a product of p-th powers and commutators of the generators, as in Labute's Proposition 3.

Main definitions

• TauCeti.ContCohomology.IsHeisenbergCochain.negRestrict: the restriction -h|_N, a continuous 1-cocycle on a normal subgroup N on which a and b vanish.

Main results

• TauCeti.ContCohomology.IsHeisenbergCochain.isTransgressionLift: -h is a transgression lift of -h|_N, and TauCeti.ContCohomology.IsHeisenbergCochain.negRestrict_mem_H1ConjInvariants: the class of -h|_N is conjugation-invariant.
• TauCeti.ContCohomology.IsHeisenbergCochain.transgression_negRestrict: the transgression of -h|_N is the cup product of the descended cocycles.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §1.4 and Proposition 3.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter III, §9.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.isTransgressionLift {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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] [IsTopologicalAddGroup 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) : IsTransgressionLift (fun (n : ↥N) => -h ↑n) fun (g : G) => -h g

A Heisenberg cochain is a transgression lift. If a and b vanish on the normal subgroup N, then -h is a transgression lift of its restriction -h|_N.

def TauCeti.ContCohomology.IsHeisenbergCochain.negRestrict {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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] [IsTopologicalAddGroup 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) : ↥(Z1 (↥N) P)

The restriction -h|_N of a Heisenberg cochain to a normal subgroup N on which a and b vanish, a continuous 1-cocycle on N. Its class is conjugation-invariant (TauCeti.ContCohomology.IsHeisenbergCochain.negRestrict_mem_H1ConjInvariants) and transgresses to the cup product of the descended cocycles (TauCeti.ContCohomology.IsHeisenbergCochain.transgression_negRestrict).

Equations

• hh.negRestrict haN hbN = ⟨fun (n : ↥N) => -h ↑n, ⋯⟩

@[simp]

theorem TauCeti.ContCohomology.IsHeisenbergCochain.coe_negRestrict {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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] [IsTopologicalAddGroup 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) : ↑(hh.negRestrict haN hbN) = fun (n : ↥N) => -h ↑n

The restriction -h|_N, as a function on N.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.negRestrict_mem_H1ConjInvariants {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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] [IsTopologicalAddGroup 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] [ContinuousSMul G P] (haN : ∀ (n : ↥N), ↑a ↑n = 0) (hbN : ∀ (n : ↥N), ↑b ↑n = 0) : ↑(hh.negRestrict haN hbN) ∈ H1ConjInvariants G P N

The class of -h|_N in H¹(N, P) is conjugation-invariant.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.transgression_negRestrict {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace 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] [IsTopologicalAddGroup P] [DiscreteTopology P] [DistribMulAction G P] [ContinuousSMul G P] {N : Subgroup G} [N.Normal] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A)] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) 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)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (hN : IsClosed ↑N) (haN : ∀ (n : ↥N), ↑a ↑n = 0) (hbN : ∀ (n : ↥N), ↑b ↑n = 0) : (transgression G P N hN) ⟨↑(hh.negRestrict haN hbN), ⋯⟩ = ((explicitCup11 (G ⧸ N) (↥(FixedPoints.addSubgroup (↥N) M)) (↥(FixedPoints.addSubgroup (↥N) A)) (↥(FixedPoints.addSubgroup (↥N) P)) (N.fixedPointsPairing μ ⋯) ⋯ ⋯) ↑(descendZ1 a haN)) ↑(descendZ1 b hbN)

The transgression of -h|_N is the cup product. Let N be a closed normal subgroup of a profinite group G, let a and b be continuous 1-cocycles vanishing on N, with descents a' and b' to G ⧸ N valued in the N-invariants, and let h be a Heisenberg cochain for (a, b). Then the transgression H¹(N, P)^{G ⧸ N} → H²(G ⧸ N, P ^ N) sends the class of -h|_N to the explicit (1,1) cup product a' ⌣ b' for the pairing induced by μ on the invariants.