Commit 2023-11-08 04:41 2852d235

View on Github →

feat(RepresentationTheory/GroupCohomology/LowDegree): H¹(G, A) ≃ Hom(G, A) for a trivial representation (#7988)

Estimated changes

Modified Mathlib/RepresentationTheory/Basic.lean

added theorem Representation.apply_eq_self

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

added def groupCohomology.H0LequivOfIsTrivial

added theorem groupCohomology.H0LequivOfIsTrivial_apply

added theorem groupCohomology.H0LequivOfIsTrivial_eq_subtype

added theorem groupCohomology.H0LequivOfIsTrivial_symm_apply

added def groupCohomology.H1LequivOfIsTrivial

added theorem groupCohomology.H1LequivOfIsTrivial_H1_π_apply_apply

added theorem groupCohomology.H1LequivOfIsTrivial_comp_H1_π

added theorem groupCohomology.H1LequivOfIsTrivial_symm_apply

modified theorem groupCohomology.dOne_comp_eq

modified theorem groupCohomology.dZero_comp_eq

added theorem groupCohomology.dZero_eq_zero

added theorem groupCohomology.mem_oneCocycles_of_addMonoidHom

added theorem groupCohomology.oneCoboundaries_eq_bot_of_isTrivial

added def groupCohomology.oneCochainsLequiv

deleted def groupCohomology.oneCochainsLinearEquiv

added def groupCohomology.oneCocyclesLequivOfIsTrivial

modified theorem groupCohomology.oneCocycles_map_inv

added theorem groupCohomology.oneCocycles_map_mul_of_isTrivial

modified theorem groupCohomology.oneCocycles_map_one

added def groupCohomology.threeCochainsLequiv

deleted def groupCohomology.threeCochainsLinearEquiv

added def groupCohomology.twoCochainsLequiv

deleted def groupCohomology.twoCochainsLinearEquiv

added def groupCohomology.zeroCochainsLequiv

deleted def groupCohomology.zeroCochainsLinearEquiv

Modified Mathlib/RepresentationTheory/Invariants.lean

added theorem Representation.invariants_eq_top

Modified Mathlib/RepresentationTheory/Rep.lean