[Merged by Bors] - feat(representation_theory/group_cohomology/basic): add standard definition of group cohomology

[101damnations]

We define the complex of inhomogeneous cochains, define group cohomology to be its cohomology, and prove this is isomorphic to the appropriate Ext groups.

---

I've defined the complex to be $0 \to Fun(G^0, M) \to Fun(G^1, M) \to \dots$ as it makes things simpler for now, and then when I add API for $H^0$ and $H^1$ I can give better expressions for low degree cochains. Rather than just defining the complex to be $0 \to M \to Fun(G, M) \to \dots$ from the start. Not sure which is better or if it matters much.

• depends on: [Merged by Bors] - feat(representation_theory/Rep): describe monoidal closed structure #18148
• depends on: [Merged by Bors] - feat(representation_theory/group_cohomology_resolution): add isomorphism with nth inhomogeneous cochains #18159
  

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[eric-wieser]

Please don't do this until the merge is completed and through mathport (i.e. it appears on https://leanprover-community.github.io/mathlib-port-status/out-of-sync and is not red)

Everything is set for you to forward-port this now; just search https://leanprover-community.github.io/mathlib-port-status/out-of-sync for your name and click on the two files that come up.