The class of the pro-p class module generates H² for a cyclic quotient

Let G be a profinite group with scd_p G ≤ 2 and let V be an open normal subgroup such that G ⧸ V is a cyclic p-group. Then H²(G ⧸ V, V^ab(p)) is cyclic of order #(G ⧸ V), generated by the class u_{G/V}(p) of the factor set of the extension of G ⧸ V by V^ab(p) (TauCeti.abelianizationProPClass). This is the degree-two half of NSW (3.6.4), (ii) ⇒ (iii), for a cyclic quotient; it is the class formation axiom that, together with the vanishing of H¹, makes the modules V^ab(p) a p-class formation for G. The prime-order case is the base case of the induction over p-group quotients in NSW (3.6.4).

The computation runs through the description H²(Γ, A) ≅ A^Γ / N(A) of the second cohomology of a finite cyclic group Γ = ⟨σ⟩ (TauCeti.ContCohomology.explicitH2CyclicEquiv), which sends u_{G/V}(p) to the class of ∑_τ u(τ, σ), that is, of the transfer Ver σ.out (TauCeti.abelianizationProPTransfer_out). Reading the transfer Ver : G → V^ab(p) in A^Γ / N(A) gives a homomorphism from G:

• it is onto, because under scd_p G ≤ 2 the image of Ver is the subgroup of invariants (TauCeti.abelianizationProPTransfer_range);
• its kernel is V. On V the transfer is the norm (TauCeti.abelianizationProPTransfer_apply_of_mem). Conversely, if Ver g is the norm of the class of v ∈ V, then Ver (g v⁻¹) = 1, so g v⁻¹ dies in G^ab(p) (TauCeti.abelianizationProPTransfer_eq_one_iff), and hence in the abelian p-group G ⧸ V, which is a quotient of G^ab(p).

So A^Γ / N(A) is isomorphic to G ⧸ V, the image of u_{G/V}(p) corresponding to the generator σ.

Main results

• TauCeti.abelianizationProPClass_generates_of_isCyclic: for a cyclic p-group quotient G ⧸ V, the class u_{G/V}(p) generates H²(G ⧸ V, V^ab(p)), a group of order #(G ⧸ V).
• TauCeti.abelianizationProPClass_generates_of_card_eq_prime: the case #(G ⧸ V) = p.

References

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

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

The class of the pro-p class module generates H² for a cyclic quotient (NSW (3.6.4), (ii) ⇒ (iii), in degree two and p-primary form). For a profinite group G with scd_p G ≤ 2 and an open normal subgroup V whose quotient G ⧸ V is a cyclic p-group, the class u_{G/V}(p) generates H²(G ⧸ V, V^ab(p)), and this group has order #(G ⧸ V).

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

The class of the pro-p class module generates H² for a quotient of prime order. For a profinite group G with scd_p G ≤ 2 and an open normal subgroup V of prime index p, the class u_{G/V}(p) generates H²(G ⧸ V, V^ab(p)), a group of order p. This is the base case of the induction over p-group quotients in NSW (3.6.4).