Group homology in degrees zero and one

Complements to Mathlib's Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, which identifies H₀(G, A) with the coinvariants of A, and H₁(G, A) with Gᵃᵇ ⊗ A for trivial coefficients A.

Main results

• TauCeti.groupHomology.H0π_eq_iff: two elements of A have the same class in H₀(G, A) exactly when their difference lies in the augmentation submodule Representation.Coinvariants.ker A.ρ.
• TauCeti.groupHomology.isZero_H1_of_forall_exists_zpow_eq: if every element of G is an m-th power and m kills the trivial coefficients A, then H₁(G, A) = 0.

theorem TauCeti.groupHomology.H0π_eq_iff {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {x y : ↑A} : (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π A)) x = (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π A)) y ↔ x - y ∈ Representation.Coinvariants.ker A.ρ

Two elements of A have the same class in H₀(G, A) exactly when their difference lies in the augmentation submodule Representation.Coinvariants.ker A.ρ, the kernel of the projection to the coinvariants.

theorem TauCeti.groupHomology.isZero_H1_of_forall_exists_zpow_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (m : ℤ) (hG : ∀ (g : G), ∃ (x : G), x ^ m = g) (hA : ∀ (a : ↑A), m • a = 0) : CategoryTheory.Limits.IsZero (groupHomology.H1 A)

First homology of a divisible group. If every element of G is an m-th power and multiplication by m is zero on the trivial representation A, then H₁(G, A) = Gᵃᵇ ⊗ A vanishes.