The functional on gr_1(G) of a Heisenberg cochain

Let G be a topological group, let M, A and P be G-modules with a pairing μ : M →+ A →+ P, let a : G → M and b : G → A be continuous 1-cocycles and let h : G → P be a Heisenberg cochain for (a, b) (TauCeti.ContCohomology.IsHeisenbergCochain), so that h (g * g') = h g + g • h g' + μ (a g) (g • b g').

Suppose that the action on P is trivial, that a and b vanish on the first term λ_1(G) of the lower p-series, which is automatic for trivial actions when M and A are killed by p (TauCeti.ContCohomology.apply_eq_zero_of_mem_Z1_of_mem_pLowerCentralSeries_one), and that P is killed by p. Then the Heisenberg law makes h a continuous homomorphism on λ_1(G), and its values on the p-th powers and on the commutators with G vanish, so h descends to an additive functional

gr_1(G) = λ_1(G) ⧸ λ_2(G) →+ P,

the graded restriction TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict of h. When the actions on M and A are trivial as well, its values on the two kinds of elements spanning gr_1(G) are the two components of the cup pairing of a and b:

• on a bracket [x, y] of degree-zero classes, the antisymmetric part μ (a x) (b y) - μ (a y) (b x);
• on a p-th power π x, the diagonal value (p choose 2) • μ (a x) (b x), which vanishes for odd p and is μ (a x) (b x) for p = 2.

By the transgression formula of TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.Transgression, the class of -h|_N for a closed normal N ≤ λ_1(G) transgresses to the cup product of the descended cocycles, and TauCeti.ContCohomology.IsHeisenbergCochain.negRestrict_apply_eq_neg_gradedRestrict_gradedMk records that this cocycle is -gradedRestrict composed with the projection N → gr_1(G). The graded restriction is thus the gr_1-side input to Labute's Proposition 3, which reads the cup product of a pro-p group off the class of a relator in gr_1 of the free group; that identification is not carried out here.

Main definitions

• TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict: the functional gr_1(G) →+ P induced by a Heisenberg cochain.

Main results

• TauCeti.ContCohomology.apply_eq_zero_of_mem_Z1_of_mem_pLowerCentralSeries_one: a continuous 1-cocycle for a trivial action on a group killed by p vanishes on λ_1(G).
• TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedMk: the defining equation gradedRestrict (gradedMk n) = h n.
• TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedBracket_gradedMkZero, TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedPow_gradedMkZero: the values on brackets and on p-th powers of degree-zero classes.
• TauCeti.ContCohomology.IsHeisenbergCochain.negRestrict_apply_eq_neg_gradedRestrict_gradedMk: the cocycle -h|_{λ_1} of the transgression formula is -gradedRestrict on classes.

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.apply_eq_zero_of_mem_Z1_of_mem_pLowerCentralSeries_one {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [T1Space M] [DistribMulAction G M] (htriv : ∀ (g : G) (m : M), g • m = m) (hpM : ∀ (m : M), p • m = 0) {f : G → M} (hf : f ∈ Z1 G M) {g : G} (hg : g ∈ pLowerCentralSeries p G 1) : f g = 0

Cocycles for a trivial action on a group killed by p vanish on λ_1(G). A continuous 1-cocycle for a trivial action is a continuous homomorphism, and its kernel is closed and contains the p-th powers and the commutators.

def TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) : gradedPiece p G 1 →+ P

The graded restriction of a Heisenberg cochain. For a Heisenberg cochain h of the cocycles a and b, with trivial action on P, a and b vanishing on λ_1(G) and P killed by p, the restriction of h to λ_1(G) is a continuous homomorphism killing λ_2(G), and this is the additive functional it induces on gr_1(G) = λ_1(G) ⧸ λ_2(G). Its defining equation is TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedMk, and when the actions on M and A are trivial as well, its values on brackets and p-th powers of degree-zero classes are the two components of the cup pairing of a and b (TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedBracket_gradedMkZero, TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedPow_gradedMkZero).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedMk {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) (n : ↥(pLowerCentralSeries p G 1)) : (hh.gradedRestrict htrivP haN hbN hP) (gradedMk p G 1 n) = h ↑n

The graded restriction on classes: the defining equation of TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.negRestrict_apply_eq_neg_gradedRestrict_gradedMk {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) [IsTopologicalAddGroup P] (n : ↥(pLowerCentralSeries p G 1)) : ↑(hh.negRestrict haN hbN) n = -(hh.gradedRestrict htrivP haN hbN hP) (gradedMk p G 1 n)

The cocycle -h|_{λ_1(G)} of the transgression formula is -gradedRestrict on classes.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedBracket_gradedMkZero {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) (htrivM : ∀ (g : G) (m : M), g • m = m) (htrivA : ∀ (g : G) (x : A), g • x = x) (g g' : G) : (hh.gradedRestrict htrivP haN hbN hP) (((gradedBracket p G 0 0) (gradedMkZero p G g)) (gradedMkZero p G g')) = (μ (↑a g)) (↑b g') - (μ (↑a g')) (↑b g)

The graded restriction on a bracket of degree-zero classes is the antisymmetric part of the cup pairing: [x, y] ↦ μ (a x) (b y) - μ (a y) (b x).

theorem TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedPow_gradedMkZero {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) (htrivM : ∀ (g : G) (m : M), g • m = m) (htrivA : ∀ (g : G) (x : A), g • x = x) (g : G) : (hh.gradedRestrict htrivP haN hbN hP) (gradedPow p G 0 (gradedMkZero p G g)) = p.choose 2 • (μ (↑a g)) (↑b g)

The graded restriction on a p-th power of a degree-zero class is the diagonal value of the cup pairing, weighted by p choose 2: π x ↦ (p choose 2) • μ (a x) (b x).

theorem TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedPow_gradedMkZero_of_odd {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) (htrivM : ∀ (g : G) (m : M), g • m = m) (htrivA : ∀ (g : G) (x : A), g • x = x) (hp : Odd p) (g : G) : (hh.gradedRestrict htrivP haN hbN hP) (gradedPow p G 0 (gradedMkZero p G g)) = 0

For odd p, the graded restriction vanishes on the p-th powers of degree-zero classes: p divides p choose 2, and P is killed by p.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_gradedPow_gradedMkZero_of_two {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) (htrivM : ∀ (g : G) (m : M), g • m = m) (htrivA : ∀ (g : G) (x : A), g • x = x) (hp : p = 2) (g : G) : (hh.gradedRestrict htrivP haN hbN hP) (gradedPow p G 0 (gradedMkZero p G g)) = (μ (↑a g)) (↑b g)

For p = 2, the graded restriction on the square of a degree-zero class is the diagonal value μ (a x) (b x) of the cup pairing.

theorem TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_degreeOneFamily_inl {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) (htrivM : ∀ (g : G) (m : M), g • m = m) (htrivA : ∀ (g : G) (x : A), g • x = x) {ι : Type u_1} [LT ι] (y : ι → G) (i : ι) : (hh.gradedRestrict htrivP haN hbN hP) (degreeOneFamily p y (Sum.inl i)) = p.choose 2 • (μ (↑a (y i))) (↑b (y i))

The graded restriction on the p-power members of a degree-one family: π (y i) ↦ (p choose 2) • μ (a (y i)) (b (y i)).

theorem TauCeti.ContCohomology.IsHeisenbergCochain.gradedRestrict_degreeOneFamily_inr {p : ℕ} {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] [T1Space P] [DistribMulAction G P] {μ : M →+ A →+ P} {a : ↥(Z1 G M)} {b : ↥(Z1 G A)} {h : G → P} (hh : IsHeisenbergCochain μ a b h) (htrivP : ∀ (g : G) (x : P), g • x = x) (haN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑a ↑n = 0) (hbN : ∀ (n : ↥(pLowerCentralSeries p G 1)), ↑b ↑n = 0) (hP : ∀ (x : P), p • x = 0) (htrivM : ∀ (g : G) (m : M), g • m = m) (htrivA : ∀ (g : G) (x : A), g • x = x) {ι : Type u_1} [LT ι] (y : ι → G) (ij : { ij : ι × ι // ij.1 < ij.2 }) : (hh.gradedRestrict htrivP haN hbN hP) (degreeOneFamily p y (Sum.inr ij)) = (μ (↑a (y (↑ij).1))) (↑b (y (↑ij).2)) - (μ (↑a (y (↑ij).2))) (↑b (y (↑ij).1))

The graded restriction on the bracket members of a degree-one family: [y i, y j] ↦ μ (a (y i)) (b (y j)) - μ (a (y j)) (b (y i)).