The degree-zero trace/corestriction comparison

The coinduced trace is developed with the rest of the coinduced-module API in TauCeti.RepresentationTheory.Homological.ContCohomology.Coinduced, and on the discrete carrier in TauCeti.RepresentationTheory.Homological.ContCohomology.Coinduced.Discrete. This file proves that in degree zero its composite with the explicit Shapiro isomorphism is exactly the corestriction norm m ↦ ∑ x, t x • m of TauCeti.ContCohomology.explicitCor0: a G-invariant element of Coind_U^G M is the constant function at its value at 1 (TauCeti.ContCohomology.apply_eq_apply_one_of_mem_H0), so the trace of it is the norm of that value.

Main declarations

• TauCeti.ContCohomology.explicitCoeff0_trace_eq_explicitCor0_comp_explicitShapiro0 and TauCeti.ContCohomology.explicitCor0_eq_explicitCoeff0_trace: in degree zero the trace induces the corestriction norm, and corestriction is Shapiro's isomorphism followed by it.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (1.5.7), for the normalization of corestriction.

theorem TauCeti.ContCohomology.explicitCoeff0_trace_eq_explicitCor0_comp_explicitShapiro0 {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] : explicitCoeff0 G (DiscreteCoind G U M) (DiscreteCoind.trace G U M) = (explicitCor0 G M U).comp (explicitShapiro0 G U M).toAddMonoidHom

In degree zero the trace is the corestriction norm. A G-invariant element of Coind_U^G M is constant, so the trace sends it to the norm ∑ x, x • m of the U-invariant value m that Shapiro's isomorphism TauCeti.ContCohomology.explicitShapiro0 reads off it. This is the degree-zero factorization through Shapiro's isomorphism and the trace.

theorem TauCeti.ContCohomology.explicitCor0_eq_explicitCoeff0_trace {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] {U : Subgroup G} [U.FiniteIndex] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] : explicitCor0 G M U = (explicitCoeff0 G (DiscreteCoind G U M) (DiscreteCoind.trace G U M)).comp (explicitShapiro0 G U M).symm.toAddMonoidHom

Degree-zero corestriction factors through Shapiro's isomorphism and the trace. This is TauCeti.ContCohomology.explicitCoeff0_trace_eq_explicitCor0_comp_explicitShapiro0 read through the inverse of the degree-zero Shapiro isomorphism.