Kevin Buzzard (May 31 2019 at 22:04):
Cocycles are subgroups of cochains; coboundaries are subgroups of cocycles. Cohomology groups are cocycles over coboundaries. At least, that's how it works in group cohomology, and maybe in topology too.
I guess the cocycles will have to end up being a type at some point, because many arguments involve chasing cocycles and then proving that everything descends...sorry...lifts...to cohomology classes. (That still leaves a bad taste in my mouth). But the coboundaries are going to end up being a subtype of a subtype, which is kind of silly. In general we'll have a group
G and then
Z B : set G with
B \subseteq Z, but will end up using the subtype corresponding to
B and then we'll have to make the subtype of
B corresponding to
Z. Is this a situation where I should just try something and see if it works? Have we already run into this issue @Reid Barton @Floris van Doorn ? Am I fussing over nothing? I have a student working on group cohomology and this is about to hit us.
Floris van Doorn (May 31 2019 at 22:35):
In the Lean 2 HoTT library I've done homology (in this case of modules over a ring - obviously at some point we want to do it generally in an abelian category): https://github.com/cmu-phil/Spectral/blob/master/algebra/submodule.hlean#L376
You will indeed need lemma's/constructions, like if
B are both subgroups of
B \subseteq Z then
B is a subgroup of
Z. Of course, the last
B is not actually
B but something like
(subtype.val \-1' B : set Z). But everything works fine.
@Jeremy Avigad might tell you a different story, which is also worth considering. The idea is that if you do a lot of group theory in a single group
G, you should be really doing subgroup theory. That means that for every definition and lemma, when a mathematician would write "Group", you would write "subgroup of
G". And then you try to reason as much as you can using sets (and subsets) instead of subtypes. Jeremy can probably tell this story better.
Patrick Massot (May 31 2019 at 22:54):
I think this always the same story, explained in https://hal.inria.fr/hal-00825074v1/document that was already quoted countless times on this chat
Chris Hughes (May 31 2019 at 23:22):
Can we do most of the subgroup theory using injective group homs instead? Sounds a bit like the localisation issue.
Reid Barton (Jun 01 2019 at 05:57):
If you want to do homological algebra in an arbitrary abelian category then you are forced to do what Chris suggests anyways
Jeremy Avigad (Jun 01 2019 at 13:01):
I was just conveying Georges' story, but I spent a year with Georges formalizing finite group theory, and I think he got that part right. The point is that finite group theory really is finite subgroup theory. There are zillions of constructions of subgroups-- intersections, subgroups generated by elements, conjugates, p-cores, the Frattini subgroup, products, semidirect products, etc., etc. The usual style of argumentation involves elementhood and inclusions between them subgroup. It is fiddly and combinatorial, and it would be a mess to carry them out if each construction took you to a different type.
Kevin Buzzard (Jun 01 2019 at 14:58):
I need this for a student project and I want to get it right. Seems to me that Assia is talking subgroups but Chris is suggesting something else. Chris' solution looks mathematically meaningful to me; an injection is canonically isomorphic to an inclusion and it's good to be as flexible as we can
Chris Hughes (Jun 01 2019 at 15:03):
The downside of my approach is that the lattice of subgroups, or any other structure on the subgroups moves up a universe. And then there's the question of whether we should demand a computable partial inverse i.e. an equivalent of
Kevin Buzzard (Jun 02 2019 at 14:00):
@Assia Mahboubi 's story is about finite groups. We are thinking about typically infinite abelian groups. This might change things. Furthermore, in her situation one can imagine wanting to think about lots of subgroups of a group. We have cochains, cocycles, coboundaries, and that's it.
Maybe this is a situation where I should just try something and see how it works out.
Kevin Buzzard (Jun 04 2019 at 07:38):
Thinking about this a bit more, I think that perhaps we just need a general theory of cokernels of morphisms in our various concrete abelian categories. And such a theory would have to be rewritten when we bundle these morphisms. @Chris Hughes is there any progress on bundling?
Last updated: May 09 2021 at 10:11 UTC