The cohomology of a closed subgroup as a colimit over the open subgroups containing it

Let G be a profinite group, X a smooth discrete representation of G (a discrete module with continuous action), and H ≤ G a closed subgroup. Then H is the intersection of the open subgroups V containing it, and the continuous cohomology of H is the filtered colimit of the cohomology of those V:

Hⁿ(H, X) = colim_{H ≤ V open} Hⁿ(V, X).

This file proves that description elementwise, in every degree, on Mathlib's canonical carrier continuousCohomology n:

• surjectivity: every class of Hⁿ(H, X) is the restriction of a class of Hⁿ(V, X) for some open V ⊇ H;
• injectivity: a class of Hⁿ(G, X) restricting to zero on H restricts to zero on some open V ⊇ H. Applied with an open subgroup in place of G, this says that two classes of Hⁿ(V, X) with the same restriction to H agree after restriction to some open V' ⊆ V containing H.

Together they identify Hⁿ(H, X) with the direct limit of the groups Hⁿ(V, X) along the restriction maps resLE, over the open subgroups V ⊇ H ordered by reverse inclusion. In particular any question about a class of Hⁿ(H, X) — whether it vanishes, whether two classes agree — can be settled at some open, hence finite-index, subgroup of G. The results are stated for smooth discrete X, so the action of G on X is required to be continuous.

Main results

• TauCeti.ContinuousCohomology.resolutionMap_subgroupSubtype_eq_zero_iff, TauCeti.ContinuousCohomology.exists_openSubgroup_le_resolutionMap_subgroupSubtype_eq_zero: on the coinduced resolution, restriction to a subgroup vanishes exactly when the cochain vanishes on tuples from the subgroup, and vanishing on a closed subgroup spreads to an open subgroup.
• TauCeti.ContinuousCohomology.resolutionMap_subgroupSubtype_surjective, TauCeti.ContinuousCohomology.exists_mem_invariants_resolutionMap_subgroupSubtype_eq: on the coinduced resolution, restriction to a closed subgroup is surjective in every degree, and in every positive degree also on invariant elements.
• TauCeti.ContinuousCohomology.exists_openSubgroup_le_res_eq_zero: a class restricting to zero on a closed subgroup restricts to zero on an open subgroup containing it.
• TauCeti.ContinuousCohomology.exists_openSubgroup_res_eq_zero: a class of positive degree restricts to zero on some open subgroup.
• TauCeti.ContinuousCohomology.exists_openSubgroup_le_resLE_eq: every class of a closed subgroup is restricted from an open subgroup containing it.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §2.2, Proposition 8.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.1).
• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Section 6.5.

Restriction on the coinduced resolution

The restriction of a homogeneous cochain to a subgroup S is, on the coinduced resolution, ContinuousCohomology.resolutionMap along the inclusion of S with the identity of the coefficients: it reads the iterated map C(G, C(G, …, X)) on tuples from S, so it vanishes exactly when the cochain does (ResolutionVanishesOn).

@[simp]

theorem TauCeti.ContinuousCohomology.resolutionMap_subgroupSubtype_eq_zero_iff {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} (S : Subgroup G) (n : ℕ) (F : ↑(X.resolutionX n)) : (TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.subgroupSubtype S) (CategoryTheory.CategoryStruct.id (TopRep.res S.subtype X)) n)) F = 0 ↔ ResolutionVanishesOn X (↑S) n F

The restriction of an element of the coinduced resolution to a subgroup S is zero exactly when the element vanishes on S.

theorem TauCeti.ContinuousCohomology.exists_openSubgroup_le_resolutionMap_subgroupSubtype_eq_zero {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] [DiscreteTopology ↑X] [TotallyDisconnectedSpace G] {H : Subgroup G} (hH : IsClosed ↑H) {n : ℕ} {F : ↑(X.resolutionX n)} (hF : (TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.subgroupSubtype H) (CategoryTheory.CategoryStruct.id (TopRep.res H.subtype X)) n)) F = 0) : ∃ (V : OpenSubgroup G), H ≤ ↑V ∧ (TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.subgroupSubtype ↑V) (CategoryTheory.CategoryStruct.id (TopRep.res (↑V).subtype X)) n)) F = 0

Vanishing on a closed subgroup spreads to an open subgroup. An element of the coinduced resolution of a discrete representation of a profinite group whose restriction to a closed subgroup H vanishes has vanishing restriction to some open subgroup containing H.

Extension from a closed subgroup

theorem TauCeti.ContinuousCohomology.resolutionMap_subgroupSubtype_surjective {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [CompactSpace G] [DiscreteTopology ↑X] [TotallyDisconnectedSpace G] {H : Subgroup G} (hH : IsClosed ↑H) (n : ℕ) : Function.Surjective ⇑(TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.subgroupSubtype H) (CategoryTheory.CategoryStruct.id (TopRep.res H.subtype X)) n))

Restriction of the coinduced resolution to a closed subgroup is surjective. Over a profinite group, every element of the coinduced resolution of the restriction of a discrete representation to a closed subgroup H is the restriction of an element of the resolution of G.

theorem TauCeti.ContinuousCohomology.exists_mem_invariants_resolutionMap_subgroupSubtype_eq {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] [TotallyDisconnectedSpace G] (hX : IsSmoothDiscrete k X) {H : Subgroup G} (hH : IsClosed ↑H) (n : ℕ) {w : ↑((TopRep.res H.subtype X).resolutionX (n + 1))} (hw : w ∈ ((TopRep.res H.subtype X).resolutionX (n + 1)).ρ.invariants) : ∃ W ∈ (X.resolutionX (n + 1)).ρ.invariants, (TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.subgroupSubtype H) (CategoryTheory.CategoryStruct.id (TopRep.res H.subtype X)) (n + 1))) W = w

An invariant cochain of a closed subgroup extends to an invariant cochain of the group. Over a profinite group and for a smooth discrete representation X, every H-invariant element w of the coinduced resolution, in positive degree n + 1, of the restriction of X to a closed subgroup H is the restriction of a G-invariant element of the resolution of X. In degree zero the resolution is X itself, whose H-invariants need not be G-invariant.

The colimit description

theorem TauCeti.ContinuousCohomology.exists_openSubgroup_le_res_eq_zero {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} (hX : IsSmoothDiscrete k X) {H : Subgroup G} (hH : IsClosed ↑H) {x : ↑(continuousCohomology n X).toModuleCat} (hx : (TopModuleCat.Hom.hom (res H X n)) x = 0) : ∃ (V : OpenSubgroup G), H ≤ ↑V ∧ (TopModuleCat.Hom.hom (res (↑V) X n)) x = 0

A class restricting to zero on a closed subgroup restricts to zero on an open subgroup containing it. For a profinite group G, a smooth discrete representation X and a closed subgroup H, a class of Hⁿ(G, X) whose restriction to H vanishes has vanishing restriction to some open subgroup V ⊇ H. This is the injectivity half of the description of Hⁿ(H, X) as the filtered colimit of the Hⁿ(V, X) over the open subgroups V ⊇ H; applied to an open subgroup in place of G, it says that two classes of Hⁿ(V, X) with the same restriction to H agree after restriction to some open subgroup between H and V.

theorem TauCeti.ContinuousCohomology.exists_openSubgroup_res_eq_zero {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} (hX : IsSmoothDiscrete k X) (x : ↑(continuousCohomology (n + 1) X).toModuleCat) : ∃ (V : OpenSubgroup G), (TopModuleCat.Hom.hom (res (↑V) X (n + 1))) x = 0

Every class of positive degree dies on some open subgroup. For a profinite group G and a smooth discrete representation X, every class of Hⁿ⁺¹(G, X) restricts to zero on some open subgroup of G: it restricts to zero on the closed trivial subgroup, which has no cohomology in positive degrees, hence on an open subgroup containing it.

theorem TauCeti.ContinuousCohomology.exists_openSubgroup_le_resLE_eq {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} (hX : IsSmoothDiscrete k X) {H : Subgroup G} (hH : IsClosed ↑H) (y : ↑(continuousCohomology n (TopRep.res H.subtype X)).toModuleCat) : ∃ (V : OpenSubgroup G) (hHV : H ≤ ↑V) (x : ↑(continuousCohomology n (TopRep.res (↑V).subtype X)).toModuleCat), (TopModuleCat.Hom.hom (resLE hHV X n)) x = y

Every class of a closed subgroup is restricted from an open subgroup containing it. For a profinite group G, a smooth discrete representation X and a closed subgroup H, every class of Hⁿ(H, X) is the restriction of a class of Hⁿ(V, X) for some open subgroup V ⊇ H. This is the surjectivity half of the description of Hⁿ(H, X) as the filtered colimit of the Hⁿ(V, X) over the open subgroups V ⊇ H.