Commit 2025-05-29 14:16 304e3a7d

View on Github →

refactor(RepresentationTheory/GroupCohomology/*): replace nCochainsLequiv with isomorphisms in ModuleCat for n = 0, 1, 2 (#24693) These are more useful as ModuleCat isos in practice.

Estimated changes

Modified Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean

added theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsIso

deleted theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsLequiv

added theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsIso

deleted theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsLequiv

added theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsIso

deleted theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsLequiv

added theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsIso

deleted theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsLequiv

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

added def groupCohomology.H0IsoOfIsTrivial

added theorem groupCohomology.H0IsoOfIsTrivial_hom_apply

added theorem groupCohomology.H0IsoOfIsTrivial_hom_hom

added theorem groupCohomology.H0IsoOfIsTrivial_inv_apply

deleted def groupCohomology.H0LequivOfIsTrivial

deleted theorem groupCohomology.H0LequivOfIsTrivial_apply

deleted theorem groupCohomology.H0LequivOfIsTrivial_eq_subtype

deleted theorem groupCohomology.H0LequivOfIsTrivial_symm_apply

added def groupCohomology.H1IsoOfIsTrivial

added theorem groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply

added theorem groupCohomology.H1IsoOfIsTrivial_symm_apply

deleted def groupCohomology.H1LequivOfIsTrivial

deleted theorem groupCohomology.H1LequivOfIsTrivial_H1_π_apply_apply

deleted theorem groupCohomology.H1LequivOfIsTrivial_comp_H1π

deleted theorem groupCohomology.H1LequivOfIsTrivial_symm_apply

added theorem groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom

added theorem groupCohomology.comp_dOne_eq

added theorem groupCohomology.comp_dTwo_eq

added theorem groupCohomology.comp_dZero_eq

modified def groupCohomology.dOne

added theorem groupCohomology.dOne_comp_dTwo

deleted theorem groupCohomology.dOne_comp_dZero

deleted theorem groupCohomology.dOne_comp_eq

modified def groupCohomology.dTwo

deleted theorem groupCohomology.dTwo_comp_dOne

deleted theorem groupCohomology.dTwo_comp_eq

modified def groupCohomology.dZero

modified def groupCohomology.dZeroArrowIso

added theorem groupCohomology.dZero_comp_dOne

deleted theorem groupCohomology.dZero_comp_eq

deleted theorem groupCohomology.dZero_comp_subtype

modified theorem groupCohomology.dZero_ker_eq_invariants

added def groupCohomology.oneCochainsIso

deleted def groupCohomology.oneCochainsLequiv

modified def groupCohomology.oneCocycles

added def groupCohomology.oneCocyclesIsoOfIsTrivial

deleted def groupCohomology.oneCocyclesLequivOfIsTrivial

added theorem groupCohomology.subtype_comp_dZero

added def groupCohomology.threeCochainsIso

deleted def groupCohomology.threeCochainsLequiv

added def groupCohomology.twoCochainsIso

deleted def groupCohomology.twoCochainsLequiv

modified def groupCohomology.twoCocycles

added def groupCohomology.zeroCochainsIso

deleted def groupCohomology.zeroCochainsLequiv