recursive definition of Continuous Cohomology

Stream: mathlib4

[Richard Hill]

I'd like to define continuous group cohomology in the following way. Assume G is a topological group and π is a representation of G on an additive commutative topological group M (or more generally a topological R-module, where R is a commutative ring).

I'll assume that for all g : G, the map π g : M → M is continuous, and for all r : R the map M → M defined by m ↦ r • m is continuous. Under these conditions, we can define a new representation I π of G on the topological group C(G,M) of continuous maps (with the compact open topology), where the action of G is by conjugation. It's easy to check that the representation I π satisfies the same weak continuity conditions as π.

If we let π →ᵢ π' denote the set of continuous intertwining operators from π to another representation π', then there is an intertwining operator const : π →ᵢ C(G,M) which takes m : M to the constant function with value m. Also, for any intertwining operator φ : π →ᵢ π', there is a corresponding intertwining operator map φ : I π →ᵢ I π', which takes a continuous map f : G → M to the continuous map g ↦ φ(f g).

We can use this notation to define a resolution of representation π as the sequence
0 → π →ᵢ I π →ᵢ I (I π) →ᵢ I (I (I π)) →ᵢ ...,
where the map π →ᵢ I π is const and the other maps are:
d₀ = const - map const,
d₁ = const - map d₀
d₂ = const - map d₁, etc.
This kind of recursive definition avoids the the finite alternating sum of maps that appears in most definitions, and this seems to simplify the proofs. For example, it's trivial to prove from the definitions that this sequence is exact, and all of the maps are continuous.

To obtain the continuous group cohomology, we take the invariants, and then take the cohomology of the resulting cochain complex. The definition is very general: it requires only a very weak continuity condition on the representation π, and it avoids the assumption that G is locally compact.

[Kevin Buzzard]

This I guess must specialise to group cohomology when G and M have the discrete topology but I've never seen this approach before. I suppose it doesn't matter at all that our current definition of group cohomology is different. One approach for continuous group cohomology which I've seen is "do group cohomology for finite quotients and then take a filtered colimit" but it wouldn't surprise me if your approach is easier to formalise.

One question this raises is which of the 7 currently available versions of "representation" you want to use.

[Joël Riou]

For a definition of group cohomology, I would rather use a certain subcomplex of continuous cochains in the complex of inhomogeneous cochains defined in https://leanprover-community.github.io/mathlib4_docs/Mathlib/RepresentationTheory/GroupCohomology/Basic.html (this is the definition in the stacks project https://stacks.math.columbia.edu/tag/0DVG): this would ease comparison results in situations which appear in Galois cohomology (like the relation with the colimit of the cohomology of finite quotients mentionned by Kevin).
If there are two nonequivalent definitions which require different assumptions on the group G, the module M and the G-action on M (and how it is bundled...), we should probably implement both...

[Richard Hill]

One approach for continuous group cohomology which I've seen is "do group cohomology for finite quotients and then take a filtered colimit"

This only works if the group is profinite and the module is discrete.

[Richard Hill]

As you say, one can define "continuous cohomology" to mean the same as in https://leanprover-community.github.io/mathlib4_docs/Mathlib/RepresentationTheory/GroupCohomology/Basic.html, but with all the maps continuous. However, there are a few limitations with this.

1. if the action is not continuous in the stronger sense that G \times M \to M is continuous, then the coboundary map will not take continuous maps to continuous maps.
2. The stronger continuity condition is not preserved by continuous induction unless the group G is locally compact.
3. The only proof that I've seen that the spaces C(G^n,M) form a continuously injective resolution is to identify these spaces with C(G,_), i.e. it reduces the problem to my approach (see page 3 of https://deepblue.lib.umich.edu/bitstream/handle/2027.42/46596/222_2005_Article_BF01389727.pdf;sequence=1). This reduction breaks down if G is not locally compact because the two spaces are not the same . There may be some way around this problem; I don't know.

[Richard Hill]

One question this raises is which of the 7 currently available versions of "representation" you want to use.

I don't think this makes a lot of difference (and I don't think I know all seven definitions), but my code uses Representation R G and a type class to keep track of the continuity condition.

[Johan Commelin]

1. This all looks great! I'm excited to see this.
2. Here's a discussion about the (thirty-)seven definitions: #maths > Representation Theory @ 💬

[Johan Commelin]

@Richard Hill It sounds like you have already formalized (almost) all of what you describe above. Is this project publicly available somewhere?

[Richard Hill]

Thanks for your comments. I'm not quite ready with my code, although it's quite close now. I started off working on the case where the coefficient ring R is the integers, and I completed a sorry-free version of this. However I guess people will want a version with a general CommRing R. I also have a few annoying places where lemmas do not work because of the Type synonyms which I'm using, so I'd like to tidy that up.

[Johan Commelin]

Great! Looking forward to the final result!

[Richard Hill]

@Johan Commelin my current sketch is here : https://github.com/rmhi/cts_cohomology/blob/master/CtsCohomology/Basic.lean.
Most of this file is API. The actual definition of the complex of homogeneous cochains is lines 342 to 419 (in the initial commit). At the moment, this is just a functor of the module, but it's not much more work to make it a functor of the group as well. Also, I haven't proved that the resolution is continuously injective, and this needs extra conditions on the representation.

[Johan Commelin]

This sat on my backlog for a week. It's great that you have this. Do you plan on pushing (parts of) it to mathlib?

[Kevin Buzzard]

There is #21300 for starters. But Richard has talked to me about these ideas and I am convinced that they're rather beautiful (he has formalized a bunch of stuff which isn't in PRs and it seems to work fine) but at the back of my mind I am worried that when Amelia said "hey here's how I propose to do group cohomology Joel's response was "actually you should do it a very different way" and Amelia took Joel's advice; I am a bit confused about whether Richard's novel approach to the definitions will be something which Joel won't like.

[Joël Riou]

I am very much ok with Richard approach if the formalization includes a map from his complex to Amelia's, and that it is a quasi-isomorphism when the group and module are discrete.

[Joël Riou]

Otherwise, I agree that the construction is beautiful!

[Richard Hill]

many thanks for all of your comments. I'll start making a few PRs on this.