The group homology of a k-linear G-representation

Let k be a commutative ring and G a group. This file defines the group homology of A : Rep k G to be the homology of the complex $$\dots \to \bigoplus_{G^2} A \to \bigoplus_{G^1} A \to \bigoplus_{G^0} A$$ with differential $d_n$ sending $a\cdot (g_0, \dots, g_n)$ to $$\rho(g_0^{-1})(a)\cdot (g_1, \dots, g_n)$$ $$+ \sum_{i = 0}^{n - 1}(-1)^{i + 1}a\cdot (g_0, \dots, g_ig_{i + 1}, \dots, g_n)$$ $$+ (-1)^{n + 1}a\cdot (g_0, \dots, g_{n - 1})$$ (where ρ is the representation attached to A).

We have a k-linear isomorphism $\bigoplus_{G^n} A \cong (A \otimes_k \left(\bigoplus_{G^n} k[G]\right))_G$ given by Rep.coinvariantsTensorFreeLEquiv. If we conjugate the $n$th differential in $(A \otimes_k P)_G$ by this isomorphism, where P is the bar resolution of k as a trivial k-linear G-representation, then the resulting map agrees with the differential $d_n$ defined above, a fact we prove.

Hence our $d_n$ squares to zero, and we get $\mathrm{H}_n(G, A) \cong \mathrm{Tor}_n(A, k),$ where $\mathrm{Tor}$ is defined by deriving the second argument of the functor $(A, B) \mapsto (A \otimes_k B)_G.$

Main definitions

• Rep.Tor k G n: the left-derived functors given by deriving the second argument of $(A, B) \mapsto (A \otimes_k B)_G$.
• Rep.coinvariantsTensorBarResolution A: a complex whose objects are $(A \otimes_k \left(\bigoplus_{G^n} k[G]\right))_G$ and whose homology is the group homology $\mathrm{H}_n(G, A)$.
• groupHomology.inhomogeneousChains A: a complex whose objects are $\bigoplus_{G^n} A$ and whose homology is the group homology $\mathrm{H}_n(G, A).$
• groupHomology.inhomogeneousChainsIso A: an isomorphism between the above two complexes.
• groupHomology A n: this is $\mathrm{H}_n(G, A),$ defined as the $n$th homology of the second complex, inhomogeneousChains A.
• groupHomologyIsoTor A n: an isomorphism $\mathrm{H}_n(G, A) \cong \mathrm{Tor}_n(A, k)$ induced by inhomogeneousChainsIso A.

Implementation notes

Group homology is typically stated for G-modules, or equivalently modules over the group ring ℤ[G]. However, ℤ can be generalized to any commutative ring k, which is what we use. Moreover, we express k[G]-module structures on a module k-module A using the Rep definition. We avoid using instances Module (MonoidAlgebra k G) A so that we do not run into possible scalar action diamonds.

Note that the existing definition of Tor in Mathlib.CategoryTheory.Monoidal.Tor is for monoidal categories, and the bifunctor we need to derive here maps to ModuleCat k. Hence we define Rep.Tor k G n by instead left-deriving the second argument of Rep.coinvariantsTensor k G: $(A, B) \mapsto (A \otimes_k B)_G$. The functor Rep.coinvariantsTensor k G is naturally isomorphic to the functor sending A, B to A ⊗[k[G]] B, where we give A the k[G]ᵐᵒᵖ-module structure defined by g • a := A.ρ g⁻¹ a, but currently mathlib's TensorProduct is only defined for commutative rings.

TODO

• API for homology in low degree: $\mathrm{H}_0, \mathrm{H}_1$ and $\mathrm{H}_2.$ For example, the corestriction-coinflation exact sequence.
• The long exact sequence in homology attached to a short exact sequence of representations.
• Upgrading groupHomologyIsoTor to an isomorphism of derived functors.

def Rep.Tor (k G : Type u) [CommRing k] [Group G] (n : ℕ) : CategoryTheory.Functor (Rep k G) (CategoryTheory.Functor (Rep k G) (ModuleCat k))

The left-derived functors given by deriving the second argument of A, B ↦ (A ⊗[k] B)_G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.Tor_map (k G : Type u) [CommRing k] [Group G] (n : ℕ) {X✝ Y✝ : Rep k G} (f : X✝ ⟶ Y✝) : (Tor k G n).map f = CategoryTheory.NatTrans.leftDerived ((coinvariantsTensor k G).map f) n

@[simp]

theorem Rep.Tor_obj (k G : Type u) [CommRing k] [Group G] (n : ℕ) (X : Rep k G) : (Tor k G n).obj X = ((coinvariantsTensor k G).obj X).leftDerived n

theorem Rep.isZero_Tor_succ_of_projective {k G : Type u} [CommRing k] [Group G] (X Y : Rep k G) [CategoryTheory.Projective Y] (n : ℕ) : CategoryTheory.Limits.IsZero (((Tor k G (n + 1)).obj X).obj Y)

The higher Tor groups for X and Y are zero if Y is projective.

@[reducible, inline]

abbrev Rep.coinvariantsTensorBarResolution {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] : HomologicalComplex (ModuleCat k) (ComplexShape.down ℕ)

Given a k-linear G-representation A, this is the chain complex (A ⊗[k] P)_G, where P is the bar resolution of k as a trivial representation.

Equations

• A.coinvariantsTensorBarResolution = (((Rep.coinvariantsTensor k G).obj A).mapHomologicalComplex (ComplexShape.down ℕ)).obj (Rep.barComplex k G)

def groupHomology.inhomogeneousChains.d {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ℕ) : ModuleCat.of k ((Fin (n + 1) → G) →₀ ↑A.V) ⟶ ModuleCat.of k ((Fin n → G) →₀ ↑A.V)

The differential in the complex of inhomogeneous chains used to calculate group homology.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.inhomogeneousChains.d_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (n : ℕ) (g : Fin (n + 1) → G) (a : ↑A.V) : (CategoryTheory.ConcreteCategory.hom (d A n)) (Finsupp.single g a) = Finsupp.single (fun (i : Fin n) => g i.succ) ((A.ρ (g 0)⁻¹) a) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • Finsupp.single (j.contractNth (fun (x1 x2 : G) => x1 * x2) g) a

theorem groupHomology.inhomogeneousChains.d_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ℕ) [DecidableEq G] : d A n = CategoryTheory.CategoryStruct.comp (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv (CategoryTheory.CategoryStruct.comp (A.coinvariantsTensorBarResolution.d (n + 1) n) (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom)

@[reducible, inline]

noncomputable abbrev groupHomology.inhomogeneousChains {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] : ChainComplex (ModuleCat k) ℕ

Given a k-linear G-representation A, this is the complex of inhomogeneous chains $$\dots \to \bigoplus_{G^1} A \to \bigoplus_{G^0} A \to 0$$ which calculates the group homology of A.

Equations

• groupHomology.inhomogeneousChains A = ChainComplex.of (fun (n : ℕ) => ModuleCat.of k ((Fin n → G) →₀ ↑A.V)) (fun (n : ℕ) => groupHomology.inhomogeneousChains.d A n) ⋯

theorem groupHomology.inhomogeneousChains.ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {n : ℕ} [DecidableEq G] {M : ModuleCat k} {x y : (inhomogeneousChains A).X n ⟶ M} (h : ∀ (g : Fin n → G), CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle g)) x = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle g)) y) : x = y

theorem groupHomology.inhomogeneousChains.ext_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {n : ℕ} [DecidableEq G] {M : ModuleCat k} {x y : (inhomogeneousChains A).X n ⟶ M} : x = y ↔ ∀ (g : Fin n → G), CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle g)) x = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle g)) y

theorem groupHomology.inhomogeneousChains.d_def {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] (n : ℕ) : (inhomogeneousChains A).d (n + 1) n = d A n

theorem groupHomology.inhomogeneousChains.d_comp_d {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (n : ℕ) [DecidableEq G] : CategoryTheory.CategoryStruct.comp (d A (n + 1)) (d A n) = 0

def groupHomology.inhomogeneousChainsIso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] : inhomogeneousChains A ≅ A.coinvariantsTensorBarResolution

Given a k-linear G-representation A, the complex of inhomogeneous chains is isomorphic to (A ⊗[k] P)_G, where P is the bar resolution of k as a trivial G-representation.

Equations

• groupHomology.inhomogeneousChainsIso A = HomologicalComplex.Hom.isoOfComponents (fun (i : ℕ) => (A.coinvariantsTensorFreeLEquiv (Fin i → G)).toModuleIso.symm) ⋯

@[reducible, inline]

abbrev groupHomology.cycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] (n : ℕ) : ModuleCat k

The n-cycles Zₙ(G, A) of a k-linear G-representation A, i.e. the kernel of the differential Cₙ(G, A) ⟶ Cₙ₋₁(G, A) in the complex of inhomogeneous chains.

Equations

• groupHomology.cycles A n = HomologicalComplex.cycles (groupHomology.inhomogeneousChains A) n

@[reducible, inline]

abbrev groupHomology.iCycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] (n : ℕ) : cycles A n ⟶ (inhomogeneousChains A).X n

The natural inclusion of the n-cycles Zₙ(G, A) into the n-chains Cₙ(G, A).

Equations

• groupHomology.iCycles A n = HomologicalComplex.iCycles (groupHomology.inhomogeneousChains A) n

@[reducible, inline]

abbrev groupHomology.toCycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] (i j : ℕ) : (inhomogeneousChains A).X i ⟶ cycles A j

This is the map from i-chains to j-cycles induced by the differential in the complex of inhomogeneous chains.

Equations

• groupHomology.toCycles A i j = HomologicalComplex.toCycles (groupHomology.inhomogeneousChains A) i j

def groupHomology {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : ModuleCat k

The group homology of a k-linear G-representation A, as the homology of its complex of inhomogeneous chains.

Equations

• groupHomology A n = HomologicalComplex.homology (groupHomology.inhomogeneousChains A) n

@[reducible, inline]

abbrev groupHomology.π {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : cycles A n ⟶ groupHomology A n

The natural map from n-cycles to nth group homology for a k-linear G-representation A.

Equations

• groupHomology.π A n = HomologicalComplex.homologyπ (groupHomology.inhomogeneousChains A) n

theorem groupHomology_induction_on {k G : Type u} [CommRing k] [Group G] [DecidableEq G] {A : Rep k G} {n : ℕ} {C : ↑(groupHomology A n) → Prop} (x : ↑(groupHomology A n)) (h : ∀ (x : ↑(groupHomology.cycles A n)), C ((CategoryTheory.ConcreteCategory.hom (groupHomology.π A n)) x)) : C x

def groupHomologyIsoTor {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : groupHomology A n ≅ ((Rep.Tor k G n).obj A).obj (Rep.trivial k G k)

The nth group homology of a k-linear G-representation A is isomorphic to Torₙ(A, k) (taken in Rep k G), where k is a trivial k-linear G-representation.

Equations

• One or more equations did not get rendered due to their size.

theorem isZero_groupHomology_succ_of_subsingleton {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) [Subsingleton G] (n : ℕ) : CategoryTheory.Limits.IsZero (groupHomology A (n + 1))