Functoriality of group homology

Mathlib shows that the functor groupHomology.chainsFunctor k G sending a representation to its complex of inhomogeneous chains preserves zero morphisms. This file shows that it is additive, matching Mathlib's instance for its cohomological counterpart groupCohomology.cochainsFunctor.

It also records how the map on first homology induced by a group homomorphism f : H →* G reads through Mathlib's identification H₁(G, A) ≃ Gᵃᵇ ⊗ A for trivial coefficients: it is Abelianization.map f tensored with the coefficients. With trivial coefficients, the vanishing of group homology is also transported along isomorphisms of groups.

Main results

• TauCeti.groupHomology.chainsFunctorAdditive: the chains functor is additive.
• groupHomology.map_id_nsmul_id: so Hₙ(G, -) sends c • 𝟙 to multiplication by c.
• TauCeti.groupHomology.map_mkH1OfIsTrivial: with trivial coefficients, the map on H₁ induced by f : H →* G and φ : A ⟶ Res(f)(B) sends the class of x ⊗ a to that of f x ⊗ φ a.
• TauCeti.groupHomology.H1AddEquivOfIsTrivial_map: with trivial coefficients, change of group and a coefficient map act as Abelianization.map f ⊗ φ.
• MulEquiv.subsingleton_groupHomology: vanishing of group homology with trivial coefficients is invariant under group isomorphisms.
• Rep.chainsMap_inclusion_comp_chainsMap_subtype: the maps of inhomogeneous chains induced by inclusions of subgroups S ≤ T ≤ G compose.
• Rep.map_inclusion_comp_map_subtype: so do the induced maps on homology.

instance TauCeti.groupHomology.chainsFunctorAdditive {R G : Type u} [CommRing R] [Group G] : (groupHomology.chainsFunctor R G).Additive

The functor from representations to inhomogeneous group-homology chains is additive.

@[simp]

theorem TauCeti.groupHomology.map_mkH1OfIsTrivial {R G : Type u} [CommRing R] [Group G] {H : Type u} [Group H] (f : H →* G) {A : Rep R H} {B : Rep R G} [A.IsTrivial] [B.IsTrivial] (φ : A ⟶ Rep.res f B) (x : Additive (Abelianization H)) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (groupHomology.map f φ 1)) (((groupHomology.mkH1OfIsTrivial A) x) a) = ((groupHomology.mkH1OfIsTrivial B) ((MonoidHom.toAdditive (Abelianization.map f)) x)) ((Rep.Hom.hom φ) a)

With trivial coefficients, the map on first homology induced by f : H →* G and φ : A ⟶ Res(f)(B) sends the class of x ⊗ a to the class of f x ⊗ φ a.

@[simp]

theorem TauCeti.groupHomology.H1AddEquivOfIsTrivial_map {R G : Type u} [CommRing R] [Group G] {H : Type u} [Group H] {A : Rep R H} {B : Rep R G} [A.IsTrivial] [B.IsTrivial] (f : H →* G) (φ : A ⟶ Rep.res f B) (y : ↑(groupHomology.H1 A)) : (groupHomology.H1AddEquivOfIsTrivial B) ((CategoryTheory.ConcreteCategory.hom (groupHomology.map f φ 1)) y) = (TensorProduct.map (MonoidHom.toAdditive (Abelianization.map f)).toIntLinearMap (↑ℤ (Rep.Hom.hom φ).toLinearMap)) ((groupHomology.H1AddEquivOfIsTrivial A) y)

With trivial coefficients, the identification of first homology with the abelianization tensor the coefficients is natural in both the group and the coefficient module.

theorem MulEquiv.subsingleton_groupHomology {R G : Type u} [CommRing R] [Group G] {H : Type u} [Group H] (e : G ≃* H) {n : ℕ} [Subsingleton ↑(groupHomology (Rep.trivial R H R) n)] : Subsingleton ↑(groupHomology (Rep.trivial R G R) n)

Group homology with trivial coefficients is invariant under isomorphisms of groups: if it vanishes in degree n for H, then it vanishes in degree n for every group G ≃* H.

@[simp]

theorem groupHomology.map_id_nsmul_id {R G : Type u} [CommRing R] [Group G] (A : Rep R G) (c n : ℕ) : map (MonoidHom.id G) (c • CategoryTheory.CategoryStruct.id A) n = c • CategoryTheory.CategoryStruct.id (groupHomology A n)

The map on group homology induced by the multiple c • 𝟙 of the identity of a representation is multiplication by c.

theorem Rep.chainsMap_inclusion_comp_chainsMap_subtype {R G : Type u} [CommRing R] [Group G] (A : Rep R G) {S T : Subgroup G} (h : S ≤ T) : CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap (Subgroup.inclusion h) (A.resInclusionHom h)) (groupHomology.chainsMap T.subtype (CategoryTheory.CategoryStruct.id (res T.subtype A))) = groupHomology.chainsMap S.subtype (CategoryTheory.CategoryStruct.id (res S.subtype A))

The maps of inhomogeneous chains induced by inclusions of subgroups compose: the inclusion of S into T followed by that of T into G is the inclusion of S into G.

theorem Rep.chainsMap_inclusion_comp_chainsMap_subtype_assoc {R G : Type u} [CommRing R] [Group G] (A : Rep R G) {S T : Subgroup G} (h : S ≤ T) {Z : ChainComplex (ModuleCat R) ℕ} (h✝ : groupHomology.inhomogeneousChains A ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap (Subgroup.inclusion h) (A.resInclusionHom h)) (CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap T.subtype (CategoryTheory.CategoryStruct.id (res T.subtype A))) h✝) = CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap S.subtype (CategoryTheory.CategoryStruct.id (res S.subtype A))) h✝

The maps of inhomogeneous chains induced by inclusions of subgroups compose: the inclusion of S into T followed by that of T into G is the inclusion of S into G.

theorem Rep.map_inclusion_comp_map_subtype {R G : Type u} [CommRing R] [Group G] (A : Rep R G) {S T : Subgroup G} (h : S ≤ T) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupHomology.map (Subgroup.inclusion h) (A.resInclusionHom h) n) (groupHomology.map T.subtype (CategoryTheory.CategoryStruct.id (res T.subtype A)) n) = groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (res S.subtype A)) n

The maps on group homology induced by inclusions of subgroups compose: the inclusion of S into T followed by that of T into G is the inclusion of S into G.

theorem Rep.map_inclusion_comp_map_subtype_assoc {R G : Type u} [CommRing R] [Group G] (A : Rep R G) {S T : Subgroup G} (h : S ≤ T) (n : ℕ) {Z : ModuleCat R} (h✝ : groupHomology A n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.map (Subgroup.inclusion h) (A.resInclusionHom h) n) (CategoryTheory.CategoryStruct.comp (groupHomology.map T.subtype (CategoryTheory.CategoryStruct.id (res T.subtype A)) n) h✝) = CategoryTheory.CategoryStruct.comp (groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (res S.subtype A)) n) h✝

The maps on group homology induced by inclusions of subgroups compose: the inclusion of S into T followed by that of T into G is the inclusion of S into G.