The cyclic-quotient kernel in the pro-p class module

Let V be an open normal subgroup of a profinite group G, with cyclic p-group quotient generated by the class of s. An element of V with trivial image in G^ab(p) has image in V^ab(p) of the form (s • b) / b. This identifies the kernel needed in the cyclic computation of the first cohomology of the class module.

Use exists_abelianizationProPMk_eq_smul_div_of_mk_eq_one to obtain the witness b. The converse, giving the full kernel characterization, is exists_abelianizationProPMk_eq_smul_div_iff_mk_eq_one.

References

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

theorem TauCeti.exists_abelianizationProPMk_eq_smul_div_of_mk_eq_one (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] [CompactSpace G] [TotallyDisconnectedSpace G] (hV : IsOpen ↑V) (hpV : IsPGroup p (G ⧸ V)) (s : G) (hs : ∀ (q : G ⧸ V), q ∈ Subgroup.zpowers ↑s) (v : ↥V) (hv : (maximalProPQuotient.mk p (TopologicalAbelianization G)) ↑↑v = 1) : ∃ (b : abelianizationProP p G V), (abelianizationProPMk p G V) v = ↑s • b / b

The cyclic-quotient kernel calculation for the pro-p class module. If G ⧸ V is a cyclic p-group generated by the class of s, an element of V killed in G^ab(p) has class (s • b) / b in V^ab(p). No cohomological-dimension hypothesis is needed.

theorem TauCeti.exists_abelianizationProPMk_eq_smul_div_iff_mk_eq_one (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] [CompactSpace G] [TotallyDisconnectedSpace G] (hV : IsOpen ↑V) (hpV : IsPGroup p (G ⧸ V)) (s : G) (hs : ∀ (q : G ⧸ V), q ∈ Subgroup.zpowers ↑s) (v : ↥V) : (∃ (b : abelianizationProP p G V), (abelianizationProPMk p G V) v = ↑s • b / b) ↔ (maximalProPQuotient.mk p (TopologicalAbelianization G)) ↑↑v = 1

The kernel characterization for a cyclic p-group quotient. An element of V dies in G^ab(p) exactly when its class in V^ab(p) is a difference (s • b) / b, where the class of s generates G ⧸ V.