decidable equality frustrations with group homology

Stream: mathlib4

[Kevin Buzzard]

Group homology and group cohomology have similar but "dual" APIs and at the Oxford class field theory workshop it was proposed to write an which could in some cases take a lemma about group cohomology and prove a dual lemma about group homology, analogous to @[to_additive].

But this proposal has run into an unexpected roadblock: the definition of group cohomology internally uses functions G^n -> M, and the definition of group homology internally uses finitely-supported functions G^n -> M and these are implemented via Finsupp which means that G needs to have decidable equality for many results in group homology, but it is not necessary for group cohomology. I mentioned this briefly before in #mathlib4 > Keeping a def computable with inversion @ 💬 but it didn't bother me much back then; it now bothers me a bit more though because it means that it's far less clear how to write the @[to_homology] attribute.

Group homology is relatively new to mathlib and it would perhaps be feasible to refactor it to not use Finsupp but do we even have non-constructive finitely-supported functions?

Another hack would be to let the attribute just add a nonconstructive DecidableEq G instance but this doesn't sound like a good idea if we are unlucky enough to ever want to say anything about homology of a group which happens to have decidable equality. My initial reaction was that this would basically never happen but unfortunately today at the workshop we needed a proof that the trivial group had trivial homology and unfortunately the idiomatic way to say a group is trivial seems to be [Subsingleton G] and we have docs#decidableEq_of_subsingleton . This is
super-frustrating because the decidability is not buying us anything here, it is literally just getting in the way. Perhaps it's worth stressing here that rfl doesn't buy us anything in the proof that the trivial group has trivial homology; the proof has a little content, is not rfl, and decidability is literally doing nothing but getting in the way.

A horrible fix would be to demand that G had decidable equality in group cohomology too but my thoughts on that approach are unprintable.

[Eric Wieser]

Group homology is relatively new to mathlib and it would perhaps be feasible to refactor it to not use Finsupp but do we even have non-constructive finitely-supported functions?

Are finsupps an implementation detail or part of the API?

[Kevin Buzzard]

I'm not sure I understand the question well enough to be able to answer it.

[Eric Wieser]

Does anyone doing group homology need to know that it's finsupp under the hood?

[Eric Wieser]

I had a quick go at swapping Finsupp for DFinsupp; the result is worse, because DFinsupp is computable in the wrong direction. I speculate that swapping Finsupp for docs#FreeAbelianGroup might make everything computable without the cost of DecidableEq, but would be annoying due to lack of API nevermind, that's not the type I thought it was