Lifting surjections after comparing generating extension classes

A continuous equivariant surjection between the kernels of two profinite extensions need not carry the source extension class to the target class. If its image class and the target class both generate the same finite cyclic p-group, a prime-to-p power of the coefficient map does carry one class to the other. For a pro-p target kernel this power is an automorphism, so the corrected coefficient map remains surjective and lifts to a continuous surjection of extensions.

This turns the cohomological comparison of relation-module maps into a surjection of groups: the correction changes the coefficient map, but not its image or its kernel.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., I §5 Exercise 4 and the proof of (7.4.1).

theorem TauCeti.ProfiniteGroupExtension.exists_surjective_continuousMonoidHom_of_generating_classes {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} {M : Type u_2} {N : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [CommGroup M] [TopologicalSpace M] [MulDistribMulAction G M] [ContinuousSMul G M] [CompactSpace M] [CommGroup N] [TopologicalSpace N] [IsTopologicalGroup N] [MulDistribMulAction G N] [ContinuousSMul G N] [CompactSpace N] [TotallyDisconnectedSpace N] (X : ProfiniteGroupExtension G M) (Y : ProfiniteGroupExtension G N) (hN : IsProP p N) (f : M →*[G] N) (hf : Continuous ⇑f) (hs : Function.Surjective ⇑f) (hx : AddSubgroup.zmultiples (X.map f hf).contCohomologyClass = ⊤) (hy : AddSubgroup.zmultiples Y.contCohomologyClass = ⊤) (hcard : ∃ (r : ℕ), Nat.card (ContCohomology.H2 G (Additive N)) = p ^ r) : ∃ (n : ℕ) (φ : X.E →ₜ* Y.E), p.Coprime n ∧ Function.Surjective ⇑φ ∧ (∀ (m : M), φ (X.toGroupExtension.inl m) = Y.toGroupExtension.inl (f m ^ n)) ∧ Y.toGroupExtension.rightHom.comp φ.toMonoidHom = X.toGroupExtension.rightHom

A continuous equivariant surjection to a pro-p kernel lifts to a continuous surjection of extensions after a prime-to-p power correction, provided its image extension class and the target class generate the same finite p-power-order cohomology group.

The lifted homomorphism covers the identity on the quotient and restricts to m ↦ (f m)^n on the kernels. In particular, the correction retains the kernel of f.