Inflation of the pro-p class module along V ≤ W

Let G be a profinite group and V ≤ W open subgroups. The transfer W → V^ab(p) of the canonical map V → V^ab(p) factors through W^ab(p), giving Ver_{W→V} = TauCeti.abelianizationProPTransferLe : W^ab(p) →* V^ab(p). It is continuous, and when V and W are normal in G it is equivariant along the quotient map G ⧸ V → G ⧸ W, so it forms a compatible pair with that map. The induced maps on explicit H¹ and H² are NSW's map i : Hⁱ(G ⧸ W, W^ab(p)) → Hⁱ(G ⧸ V, V^ab(p)) of (3.6.1)(ii), here TauCeti.abelianizationProPInfl1 and TauCeti.abelianizationProPInfl2.

On the class of an element of V, the transfer is the norm of W.map (mk' V), the image of W in G ⧸ V. The inflation of the class u_{G/W}(p) to G ⧸ V and the push-forward of u_{G/V}(p) along V^ab(p) → W^ab(p) differ by an explicit coboundary, and the norm of the finite normal subgroup W.map (mk' V) acts on H²(G ⧸ V, V^ab(p)) as multiplication by its order (TauCeti.ContCohomology.explicitCoeff2_eq_card_nsmul). Together these give NSW (3.6.1)(ii), i (u_{G/W}(p)) = (W : V) • u_{G/V}(p), with no hypothesis on the cohomological dimension.

When scd_p G ≤ 2, the induced map Ver_{W→V} : W^ab(p) →* V^ab(p) is injective with image the invariants of W.map (mk' V). This is NSW (3.6.4)(ii) for the group W. Its strict dimension is at most that of G, and the pair V ◁ W computed in W is identified with the restriction of the pair V ◁ G by TauCeti.abelianizationProPSubgroupOfEquiv. So i is inflation from (G ⧸ V) ⧸ W.map (mk' V) ≅ G ⧸ W with coefficients the invariants. The inflation-restriction sequence TauCeti.ContCohomology.explicitInfRes_exact then makes i in degree one injective with image the kernel of restriction to W.map (mk' V), NSW (1.6.7) for this pair. In degree two the same holds when H¹(W.map (mk' V), V^ab(p)) vanishes, by TauCeti.ContCohomology.explicitInfl2_injective and TauCeti.ContCohomology.explicitInfRes2_exact.

Main definitions

• TauCeti.abelianizationProPTransferLe: the transfer W^ab(p) →* V^ab(p) for V ≤ W.
• TauCeti.abelianizationProPInfl1 and TauCeti.abelianizationProPInfl2: the compatible-pair pullbacks along G ⧸ V → G ⧸ W and Ver_{W→V} on explicit H¹ and H².

Main results

• TauCeti.abelianizationProPTransferLe_mk: on the class of w : W, the map is Mathlib's transfer of V.subgroupOf W → V^ab(p) at w.
• TauCeti.abelianizationProPTransferLe_smul: equivariance along G ⧸ V → G ⧸ W.
• TauCeti.abelianizationProPTransferLe_mk_inclusion: on the class of v : V, the map is the norm of W.map (mk' V).
• TauCeti.abelianizationProPTransferLe_injective and TauCeti.abelianizationProPTransferLe_range: under scd_p G ≤ 2, the map is injective with image the W.map (mk' V)-invariants.
• TauCeti.abelianizationProPInfl1_injective and TauCeti.abelianizationProPInfl1_exact: under scd_p G ≤ 2, the map i in degree one is injective with image the kernel of restriction to W.map (mk' V).
• TauCeti.abelianizationProPInfl2_injective and TauCeti.abelianizationProPInfl2_exact: the same in degree two, when moreover H¹(W.map (mk' V), V^ab(p)) vanishes.
• TauCeti.abelianizationProPInfl2_class: NSW (3.6.1)(ii), i (u_{G/W}(p)) = (W : V) • u_{G/V}(p).

References

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

noncomputable def TauCeti.abelianizationProPTransferLe (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) : abelianizationProP p G W →* abelianizationProP p G V

The transfer Ver_{W→V} : W^ab(p) →* V^ab(p) for open V ≤ W: Mathlib's transfer W → V^ab(p) of the canonical map V.subgroupOf W ≃ V → V^ab(p), which is continuous and so factors through the maximal pro-p abelian quotient W^ab(p).

@[simp]

theorem TauCeti.abelianizationProPTransferLe_mk (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) (w : ↥W) : (abelianizationProPTransferLe p hVW hV) ((abelianizationProPMk p G W) w) = ((abelianizationProPMk p G V).comp (Subgroup.subgroupOfEquivOfLe hVW).toMonoidHom).transfer w

On the class of w : W, abelianizationProPTransferLe is the transfer of the canonical map V.subgroupOf W → V^ab(p) at w.

theorem TauCeti.continuous_abelianizationProPTransferLe (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) : Continuous ⇑(abelianizationProPTransferLe p hVW hV)

The transfer W^ab(p) →* V^ab(p) is continuous.

theorem TauCeti.abelianizationProPTransferLe_mk_eq_subgroupOfEquiv (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) (w : ↥W) : (abelianizationProPTransferLe p hVW hV) ((abelianizationProPMk p G W) w) = (abelianizationProPSubgroupOfEquiv p hVW) ((abelianizationProPTransfer p (↥W) (V.subgroupOf W)) w)

On the class of w : W, abelianizationProPTransferLe is the transfer of the group W to its own class module (V.subgroupOf W)^ab(p), read in V^ab(p) through the change of group abelianizationProPSubgroupOfEquiv. This is how the statements about abelianizationProPTransfer for the group W apply to it.

@[simp]

theorem TauCeti.abelianizationProPTransferLe_smul (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] (q : G ⧸ V) (x : abelianizationProP p G W) : (abelianizationProPTransferLe p hVW hV) ((QuotientGroup.mapOfLE hVW) q • x) = q • (abelianizationProPTransferLe p hVW hV) x

For V and W normal in G, the transfer W^ab(p) →* V^ab(p) is equivariant along the quotient map G ⧸ V → G ⧸ W: transfer is natural under the conjugation by g, which preserves both W and V.

theorem TauCeti.abelianizationProPTransferLe_injective (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) : Function.Injective ⇑(abelianizationProPTransferLe p hVW hV)

The transfer W^ab(p) → V^ab(p) is injective under scd_p G ≤ 2: this is abelianizationProPTransfer_eq_one_iff for the group W, whose strict dimension is at most that of G.

theorem TauCeti.abelianizationProPTransferLe_range (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) : (abelianizationProPTransferLe p hVW hV).range = FixedPoints.subgroup (↥(Subgroup.map (QuotientGroup.mk' V) W)) (abelianizationProP p G V)

The image of the transfer W^ab(p) → V^ab(p) under scd_p G ≤ 2 and for V normal in G is the subgroup of invariants of the image W.map (mk' V) of W in G ⧸ V. This is abelianizationProPTransfer_range for the group W, carried to G ⧸ V by the change of group.

theorem TauCeti.abelianizationProPTransferLe_mk_inclusion (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] (v : ↥V) : (abelianizationProPTransferLe p hVW hV) ((abelianizationProPMk p G W) ((Subgroup.inclusion hVW) v)) = ∏ s : ↥(Subgroup.map (QuotientGroup.mk' V) W), ↑s • (abelianizationProPMk p G V) v

On the class in W^ab(p) of an element v of V, the transfer W^ab(p) → V^ab(p) is the norm of the image W.map (mk' V) of W in G ⧸ V: Ver_{W→V} [v] = ∏ s, s • [v]. So the transfer after the map V^ab(p) → W^ab(p) induced by the inclusion is the norm of W ⧸ V.

theorem TauCeti.abelianizationProPTransferLe_toAdditive_smul (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] (q : G ⧸ V) (x : Additive (abelianizationProP p G W)) : (MonoidHom.toAdditive (abelianizationProPTransferLe p hVW hV)) ((QuotientGroup.mapOfLE hVW) q • x) = q • (MonoidHom.toAdditive (abelianizationProPTransferLe p hVW hV)) x

The equivariance of abelianizationProPTransferLe on the additive coefficient modules: the compatibility under which it pairs with G ⧸ V → G ⧸ W on explicit cohomology.

noncomputable def TauCeti.abelianizationProPInfl1 (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] : ContCohomology.H1 (G ⧸ W) (Additive (abelianizationProP p G W)) →+ ContCohomology.H1 (G ⧸ V) (Additive (abelianizationProP p G V))

NSW's map i : H¹(G ⧸ W, W^ab(p)) → H¹(G ⧸ V, V^ab(p)) of (3.6.1)(ii): the compatible-pair pullback along the quotient map G ⧸ V → G ⧸ W and the transfer W^ab(p) → V^ab(p).

theorem TauCeti.abelianizationProPInfl1_def (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] : abelianizationProPInfl1 p hVW hV = ContCohomology.explicitMap1 (G ⧸ W) (Additive (abelianizationProP p G W)) (G ⧸ V) (Additive (abelianizationProP p G V)) { toMonoidHom := QuotientGroup.mapOfLE hVW, continuous_toFun := ⋯ } (MonoidHom.toAdditive (abelianizationProPTransferLe p hVW hV)) ⋯ ⋯

abelianizationProPInfl1 is explicitMap1 along its compatible pair.

noncomputable def TauCeti.abelianizationProPInfl2 (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] : ContCohomology.H2 (G ⧸ W) (Additive (abelianizationProP p G W)) →+ ContCohomology.H2 (G ⧸ V) (Additive (abelianizationProP p G V))

NSW's map i : H²(G ⧸ W, W^ab(p)) → H²(G ⧸ V, V^ab(p)) of (3.6.1)(ii): the compatible-pair pullback along the quotient map G ⧸ V → G ⧸ W and the transfer W^ab(p) → V^ab(p).

theorem TauCeti.abelianizationProPInfl2_def (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] : abelianizationProPInfl2 p hVW hV = ContCohomology.explicitMap2 (G ⧸ W) (Additive (abelianizationProP p G W)) (G ⧸ V) (Additive (abelianizationProP p G V)) { toMonoidHom := QuotientGroup.mapOfLE hVW, continuous_toFun := ⋯ } (MonoidHom.toAdditive (abelianizationProPTransferLe p hVW hV)) ⋯ ⋯

abelianizationProPInfl2 is explicitMap2 along its compatible pair.

theorem TauCeti.abelianizationProPInfl1_injective (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) : Function.Injective ⇑(abelianizationProPInfl1 p hVW hV)

The map i is injective in degree one under scd_p G ≤ 2, NSW (1.6.7) for the pair V ≤ W: it is inflation, after the isomorphism of coefficients given by the transfer onto the invariants.

theorem TauCeti.abelianizationProPInfl1_exact (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) : (abelianizationProPInfl1 p hVW hV).range = (ContCohomology.explicitRes1 (G ⧸ V) (Additive (abelianizationProP p G V)) (Subgroup.map (QuotientGroup.mk' V) W)).ker

The image of i in degree one under scd_p G ≤ 2 is the kernel of restriction to the image W.map (mk' V) of W in G ⧸ V, NSW (1.6.7) for the pair V ≤ W.

theorem TauCeti.abelianizationProPInfl2_injective (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) [Subsingleton (ContCohomology.H1 (↥(Subgroup.map (QuotientGroup.mk' V) W)) (Additive (abelianizationProP p G V)))] : Function.Injective ⇑(abelianizationProPInfl2 p hVW hV)

The map i is injective in degree two under scd_p G ≤ 2, when H¹(W.map (mk' V), V^ab(p)) vanishes, NSW (1.6.7) for the pair V ≤ W: it is inflation, after the isomorphism of coefficients given by the transfer onto the invariants.

theorem TauCeti.abelianizationProPInfl2_exact (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) [Subsingleton (ContCohomology.H1 (↥(Subgroup.map (QuotientGroup.mk' V) W)) (Additive (abelianizationProP p G V)))] : (abelianizationProPInfl2 p hVW hV).range = (ContCohomology.explicitRes2 (G ⧸ V) (Additive (abelianizationProP p G V)) (Subgroup.map (QuotientGroup.mk' V) W)).ker

The image of i in degree two under scd_p G ≤ 2, when H¹(W.map (mk' V), V^ab(p)) vanishes, is the kernel of restriction to the image W.map (mk' V) of W in G ⧸ V, NSW (1.6.7) for the pair V ≤ W.

theorem TauCeti.abelianizationProPInfl2_class (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : Subgroup G} [V.FiniteIndex] (hVW : V ≤ W) (hV : IsOpen ↑V) [V.Normal] [W.Normal] : (abelianizationProPInfl2 p hVW hV) (abelianizationProPClass p G W ⋯) = V.relIndex W • abelianizationProPClass p G V hV

NSW (3.6.1)(ii). The map i carries the class u_{G/W}(p) to (W : V) • u_{G/V}(p). The inflation of u_{G/W}(p) to G ⧸ V and the push-forward of u_{G/V}(p) along V^ab(p) → W^ab(p) differ by a coboundary, and the transfer after V^ab(p) → W^ab(p) is the norm of W.map (mk' V), which acts on H²(G ⧸ V, V^ab(p)) as multiplication by its order (W : V). No hypothesis on the cohomological dimension of G is needed.