Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-03 13:04 ef997baa

View on Github →

feat(representation_theory/group_cohomology/basic): add standard definition of group cohomology (#18341) We define the complex of inhomogeneous cochains, define group cohomology to be its cohomology, and prove this is isomorphic to the appropriate Ext groups.

Estimated changes

Modified src/algebra/big_operators/fin.lean

added theorem fin.inv_partial_prod_mul_eq_contract_nth

Modified src/data/fin/tuple/basic.lean

added def fin.contract_nth

added theorem fin.contract_nth_apply_of_eq

added theorem fin.contract_nth_apply_of_gt

added theorem fin.contract_nth_apply_of_lt

added theorem fin.contract_nth_apply_of_ne

Created src/representation_theory/group_cohomology/basic.lean

added def group_cohomology.inhomogeneous_cochains_iso

added def group_cohomology.linear_yoneda_obj_resolution

added theorem group_cohomology.linear_yoneda_obj_resolution_d_apply

added def group_cohomology

added def group_cohomology_iso_Ext

added def inhomogeneous_cochains.d

added theorem inhomogeneous_cochains.d_eq

Renamed src/representation_theory/group_cohomology_resolution.lean to src/representation_theory/group_cohomology/resolution.lean

modified theorem Rep.diagonal_hom_equiv_apply

modified theorem Rep.diagonal_hom_equiv_symm_apply

added theorem Rep.diagonal_hom_equiv_symm_partial_prod_succ