Corestriction in the top degree of strict cohomological dimension

Let G be a profinite group with scd_p G ≤ n and U an open subgroup. Then every p-primary class of Hⁿ(G, M) is the corestriction of a p-primary class of Hⁿ(U, M), for every discrete G-module M (the surjectivity half of NSW (3.3.11)). In the class-module theorem for groups of strict cohomological dimension two, this is what makes the transfer G^ab(p) → U^ab(p) injective.

For U normal, corestriction is moreover injective on the p-primary part of the coinvariants of G ⧸ U (the injectivity half of NSW (3.3.11)): a p-primary class of Hⁿ(U, M) whose corestriction vanishes lies in the subgroup generated by the differences (g)_* w - w of p-primary classes w, where (g)_* is the conjugation TauCeti.ContinuousCohomology.conjNormalMap. NSW state (3.3.11) as an isomorphism Hⁿ(U, M)(p)_{G ⧸ U} ≅ Hⁿ(G, M)(p) induced by corestriction; its injectivity half is stated here as this description of the kernel, which avoids forming the coinvariants. Both halves hold in every degree n, including n = 0, and only need n to bound the strict cohomological dimension at p.

Main results

• TauCeti.StrictCohomologicalDimensionLE.corestriction_surjOn_primaryComponent: under StrictCohomologicalDimensionLE p G n, corestriction maps the p-primary component of Hⁿ(U, M) onto that of Hⁿ(G, M).
• TauCeti.corestriction_surjOn_primaryComponent_of_strictCohomologicalDimensionAt_le: the same statement under scd_p G ≤ n.
• TauCeti.StrictCohomologicalDimensionLE.corestriction_ker_primaryComponent: under StrictCohomologicalDimensionLE p G n and for U normal, a p-primary class of Hⁿ(U, M) with trivial corestriction lies in the subgroup generated by the (g)_* w - w.
• TauCeti.corestriction_ker_primaryComponent_of_strictCohomologicalDimensionAt_le: the same statement under scd_p G ≤ n.

References

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

theorem TauCeti.StrictCohomologicalDimensionLE.corestriction_surjOn_primaryComponent {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U : Subgroup G} [U.FiniteIndex] (hp : Nat.Prime p) {n : ℕ} (h : StrictCohomologicalDimensionLE p G n) (hU : IsOpen ↑U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] : Set.SurjOn ⇑(CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.corestriction U M hU n)) ↑(AddCommGroup.primaryComponent (↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) M)).toModuleCat) p) ↑(AddCommGroup.primaryComponent (↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat) p)

Corestriction in the top degree of strict cohomological dimension (NSW (3.3.11), surjectivity). For a profinite group G with StrictCohomologicalDimensionLE p G n, a prime p and an open subgroup U, every p-primary class of Hⁿ(G, M) is the corestriction of a p-primary class of Hⁿ(U, M), for every discrete G-module M.

theorem TauCeti.corestriction_surjOn_primaryComponent_of_strictCohomologicalDimensionAt_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U : Subgroup G} [U.FiniteIndex] (hp : Nat.Prime p) {n : ℕ} (h : strictCohomologicalDimensionAt p G ≤ ↑n) (hU : IsOpen ↑U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] : Set.SurjOn ⇑(CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.corestriction U M hU n)) ↑(AddCommGroup.primaryComponent (↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) M)).toModuleCat) p) ↑(AddCommGroup.primaryComponent (↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat) p)

Corestriction in the top degree of strict cohomological dimension (NSW (3.3.11), surjectivity), stated through scd_p G ≤ n: for an open subgroup U of a profinite group G, corestriction maps the p-primary component of Hⁿ(U, M) onto that of Hⁿ(G, M).

Injectivity on the coinvariants

theorem TauCeti.StrictCohomologicalDimensionLE.corestriction_ker_primaryComponent {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U : Subgroup G} [U.FiniteIndex] [U.Normal] (hp : Nat.Prime p) {n : ℕ} (h : StrictCohomologicalDimensionLE p G n) (hU : IsOpen ↑U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] {y : ↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) M)).toModuleCat} (hy : y ∈ AddCommGroup.primaryComponent (↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) M)).toModuleCat) p) (hcor : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.corestriction U M hU n)) y = 0) : y ∈ AddSubgroup.closure {z : (fun (X : TopModuleCat ℤ) => ↑X.toModuleCat) (continuousCohomology n (ofDiscreteModule ℤ (↥U) M)) | ∃ (g : G), ∃ w ∈ AddCommGroup.primaryComponent (↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) M)).toModuleCat) p, z = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.conjNormalMap U M g n)) w - w}

Corestriction in the top degree of strict cohomological dimension is injective on the coinvariants (NSW (3.3.11), injectivity). For a profinite group G with StrictCohomologicalDimensionLE p G n, a prime p and an open normal subgroup U, a p-primary class of Hⁿ(U, M) whose corestriction to Hⁿ(G, M) vanishes lies in the subgroup generated by the differences (g)_* w - w of p-primary classes w ∈ Hⁿ(U, M), for every discrete G-module M.

theorem TauCeti.corestriction_ker_primaryComponent_of_strictCohomologicalDimensionAt_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U : Subgroup G} [U.FiniteIndex] [U.Normal] (hp : Nat.Prime p) {n : ℕ} (h : strictCohomologicalDimensionAt p G ≤ ↑n) (hU : IsOpen ↑U) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] {y : ↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) M)).toModuleCat} (hy : y ∈ AddCommGroup.primaryComponent (↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) M)).toModuleCat) p) (hcor : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.corestriction U M hU n)) y = 0) : y ∈ AddSubgroup.closure {z : (fun (X : TopModuleCat ℤ) => ↑X.toModuleCat) (continuousCohomology n (ofDiscreteModule ℤ (↥U) M)) | ∃ (g : G), ∃ w ∈ AddCommGroup.primaryComponent (↑(continuousCohomology n (ofDiscreteModule ℤ (↥U) M)).toModuleCat) p, z = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.conjNormalMap U M g n)) w - w}

Corestriction in the top degree of strict cohomological dimension is injective on the coinvariants (NSW (3.3.11), injectivity), stated through scd_p G ≤ n: for an open normal subgroup U of a profinite group G, a p-primary class of Hⁿ(U, M) with trivial corestriction lies in the subgroup generated by the differences (g)_* w - w of p-primary classes.