The p-cohomological dimension of a profinite group is that of a Sylow subgroup

Let G be a profinite group, p a prime and P a Sylow pro-p subgroup of G. Then cd_p G = cd_p P (Serre, Galois Cohomology, I §3.3, Cor. 1 to Prop. 14; NSW (3.3.6)). This is a special case of TauCeti.cohomologicalDimensionAt_eq_of_isClosed_of_forall_not_dvd_index, which combines the following two inequalities.

• cd_p G ≤ cd_p P: every open subgroup of G containing P has index prime to p (TauCeti.IsProPSylow.not_dvd_index_of_le), so restriction from G to P is injective on the cohomology of every discrete p-primary torsion G-module in every positive degree, and a vanishing statement for P transfers to G.
• cd_p P ≤ cd_p G: P is closed, and the p-cohomological dimension is monotone in a closed subgroup by Shapiro's lemma (TauCeti.cohomologicalDimensionAt_le_of_isClosed).

In particular all Sylow pro-p subgroups of G have the same p-cohomological dimension, and the computation of cd_p for an arbitrary profinite group reduces to that of a pro-p group.

Main results

• TauCeti.IsProPSylow.res_injective: restriction Hⁿ(G, X) → Hⁿ(P, X) to a Sylow pro-p subgroup P is injective in every degree, for a smooth discrete p-primary torsion representation X of G.
• TauCeti.CohomologicalDimensionLE.of_isProPSylow: the vanishing predicate cd_p P ≤ n for a Sylow pro-p subgroup P implies cd_p G ≤ n.
• TauCeti.IsProPSylow.cohomologicalDimensionAt_le: cd_p G ≤ cd_p P for a Sylow pro-p subgroup P of a profinite group G.
• TauCeti.IsProPSylow.cohomologicalDimensionLE_iff: the vanishing predicates cd_p G ≤ n and cd_p P ≤ n are equivalent for a Sylow pro-p subgroup P.
• TauCeti.IsProPSylow.cohomologicalDimensionAt_eq: cd_p G = cd_p P for a Sylow pro-p subgroup P of a profinite group G.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §3.3, Cor. 1 to Prop. 14.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.10) and (3.3.6).

theorem TauCeti.IsProPSylow.res_injective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} (hP : IsProPSylow p P) {k : Type w} [Ring k] [TopologicalSpace k] {X : TopRep k G} (hX : IsSmoothDiscrete k X) (hX' : IsAddPGroup p ↑X) (n : ℕ) : Function.Injective ⇑(TopModuleCat.Hom.hom (ContinuousCohomology.res P X n))

Restriction to a Sylow pro-p subgroup is injective (NSW (1.6.10)): for a Sylow pro-p subgroup P of a profinite group G and a smooth discrete p-primary torsion representation X of G, restriction Hⁿ(G, X) → Hⁿ(P, X) is injective in every degree n.

theorem TauCeti.CohomologicalDimensionLE.of_isProPSylow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} (hP : IsProPSylow p P) {n : ℕ} (h : CohomologicalDimensionLE p (↥P) n) : CohomologicalDimensionLE p G n

cd_p G ≤ cd_p P for a Sylow pro-p subgroup P, as the vanishing predicate: for a Sylow pro-p subgroup P of a profinite group G, CohomologicalDimensionLE p P n implies CohomologicalDimensionLE p G n.

theorem TauCeti.IsProPSylow.cohomologicalDimensionAt_le {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} (hP : IsProPSylow p P) : cohomologicalDimensionAt p G ≤ cohomologicalDimensionAt p ↥P

cd_p G ≤ cd_p P for a Sylow pro-p subgroup P of a profinite group G (Serre, Galois Cohomology, I §3.3, Cor. 1 to Prop. 14): the p-cohomological dimension of G is at most that of any of its Sylow pro-p subgroups.

theorem TauCeti.IsProPSylow.cohomologicalDimensionLE_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} (hP : IsProPSylow p P) {n : ℕ} : CohomologicalDimensionLE p G n ↔ CohomologicalDimensionLE p (↥P) n

cd_p G = cd_p P for a Sylow pro-p subgroup P, as the vanishing predicate: for a Sylow pro-p subgroup P of a profinite group G, CohomologicalDimensionLE p G n holds if and only if CohomologicalDimensionLE p P n does.

theorem TauCeti.IsProPSylow.cohomologicalDimensionAt_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} (hP : IsProPSylow p P) : cohomologicalDimensionAt p G = cohomologicalDimensionAt p ↥P

cd_p G = cd_p P for a Sylow pro-p subgroup P of a profinite group G (Serre, Galois Cohomology, I §3.3, Cor. 1 to Prop. 14; NSW (3.3.6)): the p-cohomological dimension of a profinite group is that of any of its Sylow pro-p subgroups.