The class module under change of group

Let V ≤ W be subgroups of a topological group G, with V open and normal in G. The pair V.subgroupOf W ◁ W, computed inside the group W, has its own class module (V.subgroupOf W)^ab(p) with the conjugation action of W ⧸ V.subgroupOf W, and its own class u_{W/V}(p). This file identifies these with the restriction of the data of the pair V ◁ G to the subgroup W.map (mk' V) of G ⧸ V:

• the groups are identified by Subgroup.quotientSubgroupOfEquivMap, W ⧸ V.subgroupOf W ≃ₜ* W.map (mk' V);
• the coefficients are identified by TauCeti.abelianizationProPSubgroupOfEquiv, (V.subgroupOf W)^ab(p) ≃ₜ* V^ab(p), which intertwines the two conjugation actions (TauCeti.abelianizationProPSubgroupOfEquiv_smul);
• the compatible-pair pullbacks along this pair are additive equivalences TauCeti.abelianizationProPSubgroupOfH1Equiv and TauCeti.abelianizationProPSubgroupOfH2Equiv on explicit H¹ and H²;
• the latter carries u_{W/V}(p) to the restriction of u_{G/V}(p) to W.map (mk' V) (TauCeti.abelianizationProPSubgroupOfH2Equiv_class).

The last statement is not a tautology: the two classes are defined by factor sets built from different representatives, chosen by Quotient.out in W ⧸ V.subgroupOf W and in G ⧸ V respectively. If a_s = c_s * b_s relates the two choices of representatives of s, with c_s ∈ V, the two factor sets differ by the coboundary of s ↦ [c_s].

This is how statements about the class module of a pair V ◁ W with W an open subgroup of G are read off from statements about the pair V ◁ G, and conversely.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Proposition (3.6.1)(i).

noncomputable def TauCeti.abelianizationProPSubgroupOfEquiv (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} (hVW : V ≤ W) : abelianizationProP p (↥W) (V.subgroupOf W) ≃ₜ* abelianizationProP p G V

For subgroups V ≤ W, the maximal pro-p abelian quotient of V, computed inside W, is the one computed inside G: the isomorphism (V.subgroupOf W)^ab(p) ≃ₜ* V^ab(p) induced by Subgroup.subgroupOfContinuousMulEquivOfLe.

@[simp]

theorem TauCeti.abelianizationProPSubgroupOfEquiv_mk (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} (hVW : V ≤ W) (w : ↥W) (hw : w ∈ V.subgroupOf W) : (abelianizationProPSubgroupOfEquiv p hVW) ((abelianizationProPMk p (↥W) (V.subgroupOf W)) ⟨w, hw⟩) = (abelianizationProPMk p G V) ⟨↑w, hw⟩

abelianizationProPSubgroupOfEquiv sends the class of an element of V.subgroupOf W to the class of the same element of V.

theorem TauCeti.abelianizationProPSubgroupOfEquiv_mk_smul (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} (hVW : V ≤ W) [V.Normal] (w : ↥W) (x : abelianizationProP p (↥W) (V.subgroupOf W)) : (abelianizationProPSubgroupOfEquiv p hVW) (↑w • x) = ↑↑w • (abelianizationProPSubgroupOfEquiv p hVW) x

abelianizationProPSubgroupOfEquiv intertwines conjugation by w : W on (V.subgroupOf W)^ab(p) with conjugation by w on V^ab(p).

theorem TauCeti.abelianizationProPSubgroupOfEquiv_smul (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} (hVW : V ≤ W) [V.Normal] (hV : IsOpen ↑V) (q : ↥W ⧸ V.subgroupOf W) (x : abelianizationProP p (↥W) (V.subgroupOf W)) : (abelianizationProPSubgroupOfEquiv p hVW) (q • x) = ↑((V.quotientSubgroupOfEquivMap W hV) q) • (abelianizationProPSubgroupOfEquiv p hVW) x

abelianizationProPSubgroupOfEquiv intertwines the action of W ⧸ V.subgroupOf W on (V.subgroupOf W)^ab(p) with the action of its image in G ⧸ V on V^ab(p), the two quotients being identified by Subgroup.quotientSubgroupOfEquivMap.

theorem TauCeti.abelianizationProPSubgroupOfEquiv_toAdditive_smul (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} (hVW : V ≤ W) [V.Normal] (hV : IsOpen ↑V) (s : ↥(Subgroup.map (QuotientGroup.mk' V) W)) (x : Additive (abelianizationProP p (↥W) (V.subgroupOf W))) : (MulEquiv.toAdditive (abelianizationProPSubgroupOfEquiv p hVW).toMulEquiv) ((V.quotientSubgroupOfEquivMap W hV).symm s • x) = s • (MulEquiv.toAdditive (abelianizationProPSubgroupOfEquiv p hVW).toMulEquiv) x

On the additive coefficient modules, abelianizationProPSubgroupOfEquiv carries the action of (quotientSubgroupOfEquivMap V W hV).symm s to the action of s. This is the compatibility under which the pair of these two isomorphisms induces maps on explicit cohomology.

noncomputable def TauCeti.abelianizationProPSubgroupOfH1Equiv (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} [V.Normal] (hVW : V ≤ W) (hV : IsOpen ↑V) : ContCohomology.H1 (↥W ⧸ V.subgroupOf W) (Additive (abelianizationProP p (↥W) (V.subgroupOf W))) ≃+ ContCohomology.H1 (↥(Subgroup.map (QuotientGroup.mk' V) W)) (Additive (abelianizationProP p G V))

The change of group on explicit H¹: the compatible-pair pullback along (quotientSubgroupOfEquivMap V W hV).symm and abelianizationProPSubgroupOfEquiv p hVW, an isomorphism H¹(W ⧸ V.subgroupOf W, (V.subgroupOf W)^ab(p)) ≃+ H¹(W.map (mk' V), V^ab(p)).

theorem TauCeti.abelianizationProPSubgroupOfH1Equiv_def (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} [V.Normal] (hVW : V ≤ W) (hV : IsOpen ↑V) : abelianizationProPSubgroupOfH1Equiv p hVW hV = ContCohomology.explicitMap1Equiv (↥W ⧸ V.subgroupOf W) (Additive (abelianizationProP p (↥W) (V.subgroupOf W))) (↥(Subgroup.map (QuotientGroup.mk' V) W)) (Additive (abelianizationProP p G V)) (V.quotientSubgroupOfEquivMap W hV).symm (MulEquiv.toAdditive (abelianizationProPSubgroupOfEquiv p hVW).toMulEquiv) ⋯ ⋯ ⋯

abelianizationProPSubgroupOfH1Equiv is explicitMap1Equiv along its compatible pair.

noncomputable def TauCeti.abelianizationProPSubgroupOfH2Equiv (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} [V.Normal] (hVW : V ≤ W) (hV : IsOpen ↑V) : ContCohomology.H2 (↥W ⧸ V.subgroupOf W) (Additive (abelianizationProP p (↥W) (V.subgroupOf W))) ≃+ ContCohomology.H2 (↥(Subgroup.map (QuotientGroup.mk' V) W)) (Additive (abelianizationProP p G V))

The change of group on explicit H²: the compatible-pair pullback along (quotientSubgroupOfEquivMap V W hV).symm and abelianizationProPSubgroupOfEquiv p hVW, an isomorphism H²(W ⧸ V.subgroupOf W, (V.subgroupOf W)^ab(p)) ≃+ H²(W.map (mk' V), V^ab(p)).

theorem TauCeti.abelianizationProPSubgroupOfH2Equiv_def (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} [V.Normal] (hVW : V ≤ W) (hV : IsOpen ↑V) : abelianizationProPSubgroupOfH2Equiv p hVW hV = ContCohomology.explicitMap2Equiv (↥W ⧸ V.subgroupOf W) (Additive (abelianizationProP p (↥W) (V.subgroupOf W))) (↥(Subgroup.map (QuotientGroup.mk' V) W)) (Additive (abelianizationProP p G V)) (V.quotientSubgroupOfEquivMap W hV).symm (MulEquiv.toAdditive (abelianizationProPSubgroupOfEquiv p hVW).toMulEquiv) ⋯ ⋯ ⋯

abelianizationProPSubgroupOfH2Equiv is explicitMap2Equiv along its compatible pair.

theorem TauCeti.abelianizationProPSubgroupOfH2Equiv_class (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : Subgroup G} [V.Normal] (hVW : V ≤ W) (hV : IsOpen ↑V) : (abelianizationProPSubgroupOfH2Equiv p hVW hV) (abelianizationProPClass p (↥W) (V.subgroupOf W) ⋯) = (ContCohomology.explicitRes2 (G ⧸ V) (Additive (abelianizationProP p G V)) (Subgroup.map (QuotientGroup.mk' V) W)) (abelianizationProPClass p G V hV)

NSW (3.6.1)(i). The change of group carries the class u_{W/V}(p) of the pair V.subgroupOf W ◁ W to the restriction of the class u_{G/V}(p) to the subgroup W.map (mk' V) of G ⧸ V.