The explicit continuous complex of a discrete group is Mathlib's inhomogeneous complex #
For a group G carrying the discrete topology every continuity condition in the explicit
low-degree complex of continuous cochains is vacuous, so that complex is literally Mathlib's
complex of inhomogeneous cochains of the representation Rep.ofDistribMulAction ℤ G M. This file
proves that, degree by degree, and concludes with the three additive isomorphisms
H⁰(G, M) ≃+ H⁰_grp(G, M), H¹(G, M) ≃+ H¹_grp(G, M), H²(G, M) ≃+ H²_grp(G, M).
Main definitions #
TauCeti.ContCohomology.explicitH0IsoGroupCohomology,TauCeti.ContCohomology.explicitH1IsoGroupCohomologyandTauCeti.ContCohomology.explicitH2IsoGroupCohomology: the three comparison isomorphisms.TauCeti.ContCohomology.explicitH1AddEquivGroupCohomologyandTauCeti.ContCohomology.explicitH2AddEquivGroupCohomology: the same comparison for a representationB : Rep k Hover any coefficient ring, along a group isomorphismG ≃* Hand an equivariant additive isomorphismM ≃+ B; the comparisons in degrees1and2are their instances along the identities.TauCeti.ContCohomology.H0AddEquivInvariants,TauCeti.ContCohomology.Z1AddEquivCocycles₁andTauCeti.ContCohomology.Z2AddEquivCocycles₂: the underlying identifications of the numerators, which is where the mathematical content sits; the two isomorphisms in degrees1and2are the induced maps on the subquotients, and in degree0there is no denominator to divide by.
Degree 0 needs no topological hypothesis whatever, and degree 1 needs discreteness only for
the cocycles: B¹ is the image of all of M, so it never sees a continuity condition. It is
degree 2 where discreteness enters the denominator, B² being the image of the continuous
1-cochains.
Main statements #
TauCeti.ContCohomology.C1_eq_topandTauCeti.ContCohomology.C2_eq_top: over a discrete group every cochain is continuous.TauCeti.ContCohomology.d0_apply_eq_d₀₁_hom_applyand its degree-1and degree-2counterparts: the explicit differentials are Mathlib's, on the nose.TauCeti.ContCohomology.mem_cocycles₁_iff_mem_Z1,TauCeti.ContCohomology.mem_coboundaries₁_iff_mem_B1and their degree-2and degree-0counterparts: the dictionary between the two sets of cocycles and coboundaries.
Implementation notes #
The universes are pinned by the pin and not by the mathematics. Mathlib's low-degree
groupCohomology comparison API forces the group and coefficient module into Type 0 when the
coefficient ring is ℤ. Thus the three final comparison isomorphisms carry G M : Type, while the
differentials, membership dictionaries, and numerator equivalences keep every universe not
constrained by Mathlib's representation API arbitrary. C1_eq_top and C2_eq_top mention nothing
of Mathlib's theory and are fully polymorphic, and so are G and M in the comparisons along a
compatible pair, where only k and H share a universe. When the pin drops these restrictions the
binders here can simply be widened.
The isomorphisms are built as AddEquivs and not as isomorphisms in ModuleCat ℤ. The explicit
H¹ and H² are bare additive groups by construction, their inherited quotient topology being the
wrong one; TauCeti.ContCohomology.DiscreteH1 and DiscreteH2 are the carriers used when a
topology is wanted, and the comparison with the canonical continuous cohomology is where that
choice matters. Against groupCohomology there is no topology on either side, so an additive
isomorphism is the whole statement.
Rep.ofDistribMulAction ℤ G M is Mathlib's translation of an unbundled DistribMulAction into
Rep ℤ G; the ℤ-linearity of the comparison is automatic and is not restated, because the
explicit complex is a complex of additive groups. Mathlib's cocyclesOfIsCocycle₁,
isCocycle₁_of_mem_cocycles₁ and their siblings prove the same dictionary as the four membership
lemmas here, but they are stated for {k G A : Type u} — all three in one universe — so they are
not reused; the proofs below go through groupCohomology.mem_cocycles₁_iff and
mem_cocycles₂_iff, which carry no such constraint.
This implements the "continuous against discrete" milestone of Layer 3 of the human-authored
roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md, whose Suggested.lean fixes the names
explicitH0IsoGroupCohomology, explicitH1IsoGroupCohomology and explicitH2IsoGroupCohomology.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2: the cohomology of a profinite group is computed by the complex of continuous cochains, which for a discrete group is the abstract inhomogeneous complex.
The explicit degree-0 differential is Mathlib's d₀₁.
The explicit degree-1 differential is Mathlib's d₁₂.
The explicit degree-2 differential is Mathlib's d₂₃.
Degree 0: the invariants of the induced representation are the explicit H⁰ = M^G.
Degree 1, cocycles: over a discrete group the continuity half of Z¹ is free, so the
continuous 1-cocycles are Mathlib's 1-cocycles.
Degree 1, coboundaries: B¹ carries no continuity condition on its primitive, so the two
definitions agree over any topological group; discreteness is not used.
Degree 2, cocycles: as in degree 1, over a discrete group the continuity half of Z² is
free, G × G being discrete as well.
Degree 2, coboundaries. Here discreteness is used: B² is by definition the image of the
continuous 1-cochains, and over a discrete group those are all of them.
Degree 0 is the one degree where the comparison needs no hypothesis on the topology at all:
both sides are the invariants, and continuity constrains no 0-cochain.
Degree 0, on the carriers: the explicit H⁰(G, M) = M^G is the submodule of invariants of
the induced representation.
Instances For
H0AddEquivInvariants is the identity on underlying elements.
The inverse of H0AddEquivInvariants is the identity on underlying elements.
Layer 3, degree 0 against Mathlib's discrete group cohomology. The explicit H⁰(G, M) is
Mathlib's H⁰ of the representation attached to the action.
Instances For
explicitH0IsoGroupCohomology is H0AddEquivInvariants followed by the inverse of Mathlib's
groupCohomology.H0Iso.
The inverse of explicitH0IsoGroupCohomology is Mathlib's groupCohomology.H0Iso followed by
the inverse of H0AddEquivInvariants.
Along a compatible pair, over any coefficient ring #
A module met in practice is usually a representation B : Rep k H over a larger coefficient ring
k, of a group H that is only isomorphic to G, on a carrier that is only isomorphic to M.
Along a group isomorphism φ : G ≃* H and an additive isomorphism ψ : M ≃+ B intertwining the two
actions, the explicit H¹ and H² of M are those of B. The coefficient ring plays no role: a
cocycle of B over k is the same function as a cocycle of its underlying additive group.
Mathlib's groupCohomology.mapIso transports along a group isomorphism and a k-linear
isomorphism of representations over one coefficient ring; here M is only an additive group, so
the comparison is built on cocycles directly. The identities φ = .refl G, ψ = .refl M give
explicitH1IsoGroupCohomology and explicitH2IsoGroupCohomology below.
Explicit H¹ against groupCohomology along a compatible pair. For a discrete group G,
a group isomorphism φ : G ≃* H and an additive isomorphism ψ : M ≃+ B onto a
k-representation of H intertwining the actions, the explicit H¹(G, M) is H¹(H, B). The
class of a cocycle z goes to the class of h ↦ ψ (z (φ⁻¹ h)).
Instances For
explicitH1AddEquivGroupCohomology sends the class of a continuous 1-cocycle z to the
class of the cocycle h ↦ ψ (z (φ⁻¹ h)).
Transport along an action-compatible group and additive equivalence preserves the
2-cocycle condition.
Explicit H² against groupCohomology along a compatible pair. For a discrete group G,
a group isomorphism φ : G ≃* H and an additive isomorphism ψ : M ≃+ B onto a
k-representation of H intertwining the actions, the explicit H²(G, M) is H²(H, B). The
class of a cocycle z goes to the class of (h, h') ↦ ψ (z (φ⁻¹ h, φ⁻¹ h')).
Instances For
explicitH2AddEquivGroupCohomology sends the class of a continuous 2-cocycle z to the
class of the cocycle (h, h') ↦ ψ (z (φ⁻¹ h, φ⁻¹ h')).
The explicit-to-abstract comparison in degree two commutes with restriction to corresponding subgroups along the group isomorphism.
Degree 1, on the numerators: the continuous 1-cocycles are Mathlib's 1-cocycles.
Instances For
Z1AddEquivCocycles₁ does not change the underlying function G → M of a cocycle.
The inverse of Z1AddEquivCocycles₁ does not change the underlying function G → M of a
cocycle.
Layer 3, degree 1 against Mathlib's discrete group cohomology. Every continuity condition
is vacuous for a discrete group, so this identifies subquotients of the same function space.
Layer 4 uses it at every finite level. It is explicitH1AddEquivGroupCohomology along the
identities.
Instances For
explicitH1IsoGroupCohomology sends the class of a continuous 1-cocycle z to the class of
z in Mathlib's H¹.
The inverse of explicitH1IsoGroupCohomology sends the class of a 1-cocycle c in Mathlib's
H¹ to the class of c in the explicit H¹.
Degree 2, on the numerators: the continuous 2-cocycles are Mathlib's 2-cocycles.
Instances For
Z2AddEquivCocycles₂ does not change the underlying function G × G → M of a cocycle.
The inverse of Z2AddEquivCocycles₂ does not change the underlying function G × G → M of a
cocycle.
Layer 3, degree 2 against Mathlib's discrete group cohomology. The denominator is where
discreteness is used twice over: B² is the image of the continuous 1-cochains, and over a
discrete group those exhaust G → M. It is explicitH2AddEquivGroupCohomology along the
identities.
Instances For
The canonical degree-two comparison is the compatible-pair comparison in identity group and coefficient coordinates.
explicitH2IsoGroupCohomology sends the class of a continuous 2-cocycle z to the class of
z in Mathlib's H².
The inverse of explicitH2IsoGroupCohomology sends the class of a 2-cocycle c in Mathlib's
H² to the class of c in the explicit H².