The explicit low-degree complex of continuous cochains #

Continuous cochain cohomology of a topological group G acting on a topological module M is computed in low degrees by an explicit complex of plain functions carrying continuity as a predicate: C¹ is the additive subgroup of continuous elements of G → M and C² the subgroup of continuous elements of G × G → M. This file builds that complex, its differentials, its cocycles and coboundaries, and the three low-degree cohomology groups

H⁰(G, M) = M^G,   H¹(G, M) = Z¹/B¹,   H²(G, M) = Z²/B².

Main definitions #

TauCeti.ContCohomology.C1, TauCeti.ContCohomology.C2: the continuous cochains.
TauCeti.ContCohomology.d0, d1, d2: the inhomogeneous differentials, as additive homomorphisms of the ambient function groups.
TauCeti.ContCohomology.Z1, Z2: the continuous cocycles, Cⁱ ⊓ ker dⁱ.
TauCeti.ContCohomology.B1, B2: the coboundaries, range d⁰ and the image d¹(C¹) of the continuous 1-cochains.
TauCeti.ContCohomology.H0, H1, H2, their class maps H1pi, H2pi, and the discrete carriers DiscreteH1, DiscreteH2 used by the comparison with canonical cohomology, together with their identifications discreteH1Equiv, discreteH2Equiv with H1 and H2.
TauCeti.ContCohomology.sumCocycle: the additive map sending a finite-group 2-cocycle to the invariant obtained by summing it over its first argument.
TauCeti.ContCohomology.explicitMap0: the compatible-pair pullback on the explicit degree-zero carrier, with TauCeti.ContCohomology.explicitRes0 and explicitCoeff0 its two named instances.

Main statements #

TauCeti.ContCohomology.d1_comp_d0 and TauCeti.ContCohomology.d2_comp_d1: d ∘ d = 0.
TauCeti.ContCohomology.B1_le_Z1 and TauCeti.ContCohomology.B2_le_Z2: the form of d ∘ d = 0 that the two quotients need, coboundaries being continuous.
TauCeti.ContCohomology.subsingleton_H1_of_subsingleton and subsingleton_H2_of_subsingleton: a trivial group has vanishing H¹ and H².
TauCeti.ContCohomology.subsingleton_H1_of_subsingleton_coefficients and subsingleton_H2_of_subsingleton_coefficients: a zero coefficient group has vanishing H¹ and H².
TauCeti.ContCohomology.nsmul_H1_eq_zero and nsmul_H2_eq_zero: H¹(G, M) and H²(G, M) are killed by whatever kills the coefficients M.
TauCeti.ContCohomology.H1EquivOfSmulEqSelf: for a trivial action, H¹(G, M) is the group of continuous homomorphisms G →ₜ* Multiplicative M. This is the statement that makes H¹ of a profinite group computable, and it is false without continuity.

Implementation notes #

The differentials and the cocycle identities follow the conventions of Mathlib's Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean:

(d⁰ m) g       = g • m - m,
(d¹ f) (g, h)  = g • f h - f (g * h) + f g,
(d² f) (g, h, j) = g • f (h, j) - f (g * h, j) + f (g, h * j) - f (g, h).

The cocycle conditions are spelled by Mathlib's unbundled predicates groupCohomology.IsCocycle₁ and groupCohomology.IsCocycle₂, and TauCeti.ContCohomology.d1_apply_eq_zero_iff and d2_apply_eq_zero_iff identify them with the vanishing of the differentials, so that Zⁱ = Cⁱ ⊓ ker dⁱ — which is how Z1 and Z2 are defined, taking their closure under the group operations from AddMonoidHom.ker — is stated in that spelling by mem_Z1_iff and mem_Z2_iff.

Mathlib's bundled groupCohomology.cocycles₁ and cocycles₂ are not reused here: Mathlib's low-degree group cohomology API states them for Rep k G with k and G in a single universe (its binders are {k G : Type u}), and the coefficient modules of a profinite group have to be allowed to live in the group's universe with a small coefficient ring such as ℤ. The unbundled IsCocycle₁/IsCocycle₂ predicates, which Mathlib provides for exactly this purpose, carry no such constraint and are consumed directly. The cochain groups themselves are Mathlib's continuousAddSubgroup.

The trivial-action results are the continuous analogues of Mathlib's groupCohomology.cocycles₁IsoOfIsTrivial, groupCohomology.coboundaries₁_eq_bot_of_isTrivial and groupCohomology.H1IsoOfIsTrivial, in the same order and with the same proof plan; they are restated for the unbundled classes because the Mathlib versions are stated for Rep k G.

Cochains are not normalised. The identities at the unit, f 1 = 0 in degree 1 and f (1, g) = f (1, 1), f (g, 1) = g • f (1, 1) in degree 2, are the lemmas map_one_of_mem_Z1, map_one_fst_of_mem_Z2 and map_one_snd_of_mem_Z2, never definitional conditions.

H1 and H2 divide Z¹ and Z² by the coboundaries viewed inside the cocycles, in the AddSubgroup.addSubgroupOf spelling, so that no proof term enters either quotient subgroup. Each carrier retains the hypotheses of TauCeti.ContCohomology.B1_le_Z1, respectively B2_le_Z2, through that inclusion theorem, so the subgroup divided out is always the whole of B¹, respectively B², and never the intersection B ⊓ Z that addSubgroupOf would cut out at a weaker generality; AddSubgroup.map_addSubgroupOf_eq_of_le turns those inclusions into that identity whenever a consumer needs it spelled out. The two carriers therefore sit in separate sections: H¹ needs G to be a monoid acting continuously, and H² needs a continuous multiplication on G besides, because d¹ has to preserve continuity for B² = d¹(C¹) to consist of cocycles.

References #

J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2: the cohomology of a profinite group computed by the inhomogeneous complex of continuous cochains, which is the complex built here in degrees ≤ 2.