Inflation and the inflation-restriction sequence #

Inflation is the third named instance of the compatible-pair pullback on the explicit low-degree complex: for a normal subgroup N of a topological group G it is the pullback along the quotient homomorphism G → G ⧸ N paired with the inclusion M ^ N ↪ M of the invariants, which is equivariant along that homomorphism. This file defines inflation in degrees 0, 1, and 2. In degree one it proves the exactness of

0 → H¹(G ⧸ N, M ^ N) → H¹(G, M) → H¹(N, M)

at its two nodes. In degree two, when H¹(N, M) = 0, it proves that inflation is injective and, for an open normal subgroup N, the exactness of

0 → H²(G ⧸ N, M ^ N) → H²(G, M) → H²(N, M)

at H²(G, M).

Main definitions #

TauCeti.ContCohomology.explicitInfl0, explicitInfl1, and explicitInfl2: inflation on the explicit model in degrees 0, 1, and 2.
TauCeti.ContCohomology.explicitInfl0Equiv: the additive equivalence between degree-zero cohomology before and after inflation.
TauCeti.ContCohomology.descendZ1 and descendZ2: descent of continuous cocycles to G ⧸ N.

Main statements #

TauCeti.ContCohomology.explicitInfl0_injective and explicitInfl0_surjective: inflation in degree zero is bijective.
TauCeti.ContCohomology.explicitRes1_comp_explicitInfl1 and TauCeti.ContCohomology.explicitRes2_comp_explicitInfl2: restricting an inflated class back to N gives zero.
TauCeti.ContCohomology.explicitInfl0_eq_explicitMap0, explicitInfl1_eq_explicitMap1 and explicitInfl2_eq_explicitMap2: inflation in degrees 0, 1 and 2 is the compatible-pair pullback along G → G ⧸ N.
TauCeti.ContCohomology.explicitInfl1_injective: inflation is injective in degree 1.
TauCeti.ContCohomology.explicitInfRes_exact: the image of inflation is exactly the kernel of restriction in degree 1.
TauCeti.ContCohomology.explicitInfl2_injective: inflation is injective in degree 2 when H¹(N, M) = 0, for coefficients of any topology.
TauCeti.ContCohomology.explicitInfRes2_exact: for an open normal subgroup N with H¹(N, M) = 0, the image of inflation is exactly the kernel of restriction in degree 2.
TauCeti.ContCohomology.coe_descendZ1_apply_mk and coe_descendZ2_apply_mk: the descents agree with the original cocycles on quotient representatives.
TauCeti.ContCohomology.explicitInfl1_descendZ1 and explicitInfl2_descendZ2: inflating the descended cocycles returns their original classes.

Implementation notes #

Inflation lives here rather than beside explicitRes1 and explicitCoeff1 in ExplicitFunctoriality.lean because it is the one of the three named instances whose coefficients change — it needs the invariants and their quotient action — and because the exactness statements below are about that same map and belong with it.

The coefficients over the quotient group are Mathlib's FixedPoints.addSubgroup N M, with the G ⧸ N-action and the coercion lemmas supplied by TauCeti/GroupTheory/GroupAction/FixedPoints.lean; no second name for M ^ N is introduced. Continuity of that action is carried as the instance hypothesis [ContinuousSMul (G ⧸ N) (FixedPoints.addSubgroup N M)] rather than deduced from discreteness of M, because nothing below uses discreteness for anything else; TauCeti.continuousSMulQuotientFixedPointsOfContinuousSMul discharges it for a discrete M, which is the case arising in arithmetic applications.

Everything here except TauCeti.ContCohomology.explicitInfRes2_exact holds for an arbitrary topological group G and an arbitrary normal subgroup N; neither profiniteness nor closedness of N is used. Closedness would only make G ⧸ N Hausdorff, and the descent argument in TauCeti.ContCohomology.explicitInfRes_exact needs nothing but the quotient topology: a cochain on G that is constant on the cosets of N descends to a continuous cochain on G ⧸ N precisely because G ⧸ N carries that topology.

The exactness proof is the classical cochain argument. After subtracting the coboundary that trivialises a cocycle on N, the corrected cocycle vanishes on N, hence is constant on the cosets of N and takes its values in M ^ N, so it is the inflation of a continuous 1-cocycle on G ⧸ N. This is the continuous counterpart of Mathlib's discrete groupCohomology.H1InfRes and groupCohomology.H1InfRes_exact, which are stated for Rep k G and so are unavailable at the universe-polymorphic unbundled generality used here.

In degree two, exactness at H²(G, M) says that a class whose restriction to N vanishes is inflated from H²(G ⧸ N, M ^ N). The hypothesis H¹(N, M) = 0 is needed: without it, the kernel of restriction can be strictly larger than the image of inflation. The proof on cochains replaces a cocycle killed by restriction with a cohomologous one vanishing on G × N and on N × G, which then descends to G ⧸ N (TauCeti.ContCohomology.descendZ2). The cohomologous cocycle is built from a choice of coset representatives of N; openness of N makes G ⧸ N discrete, so that this choice, and hence the correction, is continuous. Injectivity in degree two needs no openness: if an inflated cocycle is the coboundary of c, the vanishing of H¹(N, M) corrects c by a coboundary to a cochain constant on the cosets of N with N-fixed values, which descends. For discrete M the weaker hypothesis that the G-invariant part of H¹(N, M) vanishes suffices, through the five-term sequence (TauCeti.ContCohomology.explicitInfl2_injective_of_subsingleton).

References #

J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.7): the inflation-restriction sequence, whose first three terms are the exact sequence proved here, and its extension to degree two when H¹(N, M) vanishes.