cohomology, and subgroups of subgroups

Stream: maths

[Kevin Buzzard]

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]

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
(note: property means set)

You will indeed need lemma's/constructions, like if Z and B are both subgroups of G and 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]

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]

Can we do most of the subgroup theory using injective group homs instead? Sounds a bit like the localisation issue.

[Reid Barton]

If you want to do homological algebra in an arbitrary abelian category then you are forced to do what Chris suggests anyways

[Jeremy Avigad]

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]

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]

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 subtype.mk.

[Kevin Buzzard]

@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]

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?