Conjugation-invariant classes in H¹ with trivial coefficients

Let N be a normal subgroup of a topological group G and M a topological G-module on which G acts trivially. Then H¹(N, M) is the group of continuous homomorphisms N → M (TauCeti.ContCohomology.H1EquivOfSmulEqSelf), and G acts on it through conjugation on N. The invariant classes H¹(N, M)^G are the continuous homomorphisms N → M that are constant on the conjugacy classes of G in N (mem_H1ConjInvariants_iff_of_smul_eq_self).

When M is killed by p, for instance M = 𝔽_p, such a homomorphism kills the p-th powers as well as the commutators ⁅N, G⁆. If moreover M is a T1Space, so that the kernel of a continuous homomorphism into M is closed, the homomorphism factors through the quotient N ⧸ Nᵖ[N, G] of N by the closed subgroup TauCeti.pLowerCentralStep p N, and conversely. Hence H¹(N, M)^G ≃ Hom_cont(N ⧸ Nᵖ[N, G], M) (H1ConjInvariantsEquivOfSmulEqSelf), for a closed normal subgroup N and a T1Space M killed by p. For M = 𝔽_p the right-hand side is the continuous 𝔽_p-dual of N ⧸ Nᵖ[N, G]; for a profinite group G its dimension is the topological generator rank of that quotient, which is worked out in TauCeti.Topology.Algebra.Group.Profinite.ProP.InvariantDual.

The invariant classes are the domain of the transgression in the five-term exact sequence of a group extension 1 → N → G → G ⧸ N → 1. For a minimal presentation 1 → R → F → G → 1 of a pro-p group by a free pro-p group, the transgression is an isomorphism, and the identification H¹(R, 𝔽_p)^F ≃ Hom_cont(R ⧸ Rᵖ[R, F], 𝔽_p) is what lets H²(G, 𝔽_p) count the generators of R as a closed normal subgroup of F.

Main results

• TauCeti.ContCohomology.mem_H1ConjInvariants_iff_of_smul_eq_self: for trivial coefficients, a class in H¹(N, M) is conjugation-invariant exactly when the continuous homomorphism N → M it represents is constant on the conjugacy classes of G in N.
• TauCeti.ContCohomology.H1ConjInvariantsEquivOfSmulEqSelf: for trivial T1Space coefficients killed by p and a closed normal subgroup N, H¹(N, M)^G is the group of continuous homomorphisms N ⧸ Nᵖ[N, G] → M.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, (3.9.5).
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), §1.4.

Invariant classes as conjugation-invariant homomorphisms

theorem TauCeti.ContCohomology.mk_mem_H1ConjInvariants_iff_of_smul_eq_self {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Subgroup G} [N.Normal] (htriv : ∀ (g : G) (m : M), g • m = m) {c : ↥(Z1 (↥N) M)} : ↑c ∈ H1ConjInvariants G M N ↔ ∀ (g : G) (n : ↥N), ↑c ((MulAut.conjNormal g) n) = ↑c n

For trivial coefficients, the class of a continuous 1-cocycle on N is conjugation-invariant exactly when the cocycle is constant on the conjugacy classes of G in N.

theorem TauCeti.ContCohomology.mem_H1ConjInvariants_iff_of_smul_eq_self {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Subgroup G} [N.Normal] (htriv : ∀ (g : G) (m : M), g • m = m) {x : H1 (↥N) M} : x ∈ H1ConjInvariants G M N ↔ ∀ (g : G) (n : ↥N), (Additive.toMul ((H1EquivOfSmulEqSelf ⋯) x)) ((MulAut.conjNormal g) n) = (Additive.toMul ((H1EquivOfSmulEqSelf ⋯) x)) n

For trivial coefficients, a class in H¹(N, M) is conjugation-invariant exactly when the continuous homomorphism N → M it represents is constant on the conjugacy classes of G in N.

Coefficients killed by p: characters of N ⧸ Nᵖ[N, G]

theorem TauCeti.ContCohomology.pLowerCentralStep_subgroupOf_le_ker_of_mem_H1ConjInvariants {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Subgroup G} [N.Normal] (htriv : ∀ (g : G) (m : M), g • m = m) (p : ℕ) [T1Space M] (hN : IsClosed ↑N) (hpM : ∀ (m : M), p • m = 0) {x : H1 (↥N) M} (hx : x ∈ H1ConjInvariants G M N) : (pLowerCentralStep p N).subgroupOf N ≤ (Additive.toMul ((H1EquivOfSmulEqSelf ⋯) x)).ker

For T1Space coefficients killed by p, the continuous homomorphism N → M representing a conjugation-invariant class kills Nᵖ[N, G]: its kernel is closed, so the characteristic property of pLowerCentralStep applies.

noncomputable def TauCeti.ContCohomology.H1ConjInvariantsEquivOfSmulEqSelf {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Subgroup G} [N.Normal] (htriv : ∀ (g : G) (m : M), g • m = m) (p : ℕ) [T1Space M] (hN : IsClosed ↑N) (hpM : ∀ (m : M), p • m = 0) : ↥(H1ConjInvariants G M N) ≃+ Additive (↥N ⧸ (pLowerCentralStep p N).subgroupOf N →ₜ* Multiplicative M)

Conjugation-invariant classes as characters of N ⧸ Nᵖ[N, G]. For a closed normal subgroup N of G and T1Space coefficients M with trivial G-action killed by p, the G-invariant classes in H¹(N, M) are the continuous homomorphisms N ⧸ Nᵖ[N, G] → M. A class is sent to the character of the quotient induced by the continuous homomorphism N → M it represents.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.H1ConjInvariantsEquivOfSmulEqSelf_apply_mk {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Subgroup G} [N.Normal] (htriv : ∀ (g : G) (m : M), g • m = m) (p : ℕ) [T1Space M] (hN : IsClosed ↑N) (hpM : ∀ (m : M), p • m = 0) (x : ↥(H1ConjInvariants G M N)) (n : ↥N) : (Additive.toMul ((H1ConjInvariantsEquivOfSmulEqSelf htriv p hN hpM) x)) ↑n = (Additive.toMul ((H1EquivOfSmulEqSelf ⋯) ↑x)) n

The character of N ⧸ Nᵖ[N, G] attached to a conjugation-invariant class takes, at the class of n, the value at n of the continuous homomorphism N → M representing the class.

@[simp]

theorem TauCeti.ContCohomology.H1ConjInvariantsEquivOfSmulEqSelf_symm_apply_coe {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Subgroup G} [N.Normal] (htriv : ∀ (g : G) (m : M), g • m = m) (p : ℕ) [T1Space M] (hN : IsClosed ↑N) (hpM : ∀ (m : M), p • m = 0) (ψ : Additive (↥N ⧸ (pLowerCentralStep p N).subgroupOf N →ₜ* Multiplicative M)) : ↑((H1ConjInvariantsEquivOfSmulEqSelf htriv p hN hpM).symm ψ) = (H1EquivOfSmulEqSelf ⋯).symm (Additive.ofMul ((Additive.toMul ψ).comp (ContinuousMonoidHom.quotientMk ((pLowerCentralStep p N).subgroupOf N))))

The conjugation-invariant class attached to a character ψ of N ⧸ Nᵖ[N, G] is represented by the composite of ψ with the quotient map.