The image of corestriction

Let U be an open subgroup of a profinite group G and M a discrete G-module. Corestriction cor : Hⁿ(U, M) ⟶ Hⁿ(G, M) is the inverse of Shapiro's isomorphism Hⁿ(G, Coind_U^G M) ≅ Hⁿ(U, M) followed by the coefficient map of the trace Coind_U^G M → M. The trace is the surjection of the trace short exact sequence

0 → traceKer G U M → Coind_U^G M → M → 0

(TauCeti.DiscreteCoind.traceShortExact), so its long exact sequence describes the image of corestriction: the sequence

Hⁿ(U, M) --cor--> Hⁿ(G, M) --δ--> Hⁿ⁺¹(G, traceKer G U M)

is exact. A class of Hⁿ(G, M) is therefore a corestriction exactly when its connecting image vanishes. This is the first step of the proof that, for a group of strict cohomological dimension n, corestriction onto the p-primary part of Hⁿ is surjective (NSW (3.3.11)).

Main results

• TauCeti.ContinuousCohomology.exact_corestriction_delta: corestriction followed by the connecting map of the trace short exact sequence is exact.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.4) and the proof of (3.3.11).

theorem TauCeti.ContinuousCohomology.exact_corestriction_delta {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) [U.FiniteIndex] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hU : IsOpen ↑U) (n : ℕ) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom (corestriction U M hU n)) ⇑(CategoryTheory.ConcreteCategory.hom ((DiscreteCoind.traceShortExact G U M hU).delta n))

The image of corestriction is the kernel of the trace connecting map. For an open subgroup U of a profinite group G and a discrete G-module M, the sequence Hⁿ(U, M) ⟶ Hⁿ(G, M) ⟶ Hⁿ⁺¹(G, traceKer G U M) formed by corestriction and the connecting map of the trace short exact sequence 0 → traceKer G U M → Coind_U^G M → M → 0 is exact.