Change of groups, maps out of tensor coinvariants, and coefficient exactness

Let f : G →* H be a group homomorphism and φ : A ⟶ Res(f)(B) a compatible map of coefficient representations. A morphism v : X ⟶ Res(f)(Y) of G-representations induces the linear map MonoidHom.coinvariantsTensorMap f φ v : (A ⊗ X)_G ⟶ (B ⊗ Y)_H on Mathlib's tensor coinvariants, which sends the class of a ⊗ x to the class of φ a ⊗ v x. It is natural in X and Y.

This is the degreewise construction underlying change of groups on the tensor coinvariants of complexes, MonoidHom.coinvariantsTensorChainMap.

Tensor coinvariants with a projective representation are exact in the other representation (CategoryTheory.ShortComplex.ShortExact.map_coinvariantsTensor_projective). For a free representation the natural identification with finitely supported coefficient families proves exactness. A projective representation is a retract of a free one, so the result holds without any flatness assumption on the coefficient representations. This supplies coefficient long exact sequences for projective-resolution computations of group homology.

For a k-module N, a k-linear map X_G ⟶ N out of the coinvariants is the same as a morphism of representations X ⟶ N to the trivial representation (Rep.coinvariantsAdjunction); Rep.coinvariantsHomLinearEquiv is the k-linear form of this bijection, for representations of any monoid. For a representation A of a group, a morphism of representations A ⊗ X ⟶ N is in turn the same as a morphism X ⟶ Homₖ(A, N) into the internal hom (Rep.MonoidalClosed.linearHomEquiv). The composite k-linear equivalence is Rep.coinvariantsTensorHomLinearEquiv; it sends f to x ↦ (a ↦ f ⟦a ⊗ x⟧) and is natural in all three variables: in X, in N (postcomposition with a linear map corresponds to the induced map of internal homs) and, contravariantly, in A (precomposition with the map induced by f : A ⟶ A' corresponds to Mathlib's MonoidalClosed.pre f). It also commutes with change of group, with precomposition by the compatible coefficient map on the internal-hom side (MonoidHom.coinvariantsTensorHomLinearEquiv_naturality).

Main definitions

• MonoidHom.coinvariantsTensorMap: the map (A ⊗ X)_G ⟶ (B ⊗ Y)_H induced by f, φ and v.
• Rep.coinvariantsHomLinearEquiv: Hom(X_G, N) ≃ₗ[k] Hom_G(X, N).
• Rep.coinvariantsTensorHomLinearEquiv: Hom((A ⊗ X)_G, N) ≃ₗ[k] Hom_G(X, Homₖ(A, N)).

Main results

• MonoidHom.coinvariantsTensorMap_mk: its value on a tensor class.
• MonoidHom.coinvariantsTensorMap_naturality: naturality in the representations.
• Rep.coinvariantsTensorHomLinearEquiv_comp: naturality of Rep.coinvariantsTensorHomLinearEquiv in the representation.
• Rep.coinvariantsTensorHomLinearEquiv_comp_ofHom, Rep.coinvariantsTensorHomLinearEquiv_coinvariantsTensor_map_app_comp: its naturality in the module and in the coefficient representation.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Chapter III, §8 and Section III.2.

The tensor coinvariants functor Rep.coinvariantsTensor is Mathlib's construction by Amelia Livingston.

noncomputable def MonoidHom.coinvariantsTensorMap {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {X : Rep k G} {Y : Rep k H} (v : X ⟶ Rep.res f Y) : ((Rep.coinvariantsTensor k G).obj A).obj X ⟶ ((Rep.coinvariantsTensor k H).obj B).obj Y

Change of groups on tensor coinvariants. For f : G →* H, a compatible coefficient map φ : A ⟶ Res(f)(B) and a morphism v : X ⟶ Res(f)(Y), this is the map (A ⊗ X)_G ⟶ (B ⊗ Y)_H sending the class of a ⊗ x to the class of φ a ⊗ v x.

@[simp]

theorem MonoidHom.coinvariantsTensorMap_mk {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {X : Rep k G} {Y : Rep k H} (v : X ⟶ Rep.res f Y) (a : ↑A) (x : ↑X) : (ModuleCat.Hom.hom (f.coinvariantsTensorMap φ v)) (((A.coinvariantsTensorMk X) a) x) = ((B.coinvariantsTensorMk Y) ((Rep.Hom.hom φ) a)) ((Rep.Hom.hom v) x)

The map sends the class of a ⊗ x to the class of φ a ⊗ v x.

theorem MonoidHom.coinvariantsTensorMap_naturality {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {X X' : Rep k G} {Y Y' : Rep k H} (v : X ⟶ Rep.res f Y) (v' : X' ⟶ Rep.res f Y') (s : X ⟶ X') (t : Y ⟶ Y') (h : CategoryTheory.CategoryStruct.comp v ((Rep.resFunctor f).map t) = CategoryTheory.CategoryStruct.comp s v') : CategoryTheory.CategoryStruct.comp (((Rep.coinvariantsTensor k G).obj A).map s) (f.coinvariantsTensorMap φ v') = CategoryTheory.CategoryStruct.comp (f.coinvariantsTensorMap φ v) (((Rep.coinvariantsTensor k H).obj B).map t)

The map is natural in the representations.

theorem Rep.coinvariantsTensor_obj_map_coinvariantsTensorMk {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) {X Y : Rep k G} (f : X ⟶ Y) (a : ↑A) (x : ↑X) : (ModuleCat.Hom.hom (((coinvariantsTensor k G).obj A).map f)) (((A.coinvariantsTensorMk X) a) x) = ((A.coinvariantsTensorMk Y) a) ((Hom.hom f) x)

The tensor-coinvariants functor acts on tensor classes through the second factor.

noncomputable def Rep.coinvariantsHomLinearEquiv {k G : Type u} [CommRing k] [Monoid G] (N : Type u) [AddCommGroup N] [Module k N] (X : Rep k G) : ((coinvariantsFunctor k G).obj X ⟶ ↧N) ≃ₗ[k] X ⟶ trivial k G N

Maps out of coinvariants are invariant maps: the bijection of the adjunction Rep.coinvariantsAdjunction between k-linear maps X_G ⟶ N and morphisms of representations X ⟶ N to the trivial representation is k-linear.

@[simp]

theorem Rep.coinvariantsHomLinearEquiv_apply_hom_apply {k G : Type u} [CommRing k] [Monoid G] (N : Type u) [AddCommGroup N] [Module k N] {X : Rep k G} (f : (coinvariantsFunctor k G).obj X ⟶ ↧N) (x : ↑X) : (Hom.hom ((coinvariantsHomLinearEquiv N X) f)) x = (CategoryTheory.ConcreteCategory.hom f) ((Representation.Coinvariants.mk X.ρ) x)

The invariant map corresponding to f : X_G ⟶ N is f composed with the projection to the coinvariants.

@[simp]

theorem Rep.coinvariantsHomLinearEquiv_symm_apply_mk {k G : Type u} [CommRing k] [Monoid G] (N : Type u) [AddCommGroup N] [Module k N] {X : Rep k G} (φ : X ⟶ trivial k G N) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom ((coinvariantsHomLinearEquiv N X).symm φ)) ((Representation.Coinvariants.mk X.ρ) x) = (Hom.hom φ) x

The map out of the coinvariants corresponding to φ : X ⟶ N sends the class of x to φ x.

noncomputable def Rep.coinvariantsTensorHomLinearEquiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (N : Type u) [AddCommGroup N] [Module k N] (X : Rep k G) : (((coinvariantsTensor k G).obj A).obj X ⟶ ↧N) ≃ₗ[k] X ⟶ A.ihom.obj (trivial k G N)

Maps out of tensor coinvariants are morphisms into the internal hom: for representations A and X of G and a k-module N, the k-linear maps (A ⊗ X)_G ⟶ N correspond k-linearly to the morphisms of representations X ⟶ Homₖ(A, N), where N carries the trivial action. The map f corresponds to x ↦ (a ↦ f ⟦a ⊗ x⟧) (Rep.coinvariantsTensorHomLinearEquiv_apply_hom_apply_apply).

@[simp]

theorem Rep.coinvariantsTensorHomLinearEquiv_apply_hom_apply_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {N : Type u} [AddCommGroup N] [Module k N] {X : Rep k G} (f : ((coinvariantsTensor k G).obj A).obj X ⟶ ↧N) (x : ↑X) (a : ↑A) : ((Hom.hom ((A.coinvariantsTensorHomLinearEquiv N X) f)) x) a = (CategoryTheory.ConcreteCategory.hom f) (((A.coinvariantsTensorMk X) a) x)

The morphism corresponding to a map f : (A ⊗ X)_G ⟶ N sends x to a ↦ f ⟦a ⊗ x⟧.

@[simp]

theorem Rep.coinvariantsTensorHomLinearEquiv_symm_apply_coinvariantsTensorMk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {N : Type u} [AddCommGroup N] [Module k N] {X : Rep k G} (φ : X ⟶ A.ihom.obj (trivial k G N)) (a : ↑A) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom ((A.coinvariantsTensorHomLinearEquiv N X).symm φ)) (((A.coinvariantsTensorMk X) a) x) = ((Hom.hom φ) x) a

The map corresponding to a morphism φ : X ⟶ Homₖ(A, N) sends ⟦a ⊗ x⟧ to φ x a.

theorem Rep.coinvariantsTensorHomLinearEquiv_comp {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {N : Type u} [AddCommGroup N] [Module k N] {X X' : Rep k G} (g : X ⟶ X') (f : ((coinvariantsTensor k G).obj A).obj X' ⟶ ↧N) : (A.coinvariantsTensorHomLinearEquiv N X) (CategoryTheory.CategoryStruct.comp (((coinvariantsTensor k G).obj A).map g) f) = CategoryTheory.CategoryStruct.comp g ((A.coinvariantsTensorHomLinearEquiv N X') f)

The correspondence is natural in the representation: precomposing a map out of (A ⊗ X')_G with the map induced by g : X ⟶ X' corresponds to precomposing with g.

theorem Rep.coinvariantsTensorHomLinearEquiv_comp_ofHom {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {N : Type u} [AddCommGroup N] [Module k N] {N' : Type u} [AddCommGroup N'] [Module k N'] {X : Rep k G} (f : ((coinvariantsTensor k G).obj A).obj X ⟶ ↧N) (g : N →ₗ[k] N') : (A.coinvariantsTensorHomLinearEquiv N' X) (CategoryTheory.CategoryStruct.comp f (ModuleCat.ofHom g)) = CategoryTheory.CategoryStruct.comp ((A.coinvariantsTensorHomLinearEquiv N X) f) (A.ihom.map ((trivialFunctor k G).map (ModuleCat.ofHom g)))

The correspondence is natural in the module: postcomposing a map out of (A ⊗ X)_G with a linear map g : N →ₗ[k] N' corresponds to postcomposing with the map Homₖ(A, N) ⟶ Homₖ(A, N') induced by g.

theorem Rep.coinvariantsTensorHomLinearEquiv_coinvariantsTensor_map_app_comp {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {N : Type u} [AddCommGroup N] [Module k N] {A' X : Rep k G} (f : A ⟶ A') (φ : ((coinvariantsTensor k G).obj A').obj X ⟶ ↧N) : (A.coinvariantsTensorHomLinearEquiv N X) (CategoryTheory.CategoryStruct.comp (((coinvariantsTensor k G).map f).app X) φ) = CategoryTheory.CategoryStruct.comp ((A'.coinvariantsTensorHomLinearEquiv N X) φ) ((CategoryTheory.MonoidalClosed.pre f).app (trivial k G N))

The correspondence is natural in the coefficient representation: precomposing a map out of (A' ⊗ X)_G with the map (A ⊗ X)_G ⟶ (A' ⊗ X)_G induced by f : A ⟶ A' corresponds to postcomposing with the map Homₖ(A', N) ⟶ Homₖ(A, N) given by precomposition with f.

theorem Rep.coinvariantsTensorFreeLEquiv_naturality {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (α : Type u) [DecidableEq α] : CategoryTheory.CategoryStruct.comp (((coinvariantsTensor k G).map f).app (free k G α)) (B.coinvariantsTensorFreeLEquiv α).toModuleIso.hom = CategoryTheory.CategoryStruct.comp (A.coinvariantsTensorFreeLEquiv α).toModuleIso.hom (ModuleCat.ofHom (Finsupp.mapRange.linearMap (Hom.hom f).toLinearMap))

The free tensor-coinvariant identification is natural in the coefficient representation.

theorem Rep.coinvariantsTensorFreeLEquiv_naturality_assoc {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (α : Type u) [DecidableEq α] {Z : ModuleCat k} (h : ↧(α →₀ ↑B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((coinvariantsTensor k G).map f).app (free k G α)) (CategoryTheory.CategoryStruct.comp (B.coinvariantsTensorFreeLEquiv α).toModuleIso.hom h) = CategoryTheory.CategoryStruct.comp (A.coinvariantsTensorFreeLEquiv α).toModuleIso.hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.mapRange.linearMap (Hom.hom f).toLinearMap)) h)

The free tensor-coinvariant identification is natural in the coefficient representation.

theorem CategoryTheory.ShortComplex.ShortExact.map_coinvariantsTensor_free {k G : Type u} [CommRing k] [Group G] {S : ShortComplex (Rep k G)} (hS : S.ShortExact) (α : Type u) : (S.map ((Rep.coinvariantsTensor k G).flip.obj (Rep.free k G α))).ShortExact

Tensor coinvariants with a free representation preserve short exact coefficient sequences. There is no flatness assumption on the coefficients.

theorem CategoryTheory.ShortComplex.ShortExact.map_coinvariantsTensor_projective {k G : Type u} [CommRing k] [Group G] {S : ShortComplex (Rep k G)} (hS : S.ShortExact) (P : Rep k G) [Projective P] : (S.map ((Rep.coinvariantsTensor k G).flip.obj P)).ShortExact

Tensor coinvariants with a projective representation preserve short exact sequences in the other representation. This is the exactness needed to form coefficient connecting maps when computing group homology from a projective resolution of the trivial representation.

theorem MonoidHom.coinvariantsTensorHomLinearEquiv_naturality {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (N : Type u) [AddCommGroup N] [Module k N] {X : Rep k G} {Y : Rep k H} (v : X ⟶ Rep.res f Y) (ℓ : ((Rep.coinvariantsTensor k H).obj B).obj Y ⟶ ↧N) : (A.coinvariantsTensorHomLinearEquiv N X) (CategoryTheory.CategoryStruct.comp (f.coinvariantsTensorMap φ v) ℓ) = CategoryTheory.CategoryStruct.comp v (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor f).map ((B.coinvariantsTensorHomLinearEquiv N Y) ℓ)) (f.ihomTrivialPrecomp N φ))

The tensor-coinvariant adjunction commutes with change of group: precomposition with the map on tensor classes becomes precomposition with the map of representations and with φ.