Cohomological dimension of a topological group

For a topological group G, a natural number p and n : ℕ, this file defines the two vanishing predicates behind cohomological dimension, stated against Mathlib's continuous cohomology Hⁱ(G, M) = continuousCohomology i (ofDiscreteModule ℤ G M) of discrete G-modules M with a continuous action:

• CohomologicalDimensionLE p G n: Hⁱ(G, M) = 0 for every i > n and every p-primary torsion M;
• StrictCohomologicalDimensionLE p G n: the p-primary component of Hⁱ(G, M) vanishes for every i > n and every M.

The two differ in both places at once: the ordinary predicate restricts the coefficients and asks the whole group to vanish, the strict one allows all coefficients and asks only the p-primary part to vanish. The p-cohomological dimension cd_p G = cohomologicalDimensionAt p G and the strict one scd_p G = strictCohomologicalDimensionAt p G are the least n in ℕ∞ satisfying them (⊤ when none does), and the cohomological dimension cd G = cohomologicalDimension G is the supremum of cd_p G over the primes p.

The first comparison between them is cd_p G ≤ scd_p G for compact G (NSW (3.3.3)). It rests on isPPrimaryTorsion_continuousCohomology: over a compact group, the continuous cohomology of a discrete p-primary torsion representation is p-primary torsion in every degree. A continuous cochain out of a compact group into a discrete module has finite image, so a single power of p kills it; that bound propagates through the iterated function spaces of the homogeneous cochain complex, and hence to its homology.

For G : Type u the coefficient modules M range over Type (max u v) for an extra universe v: Mathlib's continuous cohomology needs the coefficients in a universe containing that of G, since its resolution is built from C(G, -). Since v does not appear in the arguments, it is the first universe parameter of every definition here and is written explicitly, as in cohomologicalDimensionAt.{v} p G.

The definitions do not use that p is prime; they are meant for prime p, where p-primary is the intended notion.

Main definitions

• TauCeti.CohomologicalDimensionLE, TauCeti.StrictCohomologicalDimensionLE: the vanishing predicates.
• TauCeti.cohomologicalDimensionAt, TauCeti.strictCohomologicalDimensionAt, TauCeti.cohomologicalDimension: the invariants cd_p, scd_p and cd, valued in ℕ∞.

Main results

• TauCeti.isPPrimaryTorsion_continuousCohomology: continuous cohomology of a discrete p-primary torsion representation of a compact group is p-primary torsion.
• TauCeti.cohomologicalDimensionAt_le_iff, TauCeti.strictCohomologicalDimensionAt_le_iff, TauCeti.cohomologicalDimension_le_iff: each invariant is at most n exactly when the corresponding predicate holds at n.
• TauCeti.cohomologicalDimensionAt_eq_zero_iff: cd_p G = 0 exactly when continuous cohomology vanishes in every positive degree for every discrete p-primary torsion G-module.
• TauCeti.cohomologicalDimensionAt_le_strictCohomologicalDimensionAt: cd_p G ≤ scd_p G for compact G.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. III §3, (3.3.1) and (3.3.3).
• J.-P. Serre, Galois Cohomology, Ch. I §3.1.

Torsion of continuous cochains and of continuous cohomology

theorem TauCeti.isPPrimaryTorsion_resolutionX {p : ℕ} {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (X : TopRep k G) [DiscreteTopology ↑X] (h : IsPPrimaryTorsion p ↑X) (n : ℕ) : IsPPrimaryTorsion p ↑(X.resolutionX n)

Every term of the coinduced resolution of a discrete p-primary torsion representation of a compact group is p-primary torsion.

theorem TauCeti.isPPrimaryTorsion_homogeneousCochains {p : ℕ} {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (X : TopRep k G) [DiscreteTopology ↑X] (h : IsPPrimaryTorsion p ↑X) (n : ℕ) : IsPPrimaryTorsion p ↑(X.homogeneousCochains.X n).toModuleCat

Every term of the homogeneous cochain complex of a discrete p-primary torsion representation of a compact group is p-primary torsion.

theorem TauCeti.isPPrimaryTorsion_continuousCohomology {p : ℕ} {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (X : TopRep k G) [DiscreteTopology ↑X] (h : IsPPrimaryTorsion p ↑X) (n : ℕ) : IsPPrimaryTorsion p ↑(continuousCohomology n X).toModuleCat

The continuous cohomology of a discrete p-primary torsion representation of a compact group is p-primary torsion, in every degree.

The vanishing predicates and the invariants

def TauCeti.CohomologicalDimensionLE (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : Prop

CohomologicalDimensionLE p G n says that Hⁱ(G, M) vanishes for every i > n and every discrete p-primary torsion G-module M : Type (max u v) with a continuous action.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.StrictCohomologicalDimensionLE (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : Prop

StrictCohomologicalDimensionLE p G n says that the p-primary component of Hⁱ(G, M) vanishes for every i > n and every discrete G-module M : Type (max u v) with a continuous action.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.cohomologicalDimensionAt (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ∞

The p-cohomological dimension of G, written cd_p G: the least n with CohomologicalDimensionLE p G n, and ⊤ when there is none.

Equations

• TauCeti.cohomologicalDimensionAt p G = TauCeti.leastENatBound (TauCeti.CohomologicalDimensionLE p G)

noncomputable def TauCeti.strictCohomologicalDimensionAt (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ∞

The strict p-cohomological dimension of G, written scd_p G: the least n with StrictCohomologicalDimensionLE p G n, and ⊤ when there is none.

Equations

• TauCeti.strictCohomologicalDimensionAt p G = TauCeti.leastENatBound (TauCeti.StrictCohomologicalDimensionLE p G)

noncomputable def TauCeti.cohomologicalDimension (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ∞

The cohomological dimension of G, written cd G: the supremum over the primes q of the q-cohomological dimension cohomologicalDimensionAt q G.

Equations

• TauCeti.cohomologicalDimension G = ⨆ (q : Nat.Primes), TauCeti.cohomologicalDimensionAt (↑q) G

theorem TauCeti.cohomologicalDimensionLE_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {n : ℕ} : CohomologicalDimensionLE p G n ↔ ∀ (M : Type (max u v)) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M], IsPPrimaryTorsion p M → ∀ (i : ℕ), n < i → Subsingleton ↑(continuousCohomology i (ofDiscreteModule ℤ G M)).toModuleCat

CohomologicalDimensionLE p G n holds exactly when continuous cohomology vanishes above degree n for every discrete p-primary torsion G-module with continuous action.

theorem TauCeti.strictCohomologicalDimensionLE_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {n : ℕ} : StrictCohomologicalDimensionLE p G n ↔ ∀ (M : Type (max u v)) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M] (i : ℕ), n < i → AddCommGroup.primaryComponent (↑(continuousCohomology i (ofDiscreteModule ℤ G M)).toModuleCat) p = ⊥

StrictCohomologicalDimensionLE p G n holds exactly when the p-primary component of continuous cohomology vanishes above degree n for every discrete G-module with continuous action.

theorem TauCeti.CohomologicalDimensionLE.mono {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m n : ℕ} (h : CohomologicalDimensionLE p G m) (hmn : m ≤ n) : CohomologicalDimensionLE p G n

The ordinary vanishing predicate is upward closed in n.

theorem TauCeti.StrictCohomologicalDimensionLE.mono {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m n : ℕ} (h : StrictCohomologicalDimensionLE p G m) (hmn : m ≤ n) : StrictCohomologicalDimensionLE p G n

The strict vanishing predicate is upward closed in n.

@[simp]

theorem TauCeti.cohomologicalDimensionAt_le_iff (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : cohomologicalDimensionAt p G ≤ ↑n ↔ CohomologicalDimensionLE p G n

cohomologicalDimensionAt p G ≤ n exactly when Hⁱ(G, M) vanishes above n for every discrete p-primary torsion M.

@[simp]

theorem TauCeti.cohomologicalDimensionAt_eq_zero_iff (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : cohomologicalDimensionAt p G = 0 ↔ ∀ (M : Type (max u v)) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M], IsPPrimaryTorsion p M → ∀ (i : ℕ), 0 < i → Subsingleton ↑(continuousCohomology i (ofDiscreteModule ℤ G M)).toModuleCat

The first value of p-cohomological dimension. One has cd_p G = 0 exactly when Hⁱ(G, M) vanishes in every positive degree i for every discrete p-primary torsion G-module M with continuous action.

@[simp]

theorem TauCeti.strictCohomologicalDimensionAt_le_iff (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : strictCohomologicalDimensionAt p G ≤ ↑n ↔ StrictCohomologicalDimensionLE p G n

strictCohomologicalDimensionAt p G ≤ n exactly when the p-primary component of Hⁱ(G, M) vanishes above n for every discrete M.

@[simp]

theorem TauCeti.cohomologicalDimensionAt_eq_top_iff (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : cohomologicalDimensionAt p G = ⊤ ↔ ∀ (n : ℕ), ¬CohomologicalDimensionLE p G n

The p-cohomological dimension is infinite exactly when the ordinary vanishing predicate holds at no n.

@[simp]

theorem TauCeti.strictCohomologicalDimensionAt_eq_top_iff (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : strictCohomologicalDimensionAt p G = ⊤ ↔ ∀ (n : ℕ), ¬StrictCohomologicalDimensionLE p G n

The strict p-cohomological dimension is infinite exactly when the strict vanishing predicate holds at no n.

@[simp]

theorem TauCeti.cohomologicalDimension_le_iff (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : cohomologicalDimension G ≤ ↑n ↔ ∀ (q : ℕ), Nat.Prime q → CohomologicalDimensionLE q G n

cohomologicalDimension G ≤ n exactly when CohomologicalDimensionLE q G n holds for every prime q.

theorem TauCeti.cohomologicalDimensionAt_le_cohomologicalDimension (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hp : Nat.Prime p) : cohomologicalDimensionAt p G ≤ cohomologicalDimension G

The p-cohomological dimension is at most the cohomological dimension, for prime p.

theorem TauCeti.StrictCohomologicalDimensionLE.cohomologicalDimensionLE (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {n : ℕ} (h : StrictCohomologicalDimensionLE p G n) : CohomologicalDimensionLE p G n

Over a compact group, the strict vanishing predicate implies the ordinary one at the same n: for p-primary torsion coefficients the cohomology is itself p-primary torsion, so the vanishing of its p-primary component is the vanishing of the whole group.

theorem TauCeti.cohomologicalDimensionAt_le_strictCohomologicalDimensionAt (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : cohomologicalDimensionAt p G ≤ strictCohomologicalDimensionAt p G

cd_p ≤ scd_p (NSW (3.3.3)): over a compact group, the p-cohomological dimension is at most the strict p-cohomological dimension.