Prime-to-p restriction for the pro-p class module

Power maps of exponent prime to p are automorphisms of the pro-p class module. Consequently, restriction from a finite quotient to a subgroup of index prime to p is injective in degrees one and two.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.6.3) and (3.6.4), (i) ⇒ (iii).

theorem TauCeti.abelianizationProP_pow_bijective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) (V : Subgroup G) (hV : IsOpen ↑V) (m : ℕ) (hm : m.Coprime p) : Function.Bijective fun (a : abelianizationProP p G V) => a ^ m

The m-th power map on V^ab(p) is bijective when m is prime to p.

theorem TauCeti.abelianizationProPRes1_injective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) (V : Subgroup G) [V.Normal] (hV : IsOpen ↑V) (S : Subgroup (G ⧸ V)) (hS : ¬p ∣ S.index) : Function.Injective ⇑(ContCohomology.explicitRes1 (G ⧸ V) (Additive (abelianizationProP p G V)) S)

Restriction to a subgroup of index prime to p is injective on the first cohomology of the pro-p class module.

theorem TauCeti.abelianizationProPRes2_injective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) (V : Subgroup G) [V.Normal] (hV : IsOpen ↑V) (S : Subgroup (G ⧸ V)) (hS : ¬p ∣ S.index) : Function.Injective ⇑(ContCohomology.explicitRes2 (G ⧸ V) (Additive (abelianizationProP p G V)) S)

Restriction to a subgroup of index prime to p is injective on the second cohomology of the pro-p class module.