From a weak comparison to a surjection of profinite extensions

Suppose two profinite extensions have second cohomology groups of the same finite order, and the target extension class generates its group. Any continuous homomorphism between the extensions over the identity of the quotient, even a nonsurjective one, shows that the source extension class also generates. Its restriction to the kernels is a continuous equivariant coefficient map carrying the source class to the target class.

Consequently, a different continuous equivariant surjection on kernels, inducing an isomorphism on second cohomology, lifts after a prime-to-p power correction to a surjection of extensions when the target kernel is pro-p and its second cohomology has p-power order. This separates the weak comparison used to detect a generating class from the coefficient surjection one needs to lift.

References

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

noncomputable def TauCeti.ProfiniteGroupExtension.equivariantKernelMap {G : Type u_1} {M : Type u_2} {N : Type u_3} [Group G] [TopologicalSpace G] [CommGroup M] [TopologicalSpace M] [MulDistribMulAction G M] [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (X : ProfiniteGroupExtension G M) (Y : ProfiniteGroupExtension G N) (φ : X.E →ₜ* Y.E) (hright : Y.toGroupExtension.rightHom.comp φ.toMonoidHom = X.toGroupExtension.rightHom) : M →*[G] N

Restrict a continuous homomorphism of profinite extensions over the identity of the quotient to their kernels, with their prescribed quotient actions.

@[simp]

theorem TauCeti.ProfiniteGroupExtension.inl_equivariantKernelMap {G : Type u_1} {M : Type u_2} {N : Type u_3} [Group G] [TopologicalSpace G] [CommGroup M] [TopologicalSpace M] [MulDistribMulAction G M] [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (X : ProfiniteGroupExtension G M) (Y : ProfiniteGroupExtension G N) (φ : X.E →ₜ* Y.E) (hright : Y.toGroupExtension.rightHom.comp φ.toMonoidHom = X.toGroupExtension.rightHom) (m : M) : Y.toGroupExtension.inl ((X.equivariantKernelMap Y φ hright) m) = φ (X.toGroupExtension.inl m)

The equivariant kernel restriction agrees with the original map after inclusion.

theorem TauCeti.ProfiniteGroupExtension.continuous_equivariantKernelMap {G : Type u_1} {M : Type u_2} {N : Type u_3} [Group G] [TopologicalSpace G] [CommGroup M] [TopologicalSpace M] [MulDistribMulAction G M] [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (X : ProfiniteGroupExtension G M) (Y : ProfiniteGroupExtension G N) (φ : X.E →ₜ* Y.E) (hright : Y.toGroupExtension.rightHom.comp φ.toMonoidHom = X.toGroupExtension.rightHom) [CompactSpace N] : Continuous ⇑(X.equivariantKernelMap Y φ hright)

The restriction of a continuous homomorphism of profinite extensions to their kernels is continuous when the target kernel is compact.

@[simp]

theorem TauCeti.ProfiniteGroupExtension.contCohomologyClass_map_equivariantKernelMap {G : Type u_1} {M : Type u_2} {N : Type u_3} [Group G] [TopologicalSpace G] [CommGroup M] [TopologicalSpace M] [MulDistribMulAction G M] [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (X : ProfiniteGroupExtension G M) (Y : ProfiniteGroupExtension G N) (φ : X.E →ₜ* Y.E) (hright : Y.toGroupExtension.rightHom.comp φ.toMonoidHom = X.toGroupExtension.rightHom) [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [CompactSpace M] [IsTopologicalGroup N] [ContinuousSMul G N] [CompactSpace N] [TotallyDisconnectedSpace N] : (X.map (X.equivariantKernelMap Y φ hright) ⋯).contCohomologyClass = Y.contCohomologyClass

The kernel restriction of a weak comparison carries the source extension class to the target extension class.

theorem TauCeti.ProfiniteGroupExtension.zmultiples_contCohomologyClass_eq_top_of_comparison {G : Type u_1} {M : Type u_2} {N : Type u_3} [Group G] [TopologicalSpace G] [CommGroup M] [TopologicalSpace M] [MulDistribMulAction G M] [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (X : ProfiniteGroupExtension G M) (Y : ProfiniteGroupExtension G N) (φ : X.E →ₜ* Y.E) (hright : Y.toGroupExtension.rightHom.comp φ.toMonoidHom = X.toGroupExtension.rightHom) [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup M] [ContinuousSMul G M] [CompactSpace M] [IsTopologicalGroup N] [ContinuousSMul G N] [CompactSpace N] [TotallyDisconnectedSpace N] [Finite (ContCohomology.H2 G (Additive M))] (hcard : Nat.card (ContCohomology.H2 G (Additive M)) = Nat.card (ContCohomology.H2 G (Additive N))) (hy : AddSubgroup.zmultiples Y.contCohomologyClass = ⊤) : AddSubgroup.zmultiples X.contCohomologyClass = ⊤

A weak comparison of extensions detects a generating source class when the two second cohomology groups have the same finite order and the target class generates. No surjectivity of the comparison or its restriction to the kernels is assumed.

theorem TauCeti.ProfiniteGroupExtension.exists_surjective_continuousMonoidHom_of_comparison {G : Type u_1} {M : Type u_2} {N : Type u_3} [Group G] [TopologicalSpace G] [CommGroup M] [TopologicalSpace M] [MulDistribMulAction G M] [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (X : ProfiniteGroupExtension G M) (Y : ProfiniteGroupExtension G N) (φ : X.E →ₜ* Y.E) (hright : Y.toGroupExtension.rightHom.comp φ.toMonoidHom = X.toGroupExtension.rightHom) [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup M] [ContinuousSMul G M] [CompactSpace M] [IsTopologicalGroup N] [ContinuousSMul G N] [CompactSpace N] [TotallyDisconnectedSpace N] {p : ℕ} [Fact (Nat.Prime p)] (hN : IsProP p N) (f : M →*[G] N) (hf : Continuous ⇑f) (hs : Function.Surjective ⇑f) (hc : Function.Bijective ⇑(ContCohomology.explicitCoeff2 G (Additive M) f.toAdditive ⋯)) (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 weak comparison and a cohomologically bijective surjection on kernels give a continuous surjection of extensions after a prime-to-p power correction. The weak comparison need not be surjective and need not restrict to the given coefficient map.

The corrected map covers the identity on the quotient and restricts to m ↦ (f m)^n on kernels, with n coprime to p.