Coefficient maps in the explicit-to-algebraic cohomology comparison

For a discrete group, the comparison explicitH2AddEquivGroupCohomology commutes with continuous equivariant coefficient maps. The coefficient modules need not be discrete, and the representation may be over any commutative ring. The comparison therefore transfers an algebraic isomorphism on second cohomology to the explicit continuous coefficient map.

This is useful for maps between compact extension kernels: an algebraic calculation of the cohomology of a relation-module map can be used in the continuous extension-lifting criterion, without replacing that map by an independently chosen isomorphism of cohomology groups. The group and the additive coefficient coordinates may both be changed by the comparison.

Main results

• TauCeti.ContCohomology.explicitH2AddEquivGroupCohomology_explicitCoeff2: the naturality square.
• TauCeti.ContCohomology.explicitCoeff2_bijective_iff: bijectivity is preserved and reflected.
• TauCeti.ContCohomology.explicitCoeff2_bijective_of_isIso: transfer an algebraic isomorphism.

The construction uses the cocycle dictionary in GroupCohomologyIso/Basic.lean and Mathlib's groupCohomology.H2π_comp_map.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §2 and the proof of (7.4.1).

theorem TauCeti.ContCohomology.explicitH2AddEquivGroupCohomology_explicitCoeff2 {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] {M : Type v} {N : Type v'} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] {k H : Type w} [CommRing k] [Group H] {B C : Rep k H} (φ : G ≃* H) (ψ : M ≃+ ↑B) (χ : N ≃+ ↑C) (hψ : ∀ (g : G) (m : M), ψ (g • m) = (B.ρ (φ g)) (ψ m)) (hχ : ∀ (g : G) (n : N), χ (g • n) = (C.ρ (φ g)) (χ n)) (f : M →+[G] N) (hf : Continuous ⇑f) (F : B ⟶ C) (hF : ∀ (m : M), χ (f m) = (Rep.Hom.hom F) (ψ m)) (x : H2 G M) : (explicitH2AddEquivGroupCohomology φ χ hχ) ((explicitCoeff2 G M f hf) x) = (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id H) F 2)) ((explicitH2AddEquivGroupCohomology φ ψ hψ) x)

The explicit-to-algebraic comparison in degree two commutes with a continuous coefficient map, read in any compatible additive coordinates and over any coefficient ring.

theorem TauCeti.ContCohomology.explicitCoeff2_bijective_iff {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] {M : Type v} {N : Type v'} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] {k H : Type w} [CommRing k] [Group H] {B C : Rep k H} (φ : G ≃* H) (ψ : M ≃+ ↑B) (χ : N ≃+ ↑C) (hψ : ∀ (g : G) (m : M), ψ (g • m) = (B.ρ (φ g)) (ψ m)) (hχ : ∀ (g : G) (n : N), χ (g • n) = (C.ρ (φ g)) (χ n)) (f : M →+[G] N) (hf : Continuous ⇑f) (F : B ⟶ C) (hF : ∀ (m : M), χ (f m) = (Rep.Hom.hom F) (ψ m)) : Function.Bijective ⇑(explicitCoeff2 G M f hf) ↔ Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id H) F 2))

An explicit continuous coefficient map is bijective on second cohomology exactly when the same coefficient map in algebraic representation coordinates is bijective.

theorem TauCeti.ContCohomology.explicitCoeff2_bijective_of_isIso {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] {M : Type v} {N : Type v'} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] {k H : Type w} [CommRing k] [Group H] {B C : Rep k H} (φ : G ≃* H) (ψ : M ≃+ ↑B) (χ : N ≃+ ↑C) (hψ : ∀ (g : G) (m : M), ψ (g • m) = (B.ρ (φ g)) (ψ m)) (hχ : ∀ (g : G) (n : N), χ (g • n) = (C.ρ (φ g)) (χ n)) (f : M →+[G] N) (hf : Continuous ⇑f) (F : B ⟶ C) (hF : ∀ (m : M), χ (f m) = (Rep.Hom.hom F) (ψ m)) [CategoryTheory.IsIso (groupCohomology.map (MonoidHom.id H) F 2)] : Function.Bijective ⇑(explicitCoeff2 G M f hf)

An algebraic coefficient map that is an isomorphism on second cohomology gives a bijective explicit continuous coefficient map in compatible coordinates.