Coefficient naturality of degree-two corestriction

For an open finite-index subgroup U of a topological group G, degree-two corestriction commutes with every continuous G-equivariant additive coefficient map. This lets coefficient identifications and changes of coefficients pass through the explicit transversal construction, including when the coefficients are topological rather than discrete.

explicitCor2Transversal_explicitMap2_id gives the identity for any transversal; explicitCor2_explicitMap2_id gives it for the canonical corestriction. Together with map_explicitCor0 and explicitCor1_explicitMap1_id in Corestriction.Basic, this supplies coefficient naturality in all three explicit degrees.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §5, for corestriction and its functoriality.

theorem TauCeti.ContCohomology.explicitCor2Transversal_explicitMap2_id (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (U : Subgroup G) [U.FiniteIndex] {N : Type w} [AddCommGroup N] [DistribMulAction G N] [TopologicalSpace N] [IsTopologicalAddGroup N] [ContinuousSMul G N] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (hU : IsOpen ↑U) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (g : G) (m : M), f (g • m) = g • f m) (x : H2 (↥U) M) : (explicitCor2Transversal G N U t ht hU) ((explicitMap2 (↥U) M (↥U) N (ContinuousMonoidHom.id ↥U) f hf ⋯) x) = (explicitMap2 G M G N (ContinuousMonoidHom.id G) f hf ⋯) ((explicitCor2Transversal G M U t ht hU) x)

Degree-two corestriction for any transversal commutes with a continuous equivariant coefficient map. No continuity of the transversal or discreteness of the coefficients is needed.

theorem TauCeti.ContCohomology.explicitCor2_explicitMap2_id (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] (U : Subgroup G) [U.FiniteIndex] {N : Type w} [AddCommGroup N] [DistribMulAction G N] [TopologicalSpace N] [IsTopologicalAddGroup N] [ContinuousSMul G N] (hU : IsOpen ↑U) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (g : G) (m : M), f (g • m) = g • f m) (x : H2 (↥U) M) : (explicitCor2 G N U hU) ((explicitMap2 (↥U) M (↥U) N (ContinuousMonoidHom.id ↥U) f hf ⋯) x) = (explicitMap2 G M G N (ContinuousMonoidHom.id G) f hf ⋯) ((explicitCor2 G M U hU) x)

Degree-two corestriction commutes with continuous equivariant coefficient maps, completing coefficient naturality for the explicit low-degree cohomology groups.