The continuous cohomology obstruction to a finite embedding problem

For G → Q ← E with abelian kernel N, conjugation gives a Q-action on N, restricted to G along π. The obstruction is the class of the pullback extension in canonical continuous H²(G, N). It vanishes exactly when the embedding problem has a solution with open kernel.

If canonical continuous H²(G, M) vanishes for every finite discrete abelian G-module annihilated by p, then HasElementaryAbelianSolutions p G holds. This is the cohomological input for solvability of embedding problems with finite p-group kernel.

In the other direction, let G be a projective pro-p group (TauCeti.IsProjective). Every profinite extension of G by a pro-p group splits (GroupExtension.exists_splitting_continuous_of_isProjective), and read through the classification of profinite extensions by continuous H² this is the vanishing of the second continuous cohomology of G with coefficients in any profinite pro-p abelian G-module M (TauCeti.IsProjective.subsingleton_H2): every class of the explicit H²(G, M) is the class of a profinite extension of G by M, and the class of a split extension is zero. The extension dictionary reads its abelian kernel multiplicatively, so the vanishing is first stated for a CommGroup M; an AddCommGroup M is Additive (Multiplicative M), and TauCeti.IsProjective.subsingleton_H2_of_isPPrimaryTorsion restates the vanishing for it. Transported through the degree-two comparison with Mathlib's continuousCohomology, the statement takes its canonical form for a finite discrete p-primary G-module (TauCeti.IsProjective.subsingleton_continuousCohomology_two_of_isPPrimaryTorsion), which is the input to cd_p G ≤ 1 in TauCeti.Topology.Algebra.Group.Profinite.EmbeddingProblem.CohomologicalDimension. The vanishing of H² of a free pro-p group in TauCeti.Topology.Algebra.Group.Profinite.Free.Cohomology is the instance of these statements at freeProP p X.

Main results

• TauCeti.FiniteEmbeddingProblem.obstruction, TauCeti.FiniteEmbeddingProblem.exists_isSolution_iff_obstruction_eq_zero: the class of the pullback extension in H²(G, ker α) vanishes exactly when the embedding problem is solvable.
• TauCeti.hasElementaryAbelianSolutions_of_subsingleton_continuousCohomology_two: vanishing of H² on finite discrete modules killed by p solves the embedding problems with elementary abelian p-kernel.
• TauCeti.IsProjective.subsingleton_H2: H²(G, M) = 0 for G projective pro-p and M a profinite pro-p abelian G-module.
• TauCeti.IsProjective.subsingleton_H2_of_isPPrimaryTorsion: the same for a profinite p-primary torsion abelian G-module written additively.
• TauCeti.IsProjective.subsingleton_continuousCohomology_two_of_isPPrimaryTorsion: the same in Mathlib's continuous cohomology, for a finite discrete p-primary G-module.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §3.4 and §5.9.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. III, §5.
• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Section 7.6.

noncomputable def TauCeti.FiniteEmbeddingProblem.obstruction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] [DiscreteTopology P.E] [TopologicalSpace P.Q] [DiscreteTopology P.Q] (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) : ↑(continuousCohomology 2 (ofDiscreteModule ℤ G (Additive ↥P.α.ker))).toModuleCat

The class of the pullback extension in canonical continuous H²(G, ker α), with the conjugation action restricted along π.

Equations

• P.obstruction hcomm = (TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology G (Additive ↥P.α.ker)) (P.pullbackExtension hcomm).contCohomologyClass

theorem TauCeti.FiniteEmbeddingProblem.obstruction_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] [DiscreteTopology P.E] [TopologicalSpace P.Q] [DiscreteTopology P.Q] (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) : P.obstruction hcomm = (ContCohomology.explicitH2AddEquivContinuousCohomology G (Additive ↥P.α.ker)) (P.pullbackExtension hcomm).contCohomologyClass

The obstruction is the image of the pullback extension's cohomology class under the comparison isomorphism from explicit continuous H² to canonical continuous H².

theorem TauCeti.FiniteEmbeddingProblem.exists_isSolution_iff_obstruction_eq_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] [DiscreteTopology P.E] [TopologicalSpace P.Q] [DiscreteTopology P.Q] (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) : (∃ (β : G →* P.E), P.IsSolution β) ↔ P.obstruction hcomm = 0

An embedding problem with abelian kernel has a solution exactly when its canonical continuous cohomology obstruction vanishes.

theorem TauCeti.FiniteEmbeddingProblem.exists_isSolution_of_subsingleton_continuousCohomology_two {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] [DiscreteTopology P.E] [TopologicalSpace P.Q] [DiscreteTopology P.Q] (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) (h : Subsingleton ↑(continuousCohomology 2 (ofDiscreteModule ℤ G (Additive ↥P.α.ker))).toModuleCat) : ∃ (β : G →* P.E), P.IsSolution β

Vanishing of canonical continuous H² for the actual kernel module solves the embedding problem.

theorem TauCeti.hasElementaryAbelianSolutions_of_subsingleton_continuousCohomology_two {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} (h : ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [Finite M] [inst_4 : DistribMulAction G M] [ContinuousSMul G M], (∀ (m : M), p • m = 0) → Subsingleton ↑(continuousCohomology 2 (ofDiscreteModule ℤ G M)).toModuleCat) : HasElementaryAbelianSolutions p G

If canonical continuous H²(G, M) vanishes for every finite discrete abelian G-module annihilated by p, then every finite embedding problem for G with commutative kernel killed by p has a solution. For prime p these are the elementary abelian p-primary modules.

The vanishing of H² of a projective pro-p group

theorem TauCeti.IsProjective.subsingleton_H2 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} {M : Type v} [CommGroup M] [TopologicalSpace M] [IsTopologicalGroup M] [CompactSpace M] [TotallyDisconnectedSpace M] [MulDistribMulAction G M] [ContinuousSMul G M] (hproj : IsProjective p G) (hG : IsProP p G) (hM : IsProP p M) : Subsingleton (ContCohomology.H2 G (Additive M))

H² of a projective pro-p group vanishes. For G projective pro-p and M a profinite pro-p abelian group with a continuous action of G, the explicit second continuous cohomology group H²(G, M) is zero: every class is the class of a profinite extension of G by M, which splits.

theorem TauCeti.IsProjective.subsingleton_H2_of_isPPrimaryTorsion {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [CompactSpace M] [TotallyDisconnectedSpace M] [DistribMulAction G M] [ContinuousSMul G M] (hproj : IsProjective p G) (hG : IsProP p G) (hM : IsPPrimaryTorsion p M) : Subsingleton (ContCohomology.H2 G M)

H² of a projective pro-p group vanishes, additive form. For G projective pro-p and M a profinite p-primary torsion abelian group, written additively, with a continuous action of G, the explicit second continuous cohomology group H²(G, M) is zero.

theorem TauCeti.IsProjective.subsingleton_continuousCohomology_two_of_isPPrimaryTorsion {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} (hproj : IsProjective p G) (hG : IsProP p G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [Finite M] [DistribMulAction G M] [ContinuousSMul G M] (hM : IsPPrimaryTorsion p M) : Subsingleton ↑(continuousCohomology 2 (ofDiscreteModule ℤ G M)).toModuleCat

H² of a projective pro-p group vanishes on finite coefficients, in Mathlib's continuous cohomology: for G projective pro-p and M a finite discrete p-primary torsion abelian group with a continuous action of G, the canonical continuousCohomology 2 of the topological representation attached to M is zero.