Continuous cohomology along an isomorphism of topological groups

For an isomorphism of topological groups e : H ≃ₜ* G and a topological representation X of G, the compatible pair (e, 𝟙) induces an isomorphism

Hⁿ(G, X) ≅ Hⁿ(H, Res_e X),

whose inverse is the compatible pair (e⁻¹, 𝟙): restricting along e and then along e⁻¹ gives back X (TopRep.res_symm_res). This is how a cohomology group computed for one model of a profinite group, such as an open subgroup of an absolute Galois group, is read for another, such as the absolute Galois group of the corresponding finite extension.

Main definitions

• ContinuousMulEquiv.continuousCohomologyIso: the isomorphism Hⁿ(G, X) ≅ Hⁿ(H, Res_e X).

Main results

• ContinuousMulEquiv.continuousCohomologyIso_hom, ContinuousMulEquiv.continuousCohomologyIso_inv: it is the map of the compatible pair (e, 𝟙), with inverse that of (e⁻¹, 𝟙).
• ContinuousMulEquiv.natCard_continuousCohomology_res: the two cohomology groups have the same cardinality.

noncomputable def ContinuousMulEquiv.continuousCohomologyIso {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : H ≃ₜ* G) (X : TopRep R G) (n : ℕ) : continuousCohomology n X ≅ continuousCohomology n (TopRep.res (↑↑e) X)

Continuous cohomology along an isomorphism of topological groups. For e : H ≃ₜ* G, the compatible pair (e, 𝟙) induces Hⁿ(G, X) ≅ Hⁿ(H, Res_e X), with inverse the compatible pair of e⁻¹ and the identity of X.

@[simp]

theorem ContinuousMulEquiv.continuousCohomologyIso_hom {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : H ≃ₜ* G) (X : TopRep R G) (n : ℕ) : (e.continuousCohomologyIso X n).hom = ContinuousCohomology.map (↑e) (CategoryTheory.CategoryStruct.id (TopRep.res (↑↑e) X)) n

continuousCohomologyIso is the map of the compatible pair (e, 𝟙).

@[simp]

theorem ContinuousMulEquiv.continuousCohomologyIso_inv {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : H ≃ₜ* G) (X : TopRep R G) (n : ℕ) : (e.continuousCohomologyIso X n).inv = ContinuousCohomology.map (↑e.symm) (CategoryTheory.eqToHom ⋯) n

The inverse of continuousCohomologyIso is the map of the compatible pair (e⁻¹, 𝟙), the identity being transported along TopRep.res_symm_res.

theorem ContinuousMulEquiv.natCard_continuousCohomology_res {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : H ≃ₜ* G) (X : TopRep R G) (n : ℕ) : Nat.card ↑(continuousCohomology n (TopRep.res (↑↑e) X)).toModuleCat = Nat.card ↑(continuousCohomology n X).toModuleCat

Restriction along an isomorphism of topological groups does not change the cardinality of continuous cohomology.