Cohomological dimension is invariant under topological group isomorphisms

For an isomorphism of topological groups e : G ≃ₜ* H, the p-cohomological dimensions of G and H agree (TauCeti.cohomologicalDimensionAt_congr), and so do the strict ones (TauCeti.strictCohomologicalDimensionAt_congr). A discrete G-module M becomes one over H by letting h act as e⁻¹ h, and the map Hⁱ(H, M) → Hⁱ(G, M) along e and the identity of M is bijective (map_ofDiscreteModulePair_bijective_of_continuousMulEquiv); so vanishing of Hⁱ(H, M), or of its p-primary component, transfers to Hⁱ(G, M).

This is how the cohomological dimension of an absolute Galois group is read on either of its two models, Mathlib's Field.absoluteGaloisGroup F of an algebraic closure and Tau Ceti's TauCeti.AbsoluteGaloisGroup F of a separable closure, which are isomorphic as topological groups by TauCeti.absoluteGaloisGroupRestrictEquiv.

Main results

• TauCeti.CohomologicalDimensionLE.of_continuousMulEquiv: the vanishing predicate transfers along a topological group isomorphism.
• TauCeti.cohomologicalDimensionAt_le_of_continuousMulEquiv: cd_p G ≤ cd_p H for G ≃ₜ* H.
• TauCeti.cohomologicalDimensionAt_congr: cd_p G = cd_p H for G ≃ₜ* H.
• TauCeti.StrictCohomologicalDimensionLE.of_continuousMulEquiv, TauCeti.strictCohomologicalDimensionAt_le_of_continuousMulEquiv and TauCeti.strictCohomologicalDimensionAt_congr: the same for the strict p-cohomological dimension, scd_p G = scd_p H for G ≃ₜ* H.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §3.

theorem TauCeti.CohomologicalDimensionLE.of_continuousMulEquiv {p : ℕ} {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) {n : ℕ} (h : CohomologicalDimensionLE p H n) : CohomologicalDimensionLE p G n

The vanishing predicate transfers along a topological group isomorphism: for e : G ≃ₜ* H, CohomologicalDimensionLE p H n implies CohomologicalDimensionLE p G n.

theorem TauCeti.cohomologicalDimensionAt_le_of_continuousMulEquiv {p : ℕ} {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : cohomologicalDimensionAt p G ≤ cohomologicalDimensionAt p H

cd_p G ≤ cd_p H for G ≃ₜ* H.

theorem TauCeti.cohomologicalDimensionAt_congr {p : ℕ} {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : cohomologicalDimensionAt p G = cohomologicalDimensionAt p H

The p-cohomological dimension is invariant under topological group isomorphisms: cd_p G = cd_p H for G ≃ₜ* H.

theorem TauCeti.StrictCohomologicalDimensionLE.of_continuousMulEquiv {p : ℕ} {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) {n : ℕ} (h : StrictCohomologicalDimensionLE p H n) : StrictCohomologicalDimensionLE p G n

The strict vanishing predicate transfers along a topological group isomorphism: for e : G ≃ₜ* H, StrictCohomologicalDimensionLE p H n implies StrictCohomologicalDimensionLE p G n.

theorem TauCeti.strictCohomologicalDimensionAt_le_of_continuousMulEquiv {p : ℕ} {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : strictCohomologicalDimensionAt p G ≤ strictCohomologicalDimensionAt p H

scd_p G ≤ scd_p H for G ≃ₜ* H.

theorem TauCeti.strictCohomologicalDimensionAt_congr {p : ℕ} {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : strictCohomologicalDimensionAt p G = strictCohomologicalDimensionAt p H

The strict p-cohomological dimension is invariant under topological group isomorphisms: scd_p G = scd_p H for G ≃ₜ* H.