Commit 2025-07-10 15:14 c88ccece

feat(RepresentationTheory/Homological/GroupHomology/LowDegree): add IsCycle₁ predicate and friends (#25884) Given an additive abelian group A with an appropriate scalar action of G, we provide support for turning a finsupp f : G →₀ A satisfying the 1-cycle identity into an element of the cycles₁ of the representation on A corresponding to the scalar action. We also do this for 0-boundaries, 1-boundaries, 2-cycles and 2-boundaries. We follow the structure of RepresentationTheory/Homological/GroupCohomology/LowDegree.lean.