The profinite extension associated with a pro-p class module

For a closed normal subgroup V of a profinite group G, kill the kernel of the canonical map V → Vᵃᵇ(p) inside G. The resulting quotient sits in an exact sequence

1 → Vᵃᵇ(p) → G / ker(V → Vᵃᵇ(p)) → G/V → 1.

The inclusion identifies the kernel with the existing pro-p class module, and the extension induces its existing conjugation action. This realizes the class-module kernel as the kernel of a profinite extension, so coefficient maps can be used in the extension lifting theorem.

For prime p and a finite group presented by a free profinite group on finitely many generators, take G to be the free group and V its presentation kernel. Lyndon's isomorphism TauCeti.freeProfiniteGroup.abelianizationProPEquivRelationModule identifies the resulting coefficient group, written additively, with the relation module.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.6.2) and the proof of (7.4.1).

noncomputable def TauCeti.abelianizationProPExtensionKernel (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) : Subgroup G

The kernel of V → Vᵃᵇ(p), regarded as a subgroup of the ambient group.

@[simp]

theorem TauCeti.mem_abelianizationProPExtensionKernel_iff (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) (g : G) : g ∈ abelianizationProPExtensionKernel p G V ↔ ∃ (hg : g ∈ V), (abelianizationProPMk p G V) ⟨g, hg⟩ = 1

An ambient element belongs to the extension kernel exactly when it belongs to V and has trivial image in Vᵃᵇ(p).

theorem TauCeti.abelianizationProPExtensionKernel_le (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) : abelianizationProPExtensionKernel p G V ≤ V

The extension kernel is contained in V.

instance TauCeti.abelianizationProPExtensionKernel_normal (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : (abelianizationProPExtensionKernel p G V).Normal

@[reducible, inline]

abbrev TauCeti.abelianizationProPExtensionGroup (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) : Type u

The total group of the extension with kernel Vᵃᵇ(p).

noncomputable def TauCeti.abelianizationProPExtensionInl (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : abelianizationProP p G V →* abelianizationProPExtensionGroup p G V

The inclusion of the class module into the total group, induced by V ↪ G.

@[simp]

theorem TauCeti.abelianizationProPExtensionInl_mk (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] (v : ↥V) : (abelianizationProPExtensionInl p G V) ((abelianizationProPMk p G V) v) = ↑↑v

The inclusion sends the class of v ∈ V to its class in the ambient quotient.

theorem TauCeti.abelianizationProPExtensionInl_injective (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : Function.Injective ⇑(abelianizationProPExtensionInl p G V)

The class-module inclusion is injective.

theorem TauCeti.range_abelianizationProPExtensionInl (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : (abelianizationProPExtensionInl p G V).range = (QuotientGroup.mapOfLE ⋯).ker

The inclusion has precisely the kernel of the projection as its range.

noncomputable def TauCeti.abelianizationProPExtension (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : GroupExtension (abelianizationProP p G V) (abelianizationProPExtensionGroup p G V) (G ⧸ V)

The quotient group is an extension of G/V by its pro-p class module.

@[simp]

theorem TauCeti.abelianizationProPExtension_inl (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : (abelianizationProPExtension p G V).inl = abelianizationProPExtensionInl p G V

The inclusion in the exact sequence is the canonical class-module inclusion.

@[simp]

theorem TauCeti.abelianizationProPExtension_rightHom (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : (abelianizationProPExtension p G V).rightHom = QuotientGroup.mapOfLE ⋯

The projection in the exact sequence is induced by G → G/V.

noncomputable def TauCeti.abelianizationProPExtensionSection (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : (abelianizationProPExtension p G V).Section

The section of the class-module extension given by the representatives Quotient.out.

@[simp]

theorem TauCeti.abelianizationProPExtensionSection_apply (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] (q : G ⧸ V) : (abelianizationProPExtensionSection p G V) q = ↑(Quotient.out q)

The canonical section sends a quotient class to the class of its chosen representative.

@[simp]

theorem TauCeti.factorSetFun_abelianizationProPExtensionSection (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] (q r : G ⧸ V) : Additive.ofMul (GroupExtension.factorSetFun (abelianizationProPExtensionSection p G V) (q, r)) = abelianizationProPFactorSet p G V (q, r)

The defect of the representative section of the class-module extension is the explicit class-module cocycle, read multiplicatively. No normalization of the representatives is needed.

theorem TauCeti.abelianizationProPExtension_inducesAction (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : GroupExtension.InducesAction (abelianizationProPExtension p G V)

Conjugation in the extension induces the canonical quotient action on Vᵃᵇ(p).

instance TauCeti.isClosed_abelianizationProPExtensionKernel (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [IsClosed ↑V] : IsClosed ↑(abelianizationProPExtensionKernel p G V)

The ambient extension kernel is closed.

theorem TauCeti.continuous_abelianizationProPExtensionInl (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] : Continuous ⇑(abelianizationProPExtensionInl p G V)

The inclusion of the class module is continuous.

@[reducible, inline]

noncomputable abbrev TauCeti.abelianizationProPProfiniteExtension (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] [CompactSpace G] [IsClosed ↑V] [TotallyDisconnectedSpace G] : ProfiniteGroupExtension (G ⧸ V) (abelianizationProP p G V)

The class-module extension as a profinite group extension with the canonical action.

@[simp]

theorem TauCeti.abelianizationProPProfiniteExtension_toGroupExtension (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [hV : V.Normal] [CompactSpace G] [IsClosed ↑V] [TotallyDisconnectedSpace G] : (abelianizationProPProfiniteExtension p G V).toGroupExtension = abelianizationProPExtension p G V

Bundling the topology retains the canonical exact sequence.