Commit 2025-07-11 14:29 f91eca79

feat(RepresentationTheory/Homological/GroupHomology/LowDegree): specialized API for H0, H1, H2 (#25908) Given a k-linear G-representation A, this PR defines and provides API for:

• groupHomology.H0Iso A: isomorphism between H₀(G, A) and the coinvariants A_G of the G-representation on A.
• groupHomology.H1π A: epimorphism from the 1-cycles (defined as Ker(d₀ : (G →₀ A) → A))) to H₁(G, A).
• groupHomology.H2π A: epimorphism from the 2-cycles (defined as Ker(d₁ : (G² →₀ A) → (G →₀ A))) to H₂(G, A).