The explicit and canonical connecting maps agree

A short exact sequence 0 → A → B → C → 0 of discrete modules over a compact group G has two connecting maps in low degrees: the explicit ones TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0 : H⁰(G, C) → H¹(G, A) and explicitDelta1 : H¹(G, C) → H²(G, A), defined on inhomogeneous cochains, and the canonical TauCeti.ContCohomology.DiscreteShortExact.delta, defined in every degree by the snake lemma on Mathlib's homogeneous cochains. This file proves that the comparison isomorphisms explicitH0IsoContinuousCohomology, explicitH1IsoContinuousCohomology and explicitH2IsoContinuousCohomology carry the first to the second in degrees zero and one:

H⁰(G, C) --explicitDelta0--> H¹(G, A)        H¹(G, C) --explicitDelta1--> H²(G, A)
    |                            |                |                            |
    ≅                            ≅                ≅                            ≅
    v                            v                v                            v
H⁰_cont(G, C) ----delta 0--> H¹_cont(G, A)   H¹_cont(G, C) ----delta 1--> H²_cont(G, A)

So a statement about the long exact sequence proved on explicit cocycles, such as the Kummer description of the connecting map, is a statement about the canonical long exact sequence. Conversely, exactness of the canonical sequence at H²(G, C) transports to the explicit model, where no H³ exists: if H³(G, A) vanishes, the explicit coefficient map H²(G, B) → H²(G, C) is surjective.

Main results

• TauCeti.ContCohomology.DiscreteShortExact.explicitIso_delta0: the degree-zero square.
• TauCeti.ContCohomology.DiscreteShortExact.explicitIso_delta1: the degree-one square.
• TauCeti.ContCohomology.DiscreteShortExact.explicitCoeff2_proj_surjective_of_subsingleton: vanishing of H³(G, A) makes the explicit H²(G, B) → H²(G, C) surjective.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), (1.3.2) for the long exact sequence, and Ch. I, §2 for the comparison of inhomogeneous and homogeneous cochains.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitIso_delta0 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) (x : ↥(H0 G C)) : (TopModuleCat.Hom.hom (S.delta 0)) ((CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G C).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G A).hom) ((discreteH1Equiv G A).symm (S.explicitDelta0 x))

The explicit and canonical connecting maps agree in degree zero. Under the comparisons of H⁰ and H¹ with Mathlib's continuous cohomology, the explicit connecting map explicitDelta0 : H⁰(G, C) → H¹(G, A) is the canonical delta 0.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitIso_delta1 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) (x : DiscreteH1 G C) : (TopModuleCat.Hom.hom (S.delta 1)) ((CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G C).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology G A).hom) ((discreteH2Equiv G A).symm (S.explicitDelta1 ((discreteH1Equiv G C) x)))

The explicit and canonical connecting maps agree in degree one. Under the comparisons of H¹ and H² with Mathlib's continuous cohomology, the explicit connecting map explicitDelta1 : H¹(G, C) → H²(G, A) is the canonical delta 1.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitCoeff2_proj_surjective_of_subsingleton {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) [Subsingleton ↑(continuousCohomology 3 (ofDiscreteModule ℤ G A)).toModuleCat] : Function.Surjective ⇑(explicitCoeff2 G B S.projDistribMulActionHom ⋯)

Vanishing of H³(G, A) makes H²(G, B) → H²(G, C) surjective on the explicit second cohomology. The canonical connecting map H²(G, C) → H³(G, A) is zero, so exactness of the canonical long exact sequence at H²(G, C) makes the canonical coefficient map onto, and the degree-two comparison carries it to the explicit coefficient map.