Corestriction through the coinduced trace in degree two

For an open subgroup U of a profinite group G, the trace Coind_U^G M → M induces the same map on second cohomology as Shapiro's isomorphism followed by corestriction. Thus degree-two corestriction TauCeti.ContCohomology.explicitCor2 can be computed by inverse Shapiro followed by the coefficient map of the trace, exactly as in degrees zero and one.

Unlike degree one, no coboundary appears once the transversal is adapted to the inverse Shapiro cochain. The inverse Shapiro cochain TauCeti.ContCohomology.coindCochain2 of a 2-cochain c of U is built from a right-coset factorization w : G → U, and its value at (γ, η) is the function y ↦ homogeneous2 c (w y) (w (y γ)) (w (y γ η)). For the adapted transversal t = TauCeti.factorizationTransversal w, with w (t x)⁻¹ = 1 for every coset x, the factorization sends (t x)⁻¹ γ to the transversal word ℓᵗ_x(γ), so the trace of that value is the degree-two corestriction cochain ∑ x, t x • c (ℓᵗ_x γ, ℓᵗ_{γ⁻¹ • x} η) on the nose. The general statement then follows from the independence of explicitCor2 of the transversal.

Main declarations

• TauCeti.ContCohomology.trace_coindCochain2: the trace of the inverse Shapiro cochain is the corestriction cochain for the transversal adapted to the factorization.
• TauCeti.ContCohomology.explicitCor2_eq_explicitCoeff2_trace: degree-two corestriction is inverse Shapiro followed by the coefficient map of the trace.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §9, for the coinduced construction of the transfer.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.7), for the transversal normalization of corestriction.

theorem TauCeti.ContCohomology.trace_coindCochain2 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U : Subgroup G} [U.FiniteIndex] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (w : G → ↥U) (hw : Continuous w) (hwmul : ∀ (u : ↥U) (g : G), w (↑u * g) = u * w g) {c : ↥U × ↥U → M} (hc : Continuous c) (γ η : G) : (DiscreteCoind.trace G U M) (coindCochain2 w c hw hwmul hc (γ, η)) = (cochainsCor2 G M U (factorizationTransversal w) ⋯) c (γ, η)

The trace of the inverse Shapiro cochain is the corestriction cochain. For the transversal adapted to the factorization w, the trace Coind_U^G M → M of the inverse Shapiro 2-cochain of c is, at every pair (γ, η), the degree-two corestriction cochain of c. No cocycle condition on c is needed.

theorem TauCeti.ContCohomology.explicitCor2_eq_explicitCoeff2_trace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U : Subgroup G} [U.FiniteIndex] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) : explicitCor2 G M U hU = (explicitCoeff2 G (DiscreteCoind G U M) (DiscreteCoind.trace G U M) ⋯).comp (explicitShapiro2 G U M ⋯).symm.toAddMonoidHom

Degree-two corestriction is inverse Shapiro followed by the coefficient map of the trace. The subgroup is open, and the Shapiro isomorphism uses its resulting closedness.