The finite-quotient colimit theorem in every degree

Let G be a compact group acting continuously on a discrete module M. In every degree n, the canonical continuous cohomology Hⁿ(G, M) is the colimit of the cohomology groups Hⁿ(G ⧸ U, M^U) of the finite quotients, over the open normal subgroups U of G:

Hⁿ(G, M) = colim_U Hⁿ(G ⧸ U, M^U),

through the inflation-and-inclusion maps. This file proves that the named comparison cocone TauCeti.ContCohomology.continuousFiniteQuotientCocone of TauCeti.ContCohomology.continuousFiniteQuotientSystem is colimiting in TopModuleCat ℤ.

The argument is on Mathlib's homogeneous cochains, the invariant elements of the iterated function spaces C(G, C(G, …, M)), and it is uniform in the degree. The map induced by the comparison pair at U on these function spaces reads a function on G ⧸ U with values in M^U as a function on G with values in M.

• Descent of cochains. Every element F of C(G, C(G, …, M)) comes from the finite level U for every sufficiently small open normal U: a continuous map from the compact group G into a discrete space is uniformly locally constant and has finite image, and each of its finitely many values comes from a finite level by induction on the depth; in depth zero an element of M is fixed by an open normal subgroup. Since the map on function spaces is injective, the descended cochain of an invariant cochain is invariant, and the descended cochain of a cocycle is a cocycle.
• Surjectivity. Hence every cocycle of G is itself inflated from a finite level, with no coboundary subtracted, and every class of Hⁿ(G, M) comes from a finite level (TauCeti.ContCohomology.exists_continuousFiniteQuotientComparisonApp_eq).
• Injectivity. If a finite-level class [z] inflates to a coboundary d b, the primitive b descends to some deeper level V, where it is a primitive of the transition of z (TauCeti.ContCohomology.exists_continuousFiniteQuotientTransition_eq_zero).

Every term of the canonical complex of a compact group with discrete coefficients is discrete, so Hⁿ(G, M) is a discrete topological module and the colimit statement in TopModuleCat ℤ reduces to these two elementwise statements (TauCeti.TopModuleCat.isColimitOfJointlySurjective).

Of the profinite hypotheses only compactness of G is used, together with continuity of the action; total disconnectedness of G is not needed.

Main statements

• TauCeti.ContCohomology.exists_continuousFiniteQuotientComparisonApp_eq: every class of Hⁿ(G, M) is inflated from a finite level.
• TauCeti.ContCohomology.exists_continuousFiniteQuotientTransition_eq_zero: a finite-level class inflating to zero dies at some deeper finite level.
• TauCeti.ContCohomology.continuousFiniteQuotientColimit: the comparison cocone is colimiting.

Implementation notes

The finite-level equalization by taking a difference and the final jointly-surjective colimit argument generalize the degree-two proof in FiniteQuotient/Colimit.lean. The cochain descent argument adapts the all-degree descent on coinduced resolutions in ContCohomology/ClosedSubgroup.lean to quotient maps and fixed-point coefficients.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.2.5).
• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Corollary 6.5.6(a).
• J.-P. Serre, Galois Cohomology, Ch. I, §2.2, Proposition 8.

Cochains through the finite quotients

The cochain maps of the comparison and the transition

Surjectivity and injectivity

theorem TauCeti.ContCohomology.exists_continuousFiniteQuotientComparisonApp_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type u} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [CompactSpace G] [ContinuousSMul G M] {n : ℕ} (x : ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat) : ∃ (U : OpenNormalSubgroup G) (y : ↑(continuousCohomology n (ofDiscreteModule ℤ (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))).toModuleCat), (TopModuleCat.Hom.hom (continuousFiniteQuotientComparisonApp G M U n)) y = x

Every class is inflated from a finite level. For a compact group G and a discrete module M with continuous action, every class of Hⁿ(G, M) is the image, under inflation along G → G ⧸ U followed by the inclusion M^U → M, of a class of Hⁿ(G ⧸ U, M^U) for some open normal subgroup U. This is the surjectivity half of the finite-quotient colimit theorem; a representing cocycle is itself inflated, with no coboundary subtracted.

theorem TauCeti.ContCohomology.exists_continuousFiniteQuotientTransition_eq_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type u} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [CompactSpace G] [ContinuousSMul G M] {n : ℕ} (U : OpenNormalSubgroup G) (y : ↑(continuousCohomology n (ofDiscreteModule ℤ (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))).toModuleCat) (hy : (TopModuleCat.Hom.hom (continuousFiniteQuotientComparisonApp G M U n)) y = 0) : ∃ (V : OpenNormalSubgroup G) (hVU : V ≤ U), (TopModuleCat.Hom.hom (continuousFiniteQuotientTransition G M hVU n)) y = 0

A class inflating to zero dies at a deeper finite level. For a compact group G and a discrete module M with continuous action, a class of Hⁿ(G ⧸ U, M^U) whose image in Hⁿ(G, M) vanishes already vanishes in Hⁿ(G ⧸ V, M^V) for some open normal subgroup V ≤ U. This is the injectivity half of the finite-quotient colimit theorem.

The colimit theorem

noncomputable def TauCeti.ContCohomology.continuousFiniteQuotientColimit (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [CompactSpace G] [ContinuousSMul G M] (n : ℕ) : CategoryTheory.Limits.IsColimit (continuousFiniteQuotientCocone G M n)

The finite-quotient colimit theorem in every degree. For a compact group G and a discrete module M with continuous action, the inflation-and-inclusion cocone exhibits the canonical continuous cohomology Hⁿ(G, M) as the colimit, in TopModuleCat ℤ, of the cohomology groups Hⁿ(G ⧸ U, M^U) of the finite quotients over the open normal subgroups U of G.