Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-11 13:09 348289cc

View on Github →

feat(representation_theory/group_cohomology_resolution): add chain complex underlying the standard resolution (#16258)

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem int_cast_smul

Modified src/representation_theory/Action.lean

added def Action.of_mul_action

added theorem Action.of_mul_action_apply

added def Action.of_mul_action_limit_cone

added theorem Action.sum_hom

Modified src/representation_theory/Rep.lean

added theorem Rep.linearization_map_hom

added theorem Rep.linearization_map_hom_of

added theorem Rep.linearization_obj_ρ

added theorem Rep.linearization_of

Modified src/representation_theory/group_cohomology_resolution.lean

deleted def Rep.of_mul_action

added def classifying_space_universal_cover.cech_nerve_iso

added def classifying_space_universal_cover.cech_nerve_obj_iso

added def classifying_space_universal_cover.wide_cospan.limit_cone

added def classifying_space_universal_cover.wide_cospan

added def classifying_space_universal_cover

added def group_cohomology.resolution.X_iso

added def group_cohomology.resolution.d

added theorem group_cohomology.resolution.d_eq

added theorem group_cohomology.resolution.d_of

added def group_cohomology.resolution