group cohomology mathlib3 PR

Stream: mathlib4

[Kevin Buzzard]

Group cohomology is three files away from being ported, but after some discussion with Amelia on Thurs she convinced herself that there should be a mathlib3 refactor and more precisely the internal homs on Rep k G should be defined concretely rather than transporting an instance along a category equivalence (which was troublesome to port as well as being troublesome to work with). The mathlib3 PR is #19170 , it looks good to me, it results in a net decrease of lines, but it would be good if a category theory expert e.g. @Joël Riou or @Scott Morrison or @Adam Topaz could sign off on this one.

[Yury G. Kudryashov]

@Amelia Livingston If not done yet, could you please add a "don't port yet" comments to relevant files on https://github.com/leanprover-community/mathlib4/wiki/port-comments/_edit ?

[Kevin Buzzard]

I've now done this.

[Scott Morrison]

Yes, I agree this is a good idea. The underlying problem is probably my fault: in my defence I'll claim that it is often a useful experiment to see if working "by transport of structure" is viable, but that I should have flagged this as potentially needed a refactor. :-)

[Adam Topaz]

I think such transport constructions are certainly useful and mostly viable as is. The right approach in general is probably to provide copy constructions similar to what we have in the order library to preserve whatever defeq properties we want. In this case I think Rep k is explicit and useful enough that doing everything directly is perfectly fine as well.

[Kevin Buzzard]

My understanding (possibly incorrect) was that copy was harder than it looked because this is not just like submonoid, there is higher structure which has to typecheck.