Corestriction through the coinduced trace in degree one

For an open finite-index subgroup U, the trace on coinduced coefficients induces the same map on first cohomology as Shapiro followed by corestriction. Thus degree-one corestriction can be computed by inverse Shapiro followed by the coefficient map of the trace.

The cochains themselves differ: for a cocycle c : G → DiscreteCoind G U M and a transversal t, their difference is the coboundary of ∑ u, t u • c (t u) (t u)⁻¹. cochainsCor1_shapiro_sub_trace records this identity before passing to classes.

The coinduced construction of corestriction follows Brown, Cohomology of Groups, III §9; the transversal normalization is Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.7).

theorem TauCeti.ContCohomology.cochainsCor1_shapiro_sub_trace {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] {U : Subgroup G} [U.FiniteIndex] [ContinuousMul G] (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) {c : G → DiscreteCoind G U M} (hc : groupCohomology.IsCocycle₁ c) : (((cochainsCor1 G M U t ht) fun (u : ↥U) => (c ↑u) 1) - fun (γ : G) => (DiscreteCoind.trace G U M) (c γ)) = (d0 G M) (∑ u : G ⧸ U, t u • (c (t u)) (t u)⁻¹)

The corestriction of evaluation at 1 differs from the coinduced trace by an explicit 0-coboundary. This identity is valid before imposing continuity on the cocycle.

theorem TauCeti.ContCohomology.explicitCor1_comp_explicitShapiroMap1_eq_explicitCoeff1_trace {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] {U : Subgroup G} [U.FiniteIndex] [IsTopologicalGroup G] [CompactSpace G] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hU : IsOpen ↑U) : (explicitCor1 G M U hU).comp (explicitShapiroMap1 G U M) = explicitCoeff1 G (DiscreteCoind G U M) (DiscreteCoind.trace G U M) ⋯

In degree one, corestriction after the forward Shapiro map is the coefficient map of the coinduced trace.

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

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