Group cohomology

Stream: maths

[Kevin Buzzard]

I thought I'd test out the new API we have for homological algebra, by doing a test case: building a model for group cohomology. There are competing topologists who I believe want to build a totally different model involving these exotic $K(G,1)$ spaces or whatever they're called, but my version with homogeneous cocycles and coboundaries is on the group-cohomology branch of mathlib and I just proved $d^2=0$.

People have said various things to me in DMs about how building a model via cocycles is somehow "not the right thing to do" for some reason. However I have, in a sense, written down an explicit implementation of a projective resolution for $\Z[G]$, and used it to calculate $Ext^i(\Z[G],M):=H^i(G,M)$.

Given that I have proved that $d^2=0$ I would like to claim my free "short-exact-sequence-implies-long-exact-sequence" and "Hochschild-Serre spectral sequence" theorems, or at least the "Inf-res" long exact sequence for group cohomology in low degree. What API do you category people require? @Ken Lee ?

[Scott Morrison]

I haven't looked at this yet, but can you show that you've produced a projective resolution in the sense of #7486? This might be a good fit test.

[Scott Morrison]

@[ext] structure cochain_succ :=
(to_fun : (fin n → G) → M)
(smul_apply' : ∀ (s : G) (g : fin n → G), s • to_fun g = to_fun (λ i, s * g i))

I guess we don't have a type for bundled distrib_mul_action-compatible maps.

[Scott Morrison]

Maybe it's better to quickly develop that, i.e. just replacing fin n → G with some arbitrary distrib_mul_action G N. Presumably everything up to line 148 holds in that setting.

[Scott Morrison]

The point of #7486 (projective resolutions) #7487 (derived functors) and #7525 (Ext) is to provide you with a single "chosen" left_derived n F, for each functor F, and also to provide the API so you can bring your own favourite resolution, and know that (left_derived n F).obj X is isomorphic to the n-th homology of F applied to that resolution.

[Scott Morrison]

I think the DMs saying building the model via cocycles is not the right thing to do (not from me) are just pointing out that your calculation of d^2 = 0 here can likely be factored without much additional work into constructing a simplicial object, and then computing the alternating face complex of that simplicial object --- but that second piece of work only ever needs to be done once (and has been done in LTE).

[Scott Morrison]

But I haven't actually tried building the relevant simplicial object here, so I can't really promise that you get a reduction in work by using the alternately face complex.

[Scott Morrison]

I would hope that you can even get something that is pretty close to definitionally equal to what you've done!

[Scott Morrison]

Oh, sorry, scratch those last three comments. Maybe they only apply with the usual model of group cohomology. Maybe there's some augmentation trick, I'm not sure, to fit the homogeneous model into this picture, I'd have to think about it.

[Adam Topaz]

I'm fairly sure the homogeneous cochain complex is defeq to the alternating face map cochain complex associated to such a cosimplicial object, and furthermore this cosimplicial object can be built from K(pi,1) as a simplicial set (not a topological space! It's just the combinatorics that encapsulate the usual differential). I certainly wasn't suggesting constructing anything via any actual topological spaces :fear:

[Adam Topaz]

I don't know if the simplicial construction of this might be helpful nlab#group+cohomology

[Adam Topaz]

Looks like this describes modules with the trivial action, but I'm sure the general construction is written down somewhere...

[Kevin Buzzard]

Do we have this?

def finsupp.equiv_congr {α β M : Type*} [has_zero M] (e : α ≃ β) : (β →₀ M) ≃ (α →₀ M) :=
sorry
-- by rw e

I'm making the projective resolution using finsupp.

[Kevin Buzzard]

If you use map_domain you need M to be (unnecessarily) an add_comm_monoid and if you use comap_domain you end up noncomputable.

[Mario Carneiro]

I think you want to use emb_domain instead

[Mario Carneiro]

actually that one is noncomputable too

[Mario Carneiro]

yeah I guess the computable version only works with an equiv, since the support maps and the function comaps

[Mario Carneiro]

#7755

[Eric Wieser]

We have docs#distrib_mul_action_hom - isn't that the bundled type you ask for above?

[Ken Lee]

Scott Morrison said:

The point of #7486 (projective resolutions) #7487 (derived functors) and #7525 (Ext) is to provide you with a single "chosen" left_derived n F, for each functor F, and also to provide the API so you can bring your own favourite resolution, and know that (left_derived n F).obj X is isomorphic to the n-th homology of F applied to that resolution.

@Kevin Buzzard what Scott said here sounds like what's needed in the usual pen-and-paper maths construction of LES-from-SES for group cohomology. I remember inhomogeneous cocycles/coboundaries being very confusing, though great for computation, and I don't know much about the homogeneous ones. I also only know Inf-Res for H^1, and it always seemed quite strange to me because somehow it's about cohomologies in three different abelian categories rather than one. I don't know enough category theory to see this in a nice way.

[Eric Wieser]

@Kevin Buzzard, I think finsupp.equiv_congr is docs#finsupp.dom_congr.

[Mario Carneiro]

dom_congr also only works for add_comm_monoids

[Eric Wieser]

It's also badly named since the similar defs use domain instead of dom

[Mario Carneiro]

The definitions in equiv call this congr_left

[Eric Wieser]

docs#equiv.Pi_congr_left?

[Kyle Miller]

I'm a few days late to the party, but staring at this type

@[ext] structure cochain_succ :=
(to_fun : (fin n → G) → M)
(smul_apply' : ∀ (s : G) (g : fin n → G), s • to_fun g = to_fun (λ i, s * g i))

and thinking about @Scott Morrison's suggestion about distrib_mul_action, it seems like if you were to generalize fin n → G to an arbitrary G-module N, then this is exactly the definition of the type of G-module homomorphisms N → M:

import algebra.group_action_hom
import algebra.module.pi

universes uG uM

variables (G : Type uG) [group G]
variables (M : Type uM) [add_comm_group M] [distrib_mul_action G M]

abbreviation cochain_succ (n : ℕ) := (fin n → G) →[G] M

For my own education, I tried updating @Kevin Buzzard's implementation of d to use this type, hoping there was enough automatic stuff in mathlib already. There were some missing instances and simp lemmas, but it wasn't so bad:

import algebra.group_action_hom
import algebra.module.pi
import data.fin
import tactic

universes uG uM

variables (G : Type uG) [group G]
variables (M : Type uM) [add_comm_group M] [distrib_mul_action G M]

abbreviation cochain_succ (n : ℕ) := (fin n → G) →[G] M

instance (S : Type*) [mul_action G S] : add_comm_group (S →[G] M) :=
{ add := λ a b, { to_fun := λ s, a s + b s,
                  map_smul' := λ m c, by simp },
  zero := { to_fun := λ s, 0,
            map_smul' := λ m c, by simp },
  neg := λ a, { to_fun := λ s, -a s,
                map_smul' := λ m c, by simp },
  add_assoc := λ a b c, begin ext, apply add_assoc, end,
  add_comm := λ a b, begin ext, apply add_comm, end,
  zero_add := λ a, begin ext, apply zero_add, end,
  add_zero := λ a, begin ext, apply add_zero, end,
  add_left_neg := λ a, begin ext, apply add_left_neg, end }

@[simp]
lemma ev_zero (S : Type*) [mul_action G S] (s : S) :
  (0 : S →[G] M) s = 0 := rfl

@[simp]
lemma mul_action_hom.coe_eta_ev (S : Type*) [mul_action G S] (s : S)
  (f : S → M) (ax : ∀ (g : G) (s : S), f (g • s) = g • f s) :
  (mul_action_hom.mk f ax) s = f s := rfl

@[simp]
lemma mul_action_hom.add_ev (S : Type*) [mul_action G S]
  (f g : S →[G] M) (s : S) :
  (f + g) s = f s + g s := rfl

-- Copied from data.fin_simplicial_complex to make this code block self contained.
namespace fin
/-- The function denoted `δᵖ` by Riehl-Verity, sending`t` to `t` if `t<p` and
  `t.succ` otherwise.`-/
def delta {i j : ℕ} (hj : j = i + 1) (p : ℕ) (t : fin i) : fin j :=
-- fin.succ_above expects p : fin i.succ for some reason
⟨if (t : ℕ) < p then t else (t : ℕ).succ, begin
  subst hj,
  cases t with t ht,
  split_ifs,
  { exact ht.trans (nat.lt_succ_self _) },
  { exact nat.succ_lt_succ ht },
end⟩

lemma delta_eval {i j : ℕ} (hj : j = i + 1) (p : ℕ) (t : fin i) :
  (delta hj p t : ℕ) = if (t : ℕ) < p then t else (t : ℕ).succ := rfl

theorem delta_comm_apply  {i j k : ℕ} (hj : j = i.succ) (hk : k = j.succ) {p q : ℕ}
  (hpq : p ≤ q) (t : fin i) : delta hk q.succ (delta hj p t) = delta hk p (delta hj q t) :=
begin
  subst hk,
  subst hj,
  ext,
  cases t with t ht,
  simp only [delta_eval],
  dsimp,
  split_ifs;
  try {rw nat.succ_eq_add_one at *};
  try {push_neg at *};
  try {rw nat.succ_eq_add_one at *};
  try {linarith},
end

theorem delta_comm_apply.symm {i j k : ℕ} (hj : j = i.succ) (hk : k = j.succ) {p q_succ : ℕ}
  (hpq : q_succ ≤ p) (t : fin i) :
  delta hk p.succ (delta hj q_succ t) = delta hk q_succ (delta hj p t) :=
delta_comm_apply hj hk hpq t

end fin

def d {i j : ℕ} (hj : j = i + 1) : cochain_succ G M i →+ cochain_succ G M j :=
{ to_fun := λ c,
  { to_fun := λ g, (finset.range j).sum (λ p, (-1 : ℤ)^p • c $ λ t, g (fin.delta hj p t)),
    map_smul' := λ s g, begin
      rw [finset.smul_sum],
      simp,
      congr,
      ext,
      rw ←mul_action_hom.map_smul,
      congr,
    end },
  map_zero' := begin ext, simp, end,
  map_add' := λ a b, begin
    ext,
    change _ = _ + _,
    simp [smul_add, finset.sum_add_distrib],
  end }

I don't know if it's worth it, but that type is equivalent to

abbreviation cochain_succ (n : ℕ) := free_abelian_group (fin n → G) →[G] M

and then d comes from dualizing the chain complex of free_abelian_group (fin n → G) groups, which is essentially what others have already said. It might be worth factoring it like this if someone wanted to do group homology, too, but it seems like in the short term it would be work to develop the API for G-module homomorphisms from free abelian groups without any real payoff, assuming it doesn't already exist somewhere.

[Adam Topaz]

Note also that you don't need to take a free abelian group of anything, by the universal property of the free abelian group... It's just G-equivariant functions from n-tuples in G to N.

[Adam Topaz]

Oh sorry that's exactly what you wrote in the spoiler, Kyle :smile:

[Adam Topaz]

Anyway, this is already essentially the simplicial approach I was hoping for above.

[Adam Topaz]

For group homology you can replace functions with finsupp, and still avoid free abelian groups

[Adam Topaz]

Oh, and I just noticed Reid’s comment about EG/G from 2019…

[Amelia Livingston]

I have a bunch of files showing that the explicit description of group cohomology in terms of $Fun(G^n, M)$ is the same as Ext.
At some point while writing them I learned about delta functors and checked out the work on them & LES's in LTE. I got worried that my files are redundant and I should've been making the LTE stuff PR'able instead.
But I'm thinking there'd be a lot more work to do after that; stuff about universal delta functors would give you a correspondence with the right derived functors of the left exact functor $M^G$, and that's not what you want, really, because the cocycles etc in terms of $Fun(G^n, M)$ "come from" a projective resolution. So you'd need balancing of Ext or something, too, which seems like it might be hard.
So if I am thinking straight, I am hoping my work is still worth PR'ing. But I wanted to check.
Many thanks!

[Adam Topaz]

I think it's certainly worthwhile to have an explicit projective resolution of $\mathbb{Z}$ as a $G$-module (with the trivial action) in terms of $Fun(G^n,M)$ (which is essentially what the whole (in)homogeneous cocycle definition is all about).

[Adam Topaz]

That's the easiest way I know of showing, for example, that $H^1(G,A) = Hom(G,A)$ when $A$ has a trivial action, relating $H^2(G,M)$ to extensions, etc.

[Adam Topaz]

We should have the ability to "compute" Ext groups in terms of an explicit projective resolution (at least eventually).

[Amelia Livingston]

Fair play. Thank you!

[Adam Topaz]

@Amelia Livingston do you think it might be worthwhile to generalize a bit, and obtain a projective resolution of $A$ as a $A[G]$-module where $A$ is any commutative ring?

[Amelia Livingston]

Sure - I wasn't sure whether to do this. Could we just tensor by A instead?

[Amelia Livingston]

Hello - I want to open another PR for my group cohomology stuff; I'm not sure of the future of my current one because it could be done in better generality, as can be seen here.
I decided the complex of inhomogeneous cochains would be the best place to start right now. Would this be ok? And for the proof that d^2 = 0, should I make use of this (except I need the cochain version)?

Next PR after that could be some API for the cohomology in low degree, or the isomorphism of the complex of inhomog cochains with Hom(-, M) of a projective resolution. Also have a little file with Hilbert 90 in which doesn't technically rely on anything else.

[Joël Riou]

There are certainly different ways to do this. An approach could be to construct a resolution of A as an A[G]-module by starting from the construction of EG (which is a simplicial object in the category of G-sets). This could be done directly, or as a particular case of algebraic_topology.cech_nerve (applied to the map from the tautological G-set G to the terminal object); alternatively, this is also the nerve (now in mathlib) of a specific category. Then, the free A-module functor from sets to A-modules can be transformed into a functor F from G-sets to A-modules equipped with a G-action (i.e. A[G]-modules). Applying this functor F termwise gives a functor from simplicial G-sets to simplicial A[G]-modules. Applying this to EG, we get a certain simplicial A[G]-module, which we may denote A[EG], and then take the alternate face map complex attached to A[EG], which is a complex of A[G]-modules: it is a projective resolution of A as a A[G]-module. Using this resolution to compute Ext and by doing computations in appropriate bases, it should be possible to identify the differential to the usual differential on the usual cochain complex which computes group cohomology. (Note that I have not used cosimplicial objects, only simplicial objets! Even though at some point the alternate coface map complex should also be formalised.)

In this way, the explicit formulas for the differentials on the cochains would appear as a computation rather than as a definition, and it would save the penance of checking d^2=0.

However, I have skipped the details of some important step, which is why it is so that A[EG] is homotopic to A (in degree 0) when we forget the action of G. There are various ways to do that. The most direct approach I see would be to use an argument which appears in Goerss-Jardine, Simplicial Homotopy Theory, p. 190. (It is basically a sufficient condition for a simplicial set to be homotopy equivalent to a discrete set, and this condition of "having an extra degeneracy" is preserved when we apply the free A-module functor, and in the case of additive categories, the condition gives a chain complex homotopy. I could certainly help implementing this part.)

[Kevin Buzzard]

I am still unproud to say that we have 0 cohomology theories in mathlib, although we're clearly getting close, and my instinct would be to choose the path of least resistance, which would be homogeneous cochains, where d^2=0 is pretty easy, so they are in my view the shortest route to an actual definition of an object group_cohomolology.H n G M which we can then actually say exists. The moment we have existence, we can go on to prove that this object is all the other objects which we also call group cohomology, e.g. unhomogeneous cocycles/coboundaries, singular cohomology of these exotic spaces, derived functor cohomology etc, and opening the door to explicit computations in low degree such as "the answer to this question in group theory/field theory is an H^1" or "this theorem says that H^1 vanishes". Right now we can't do any of this stuff because we have no definition.

@Amelia Livingston Shenyang Wu developed group cohomology using unhomogeneous cocycles here and d^2=0 was painful. That's why I'm suggesting homogeneous cocycles.

[Joël Riou]

The model I suggested using the simplicial G-set EG gives exactly the homogeneous cochains! The n-simplices of EG are elements of G^{n+1} equipped with the obvious action of G. In mathlib terms, these are just fin (n+1) → G. Then, we need the free A-module functor, as a functor F from G-sets to A[G]-modules. Applying F to EG gives a simplicial A[G]-module whose alternate face map complex is the projective resolution of A which allows us to compute Ext as homogeneous cochains. That it is a complex of projective modules comes from the fact that F of a free G-set is a free A[G]-module. That it is a resolution follows that the argument I mentionned from the book by Goerss-Jardine. (Comparison with inhomogeneous cochains would presumably correspond to a particular choice of basis...)

[Kyle Miller]

Joël Riou said:

Comparison with inhomogeneous cochains would presumably correspond to a particular choice of basis...

If I remember correctly, if homogeneous cochains correspond to putting group elements at the vertices of simplices, then inhomogeneous cochains correspond to putting group elements along the spine of a simplex (the edges 0->1, 1->2, ..., n-1->n). Then, given a choice $g$ and an inhomogeneous cochain $(g_1,\dots,g_n)$, one can get a homogeneous cochain by "integrating", getting $(g,gg_1,gg_1g_2,\dots,gg_1g_2\dots g_n)$. Inhomogeneous cochains factor out the $G$ action, sort of pre-quotienting $EG$ to be $BG$, and each choice of $g$ gives a different lift of a $BG$ simplex to $EG$.

[Joël Riou]

In a draft branch https://github.com/leanprover-community/mathlib/blob/extra_degeneracy/src/algebraic_topology/extra_degeneracy.lean I have formalised the notion of extra degeneracy for an augmented simplicial object. The main definitions are

• the structure extra_degeneracy X for any X : simplicial_object.augmented C

• extra_degeneracy.map: extra degeneracies are preserved by the application of any
  functor C ⥤ D

• extra_degeneracy.for_cech_nerve_of_split_epi: the augmented Čech nerve of a split
  epimorphism has an extra degeneracy

• extra_degeneracy.preadditive.homotopy_equivalence: when the category C is
  preadditive and has a zero object, and X : simplicial_object.augmented C has an extra
  degeneracy, then the augmentation alternating_face_map_complex.ε.app X is a homotopy
  equivalence of chain complexes

Using this, one may easily get that A[EG] is a resolution of A as an A-module. Taking into account the A[G]-modules structures, one may deduce that A[EG] is a (projective) resolution of A as an A[G]-module, and then that the homogeneous cochains can be used to compute Ext groups.

[Joël Riou]

@Amelia Livingston After more thinking, it seems that as you suggested, you may need the dual version of the functor alternating_face_map_complex. It should be easy to define

def alternating_coface_map_complex : cosimplicial_object C ⥤ cochain_complex C ℕ := sorry

by using alternating_face_map_complex for the opposite category and the duality equivalences for simplicial objects or functors (in mathlib) and for homological complexes (it seems that homological_complex.op_equivalence {ι : Type*} (c : complex_shape ι) : (homological_complex Cᵒᵖ c)ᵒᵖ ≌ homological_complex C c.symm is not in mathlib yet).

Then, in order to get the homogeneous cochain complex, you would have to define a cosimplicial A-module attached to any A[G]-module M by sending the integer (n : simplex_category) to G-equivariant maps (fin (n+1) → G) → M, and apply alternating_coface_map_complex. Definitionally speaking, this might be better than using cech_nerve (which would involve taking wide_pullbacks of n+1 copies to the map G → *. The machinery I have suggested above would then enable us to do a comparison with Ext groups in the category of A[G]-modules.

[Johan Commelin]

Joël Riou said:

Amelia Livingston After more thinking, it seems that as you suggested, you may need the dual version of the functor alternating_face_map_complex. It should be easy to define

def alternating_coface_map_complex : cosimplicial_object C ⥤ cochain_complex C ℕ := sorry

by using alternating_face_map_complex for the opposite category and the duality equivalences for simplicial objects or functors (in mathlib) and for homological complexes (it seems that homological_complex.op_equivalence {ι : Type*} (c : complex_shape ι) : (homological_complex Cᵒᵖ c)ᵒᵖ ≌ homological_complex C c.symm is not in mathlib yet).

This is done in LTE: https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/homological_complex_op.lean
Feel free to copy it elsewhere (eg mathlib).

[Johan Commelin]

Also, https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/simplicial/complex.lean contains that coface cochain complex.

[Joël Riou]

Johan Commelin said:

Also, https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/simplicial/complex.lean contains that coface cochain complex.

It is nice that the dualisation of homological complexes is in LTE :smiley:
As the alternating_face_map_complexfunctor is already in mathlib, I would suggest not duplicating all the definitions and proofs (as it is done for limits/colimits, projectives/injectives), but rather obtain the coface version by dualising the functor alternating_face_map_complex and stating an appropriate simp lemma for the calculation of the differential (which may not be a definitional equality ?).

[Johan Commelin]

I did that for coboundary. So the fact that d² = 0 is deduced from the other version.

[Johan Commelin]

But it can probably be optimised a bit.

[Johan Commelin]

In fact, I think both versions should be refactored: every (co)simplicial object in C should give rise to a (co)chain complex in free ℤ C (the category with the same objects as C, but all the homsets replaced by their freely-generated ab groups).

[Joël Riou]

Johan Commelin said:

In fact, I think both versions should be refactored: every (co)simplicial object in C should give rise to a (co)chain complex in free ℤ C (the category with the same objects as C, but all the homsets replaced by their freely-generated ab groups).

I do not think so, because the construction you describe can be very easily deduced from the existing one: whisker your (co)simplicial object in C with the functor C ⥤ free ℤ C and then apply the alternating (co)face map complex functor.

[Joël Riou]

I have just PRed #14588 the definition of the alternating coface map complex.

[Joël Riou]

The definition of the alternating coface map complex is now in mathlib.