Naturality of the connecting map in group homology

Mathlib's groupHomology.δ is the connecting map Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁), j + 1 = i, of the long exact sequence of a short exact sequence X of G-representations. This file shows it is natural with respect to change of group: given f : G →* H, a short exact sequence Y of H-representations, and a morphism Φ : X ⟶ Res_f Y of short complexes, the square

Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) ↓ ↓ Hᵢ(H, Y₃) ⟶ Hⱼ(H, Y₁)

formed by the two connecting maps and the change-of-group maps groupHomology.map f Φ.τᵢ commutes.

Taking f to be the identity recovers naturality of δ for a morphism of short exact sequences of G-representations. The general case is what compares connecting maps across a change of group, for instance across Shapiro's isomorphism, whose inverse is the change-of-group map along a subgroup inclusion (TauCeti.groupHomology.indIso_inv).

Main definitions

• TauCeti.groupHomology.chainsMapShortComplex: the morphism of short complexes of chain complexes induced by a morphism X ⟶ Res_f Y along f : G →* H; its components are groupHomology.chainsMap f Φ.τᵢ (chainsMapShortComplex_τ₁ and its siblings).

Main results

• TauCeti.groupHomology.δ_naturality: the connecting map of group homology commutes with change-of-group maps.

noncomputable def TauCeti.groupHomology.chainsMapShortComplex {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (Φ : X ⟶ Y.map (Rep.resFunctor f)) : X.map (groupHomology.chainsFunctor k G) ⟶ Y.map (groupHomology.chainsFunctor k H)

A morphism Φ : X ⟶ Res_f Y of short complexes of representations, along a group homomorphism f : G →* H, induces a morphism between the short complexes of inhomogeneous chain complexes, given in each position by groupHomology.chainsMap f.

@[simp]

theorem TauCeti.groupHomology.chainsMapShortComplex_τ₁ {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (Φ : X ⟶ Y.map (Rep.resFunctor f)) : (chainsMapShortComplex f Φ).τ₁ = groupHomology.chainsMap f Φ.τ₁

The first component of chainsMapShortComplex f Φ is the chain map induced by the pair (f, Φ.τ₁).

@[simp]

theorem TauCeti.groupHomology.chainsMapShortComplex_τ₂ {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (Φ : X ⟶ Y.map (Rep.resFunctor f)) : (chainsMapShortComplex f Φ).τ₂ = groupHomology.chainsMap f Φ.τ₂

The second component of chainsMapShortComplex f Φ is the chain map induced by the pair (f, Φ.τ₂).

@[simp]

theorem TauCeti.groupHomology.chainsMapShortComplex_τ₃ {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (Φ : X ⟶ Y.map (Rep.resFunctor f)) : (chainsMapShortComplex f Φ).τ₃ = groupHomology.chainsMap f Φ.τ₃

The third component of chainsMapShortComplex f Φ is the chain map induced by the pair (f, Φ.τ₃).

theorem TauCeti.groupHomology.δ_naturality {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (hX : X.ShortExact) (hY : Y.ShortExact) (Φ : X ⟶ Y.map (Rep.resFunctor f)) (i j : ℕ) (hij : j + 1 = i) : CategoryTheory.CategoryStruct.comp (groupHomology.δ hX i j hij) (groupHomology.map f Φ.τ₁ j) = CategoryTheory.CategoryStruct.comp (groupHomology.map f Φ.τ₃ i) (groupHomology.δ hY i j hij)

The connecting map of group homology is natural with respect to change of group. For short exact sequences X of G-representations and Y of H-representations, and a morphism Φ : X ⟶ Res_f Y along f : G →* H, the connecting maps commute with the change-of-group maps groupHomology.map f.

theorem TauCeti.groupHomology.δ_naturality_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (hX : X.ShortExact) (hY : Y.ShortExact) (Φ : X ⟶ Y.map (Rep.resFunctor f)) (i j : ℕ) (hij : j + 1 = i) {Z : ModuleCat k} (h : groupHomology Y.X₁ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.δ hX i j hij) (CategoryTheory.CategoryStruct.comp (groupHomology.map f Φ.τ₁ j) h) = CategoryTheory.CategoryStruct.comp (groupHomology.map f Φ.τ₃ i) (CategoryTheory.CategoryStruct.comp (groupHomology.δ hY i j hij) h)

The connecting map of group homology is natural with respect to change of group. For short exact sequences X of G-representations and Y of H-representations, and a morphism Φ : X ⟶ Res_f Y along f : G →* H, the connecting maps commute with the change-of-group maps groupHomology.map f.