Corestriction and the connecting maps of continuous cohomology

Let 0 → A → B → C → 0 be a short exact sequence of discrete G-modules over a profinite group G, and U an open subgroup of finite index. Restricting the sequence to U gives a short exact sequence of discrete U-modules, and corestriction Hⁿ(U, -) ⟶ Hⁿ(G, -) commutes with the connecting maps of the two long exact sequences, in every degree:

Hⁿ(U, C) ---δ---> Hⁿ⁺¹(U, A)
   |                  |
  cor                cor
   v                  v
Hⁿ(G, C) ---δ---> Hⁿ⁺¹(G, A)

This is Neukirch–Schmidt–Wingberg (1.5.2) in every degree; in degrees 0 and 1 it is the explicit statement TauCeti.ContCohomology.DiscreteShortExact.explicitCor_delta0 and explicitCor_delta1 on inhomogeneous cochains.

Corestriction here is the all-degree map of Corestriction/AllDegrees.lean, built through the coinduced module Coind_U^G M and its trace (Brown, Chapter III, §9), and the statement is the counterpart for corestriction of Inflation/ConnectingMap.lean.

Main results

• TauCeti.ContCohomology.DiscreteShortExact.delta_corestriction: corestriction commutes with the connecting map in every degree, as morphisms of TopModuleCat ℤ.
• TauCeti.ContCohomology.DiscreteShortExact.delta_corestriction_apply: the same identity on classes, cor (δ x) = δ (cor x).

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), (1.5.2) and (1.6.4).
• K. S. Brown, Cohomology of Groups, Chapter III, §9, the coinduced-module construction of the transfer.

Corestriction commutes with the connecting maps

theorem TauCeti.ContCohomology.DiscreteShortExact.delta_corestriction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((S.restrict U).delta n) (ContinuousCohomology.corestriction U A hU (n + 1)) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.corestriction U C hU n) (S.delta n)

Corestriction commutes with the connecting map (NSW (1.5.2)) in every degree: for an open finite-index subgroup U of a profinite group G and a short exact sequence S of discrete G-modules, the connecting map of S restricted to U, followed by corestriction, is corestriction followed by the connecting map of S:

Hⁿ(U, C) ---δ---> Hⁿ⁺¹(U, A)
   |                  |
  cor                cor
   v                  v
Hⁿ(G, C) ---δ---> Hⁿ⁺¹(G, A)

The connecting map of U needs U compact, which follows from its openness in the compact group G.

theorem TauCeti.ContCohomology.DiscreteShortExact.delta_corestriction_assoc {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) {Z : TopModuleCat ℤ} (h : continuousCohomology (n + 1) (ofDiscreteModule ℤ G A) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((S.restrict U).delta n) (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.corestriction U A hU (n + 1)) h) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.corestriction U C hU n) (CategoryTheory.CategoryStruct.comp (S.delta n) h)

Corestriction commutes with the connecting map (NSW (1.5.2)) in every degree: for an open finite-index subgroup U of a profinite group G and a short exact sequence S of discrete G-modules, the connecting map of S restricted to U, followed by corestriction, is corestriction followed by the connecting map of S:

Hⁿ(U, C) ---δ---> Hⁿ⁺¹(U, A)
   |                  |
  cor                cor
   v                  v
Hⁿ(G, C) ---δ---> Hⁿ⁺¹(G, A)

The connecting map of U needs U compact, which follows from its openness in the compact group G.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.delta_corestriction_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) (x : ↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) C)).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.corestriction U A hU (n + 1))) ((CategoryTheory.ConcreteCategory.hom ((S.restrict U).delta n)) x) = (CategoryTheory.ConcreteCategory.hom (S.delta n)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.corestriction U C hU n)) x)

cor (δ x) = δ (cor x) for every class x ∈ Hⁿ(U, C) (NSW (1.5.2)): corestriction commutes with the connecting maps in every degree.