The class of an extension under quotient relabelling

Relabelling the quotient of a profinite extension along a continuous multiplicative equivalence pulls its continuous second cohomology class back along the inverse equivalence. Thus the class generates cohomology before relabelling exactly when it does afterwards. This allows the class of an arithmetic extension to be read over a finite Galois group instead of a quotient of the absolute Galois group.

The comparison uses ContCohomology.explicitMap2Equiv and the section-independent extension class of GroupExtension.contCohomologyClass_eq.

References

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

theorem TauCeti.ProfiniteGroupExtension.contCohomologyClass_relabelQuotient {G H M : Type u} [Group G] [Group H] [CommGroup M] [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace M] [ContinuousMul G] [ContinuousMul H] [IsTopologicalGroup M] [MulDistribMulAction G M] [MulDistribMulAction H M] [ContinuousSMul G M] [ContinuousSMul H M] [CompactSpace M] [T2Space G] [T2Space H] (X : ProfiniteGroupExtension G M) (e : G ≃ₜ* H) (hsmul : ∀ (g : G) (m : M), e g • m = g • m) : (X.relabelQuotient e hsmul).contCohomologyClass = (ContCohomology.explicitMap2 G (Additive M) H (Additive M) (↑e.symm) (AddMonoidHom.id (Additive M)) ⋯ ⋯) X.contCohomologyClass

Relabelling the quotient pulls the extension class back along the inverse quotient equivalence, with the identity on coefficients.

@[simp]

theorem TauCeti.ProfiniteGroupExtension.zmultiples_contCohomologyClass_relabelQuotient_eq_top_iff {G H M : Type u} [Group G] [Group H] [CommGroup M] [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace M] [ContinuousMul G] [ContinuousMul H] [IsTopologicalGroup M] [MulDistribMulAction G M] [MulDistribMulAction H M] [ContinuousSMul G M] [ContinuousSMul H M] [CompactSpace M] [T2Space G] [T2Space H] (X : ProfiniteGroupExtension G M) (e : G ≃ₜ* H) (hsmul : ∀ (g : G) (m : M), e g • m = g • m) : AddSubgroup.zmultiples (X.relabelQuotient e hsmul).contCohomologyClass = ⊤ ↔ AddSubgroup.zmultiples X.contCohomologyClass = ⊤

The extension class generates second cohomology exactly when the class of the extension with relabelled quotient does.