Functoriality of the pro-p class-module extension

A continuous homomorphism f : G → H carrying a normal subgroup V into W descends to G / ker(V → Vᵃᵇ(p)) → H / ker(W → Wᵃᵇ(p)). The descended map commutes with the projections to G/V and H/W. No surjectivity of f, or of its restriction to V, is required.

In particular, a lift from a free profinite presentation to an arithmetic Galois group gives a comparison between their class-module extensions. This comparison can detect a generating extension class independently of a separately constructed surjection on the kernels.

If f maps V onto W, its map on class modules is surjective. For normal subgroups, that map intertwines the quotient conjugation actions.

The construction uses TopologicalAbelianization.map followed by maximalProPQuotient.map to show that the extension kernels are preserved.

References

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

noncomputable def TauCeti.abelianizationProPMap (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) : abelianizationProP p G V →* abelianizationProP p H W

The map on pro-p class modules induced by a continuous homomorphism carrying V into W.

theorem TauCeti.continuous_abelianizationProPMap (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) : Continuous ⇑(abelianizationProPMap p f hf hVW)

The induced map on pro-p class modules is continuous.

@[simp]

theorem TauCeti.abelianizationProPMap_mk (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) (v : ↥V) : (abelianizationProPMap p f hf hVW) ((abelianizationProPMk p G V) v) = (abelianizationProPMk p H W) ⟨f ↑v, ⋯⟩

The induced class-module map sends the class of v to the class of f v.

theorem TauCeti.abelianizationProPMap_surjective (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) (hWV : W ≤ Subgroup.map f V) : Function.Surjective ⇑(abelianizationProPMap p f hf hVW)

Surjectivity on the specified subgroups implies surjectivity on their pro-p class modules. Surjectivity on the ambient groups is not required.

@[simp]

theorem TauCeti.abelianizationProPMap_id (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Subgroup G} : abelianizationProPMap p (MonoidHom.id G) ⋯ ⋯ = MonoidHom.id (abelianizationProP p G V)

The identity induces the identity on a pro-p class module.

theorem TauCeti.abelianizationProPMap_comp (p : ℕ) {G : Type u_1} {H : Type u_2} {J : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group J] [TopologicalSpace J] [IsTopologicalGroup J] {V : Subgroup G} {W : Subgroup H} {U : Subgroup J} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) (g : H →* J) (hg : Continuous ⇑g) (hWU : W ≤ Subgroup.comap g U) : abelianizationProPMap p (g.comp f) ⋯ ⋯ = (abelianizationProPMap p g hg hWU).comp (abelianizationProPMap p f hf hVW)

Composition of ambient homomorphisms induces composition on pro-p class modules. The intermediate subgroup W must be specified when rewriting this identity.

theorem TauCeti.abelianizationProPExtensionKernel_le_comap (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) : abelianizationProPExtensionKernel p G V ≤ Subgroup.comap f (abelianizationProPExtensionKernel p H W)

A continuous homomorphism preserving the specified subgroups also preserves the kernels killed in their pro-p class-module extensions.

@[simp]

theorem TauCeti.abelianizationProPMap_smul (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) [V.Normal] [W.Normal] (g : G) (a : abelianizationProP p G V) : (abelianizationProPMap p f hf hVW) (↑g • a) = ↑(f g) • (abelianizationProPMap p f hf hVW) a

The induced class-module map intertwines conjugation by an ambient element with conjugation by its image.

noncomputable def TauCeti.abelianizationProPExtensionMap (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) [V.Normal] [W.Normal] : abelianizationProPExtensionGroup p G V →ₜ* abelianizationProPExtensionGroup p H W

The continuous map on total groups of pro-p class-module extensions induced by a continuous homomorphism carrying V into W.

@[simp]

theorem TauCeti.abelianizationProPExtensionMap_mk (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) [V.Normal] [W.Normal] (x : G) : (abelianizationProPExtensionMap p f hf hVW) ↑x = ↑(f x)

The induced total-group map sends the class of x to the class of f x.

theorem TauCeti.abelianizationProPExtensionMap_unique (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) [V.Normal] [W.Normal] (φ : abelianizationProPExtensionGroup p G V →ₜ* abelianizationProPExtensionGroup p H W) (hφ : ∀ (x : G), φ ↑x = ↑(f x)) : φ = abelianizationProPExtensionMap p f hf hVW

The induced total-group map is uniquely determined by its values on representatives.

theorem TauCeti.abelianizationProPExtensionMap_surjective (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) [V.Normal] [W.Normal] (hs : Function.Surjective ⇑f) : Function.Surjective ⇑(abelianizationProPExtensionMap p f hf hVW)

Surjectivity of an ambient homomorphism implies surjectivity on the total groups of the class-module extensions; surjectivity on the specified subgroups is not needed.

theorem TauCeti.abelianizationProPExtensionMap_comp_inl (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) [V.Normal] [W.Normal] : (abelianizationProPExtensionMap p f hf hVW).comp (abelianizationProPExtension p G V).inl = (abelianizationProPExtension p H W).inl.comp (abelianizationProPMap p f hf hVW)

The map of total groups agrees with the induced class-module map on the kernels.

theorem TauCeti.rightHom_comp_abelianizationProPExtensionMap (p : ℕ) {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {V : Subgroup G} {W : Subgroup H} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) [V.Normal] [W.Normal] : (abelianizationProPExtension p H W).rightHom.comp (abelianizationProPExtensionMap p f hf hVW).toMonoidHom = (QuotientGroup.map V W f hVW).comp (abelianizationProPExtension p G V).rightHom

The map of total groups covers the induced map of quotient groups.

@[simp]

theorem TauCeti.abelianizationProPExtensionMap_id (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Subgroup G} [V.Normal] : abelianizationProPExtensionMap p (MonoidHom.id G) ⋯ ⋯ = ContinuousMonoidHom.id (abelianizationProPExtensionGroup p G V)

The identity induces the identity on the total group of a class-module extension.

theorem TauCeti.abelianizationProPExtensionMap_comp (p : ℕ) {G : Type u_1} {H : Type u_2} {J : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group J] [TopologicalSpace J] [IsTopologicalGroup J] {V : Subgroup G} {W : Subgroup H} {U : Subgroup J} (f : G →* H) (hf : Continuous ⇑f) (hVW : V ≤ Subgroup.comap f W) [V.Normal] [W.Normal] [U.Normal] (g : H →* J) (hg : Continuous ⇑g) (hWU : W ≤ Subgroup.comap g U) : abelianizationProPExtensionMap p (g.comp f) ⋯ ⋯ = (abelianizationProPExtensionMap p g hg hWU).comp (abelianizationProPExtensionMap p f hf hVW)

Composition of ambient homomorphisms induces composition on class-module extensions. The intermediate subgroup W must be specified when rewriting this identity.