The pro-p class module for arbitrary finite quotients

Restriction to a Sylow p-subgroup reduces the class-module computation for an arbitrary finite quotient to the p-group case. The restriction is injective because its index is prime to p, while the change-of-group equivalences identify its target with the cohomology of the preimage of the Sylow subgroup.

Main results

For a profinite group G with scd_p G ≤ 2 and an open normal subgroup V:

• TauCeti.subsingleton_h1_abelianizationProP: H¹(G ⧸ V, V^ab(p)) = 0;
• TauCeti.abelianizationProPClass_generates: H²(G ⧸ V, V^ab(p)) is generated by the class u_{G/V}(p) and has order the p-part of #(G ⧸ V).

For an open subgroup U of G and V ◁ U open, these apply to the pair V ◁ U, since scd_p U ≤ scd_p G (TauCeti.strictCohomologicalDimensionAt_le_of_isClosed). Through the change of group, for V ≤ W:

• TauCeti.subsingleton_h1_map_abelianizationProP: H¹(W.map (mk' V), V^ab(p)) = 0;
• TauCeti.explicitRes2_abelianizationProPClass_generates: H²(W.map (mk' V), V^ab(p)) is generated by the restriction of u_{G/V}(p) and has order the p-part of #(W.map (mk' V)).

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.6.3) and (3.6.4), (i) ⇒ (iii).

theorem TauCeti.subsingleton_h1_abelianizationProP {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : Subgroup G} [V.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) (hV : IsOpen ↑V) : Subsingleton (ContCohomology.H1 (G ⧸ V) (Additive (abelianizationProP p G V)))

The first cohomology of the pro-p class module vanishes. If G has strict p-cohomological dimension at most two and V is open and normal, then H¹(G ⧸ V, V^ab(p)) is trivial.

theorem TauCeti.abelianizationProPClass_generates {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : Subgroup G} [V.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) (hV : IsOpen ↑V) : AddSubgroup.zmultiples (abelianizationProPClass p G V hV) = ⊤ ∧ Nat.card (ContCohomology.H2 (G ⧸ V) (Additive (abelianizationProP p G V))) = p ^ padicValNat p (Nat.card (G ⧸ V))

The pro-p class generates second cohomology. If G has strict p-cohomological dimension at most two and V is open and normal, then u_{G/V}(p) generates H²(G ⧸ V, V^ab(p)), whose order is the p-part of #(G ⧸ V).

theorem TauCeti.subsingleton_h1_map_abelianizationProP {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : Subgroup G} [V.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) (hV : IsOpen ↑V) {W : Subgroup G} (hVW : V ≤ W) : Subsingleton (ContCohomology.H1 (↥(Subgroup.map (QuotientGroup.mk' V) W)) (Additive (abelianizationProP p G V)))

The first cohomology of the pro-p class module on an open subgroup vanishes. If G has strict p-cohomological dimension at most two, V is open and normal and V ≤ W, then H¹(W.map (mk' V), V^ab(p)) is trivial.

theorem TauCeti.explicitRes2_abelianizationProPClass_generates {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : Subgroup G} [V.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) (hV : IsOpen ↑V) {W : Subgroup G} (hVW : V ≤ W) : AddSubgroup.zmultiples ((ContCohomology.explicitRes2 (G ⧸ V) (Additive (abelianizationProP p G V)) (Subgroup.map (QuotientGroup.mk' V) W)) (abelianizationProPClass p G V hV)) = ⊤ ∧ Nat.card (ContCohomology.H2 (↥(Subgroup.map (QuotientGroup.mk' V) W)) (Additive (abelianizationProP p G V))) = p ^ padicValNat p (Nat.card ↥(Subgroup.map (QuotientGroup.mk' V) W))

The restricted pro-p class generates second cohomology (NSW (3.6.1)(i) with (3.6.4)). If G has strict p-cohomological dimension at most two, V is open and normal and V ≤ W, then the restriction of u_{G/V}(p) generates H²(W.map (mk' V), V^ab(p)), whose order is the p-part of #(W.map (mk' V)).