Internal homs of representations: exactness and change of group

The internal hom Rep.ihom A, sending a representation B to Homₖ(A, B), is an additive functor. When the underlying module of A is projective over k, it is exact: it takes a short exact sequence of representations to a short exact sequence (Rep.shortExact_map_ihom), since exactness of representations is tested on underlying modules and Homₖ(A, -) is exact on k-modules for projective A. Applied to trivial representations, this gives the short exact sequences of coefficients Homₖ(A, N) along which group cohomology with coefficients in an internal hom has its long exact sequence.

For a group homomorphism f : G →* H, an equivariant map φ : A ⟶ Rep.res f B, and a module N with trivial action, precomposition with φ gives an equivariant map Res(f)(Homₖ(B, N)) ⟶ Homₖ(A, N). This is the coefficient map on dual representations used in contravariant change of group for cohomology. Its underlying linear map sends ℓ to ℓ ∘ φ.

instance Rep.instAdditiveIhom_tauCeti {k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep k G) : A.ihom.Additive

The internal hom out of a representation is an additive functor.

theorem Rep.shortExact_map_ihom {k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep k G) [Module.Projective k ↑A] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) : (S.map A.ihom).ShortExact

The internal hom out of a k-projective representation is exact: if the underlying module of A is projective over k, then Homₖ(A, -) takes a short exact sequence of representations 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 to the short exact sequence 0 ⟶ Homₖ(A, X₁) ⟶ Homₖ(A, X₂) ⟶ Homₖ(A, X₃) ⟶ 0.

noncomputable def MonoidHom.ihomTrivialPrecomp {k : Type u} [CommRing k] {G : Type v} {H : Type w} [Group G] [Group H] (f : G →* H) {A : Rep k G} {B : Rep k H} (N : Type t) [AddCommGroup N] [Module k N] (φ : A ⟶ Rep.res f B) : Rep.res f (B.ihom.obj (Rep.trivial k H N)) ⟶ A.ihom.obj (Rep.trivial k G N)

Precomposition with an equivariant map along f, as a morphism between the internal hom representations.

@[simp]

theorem MonoidHom.ihomTrivialPrecomp_hom_apply {k : Type u} [CommRing k] {G : Type v} {H : Type w} [Group G] [Group H] (f : G →* H) {A : Rep k G} {B : Rep k H} (N : Type t) [AddCommGroup N] [Module k N] (φ : A ⟶ Rep.res f B) (ℓ : ↑B →ₗ[k] N) (a : ↑A) : ((Rep.Hom.hom (f.ihomTrivialPrecomp N φ)) ℓ) a = ℓ ((Rep.Hom.hom φ) a)

The internal-hom map along f acts by precomposition.

@[simp]

theorem MonoidHom.ihomTrivialPrecomp_id {k : Type u} [CommRing k] {G : Type v} [Group G] (N : Type t) [AddCommGroup N] [Module k N] (A : Rep k G) : (id G).ihomTrivialPrecomp N (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (A.ihom.obj (Rep.trivial k G N))

The identity on a representation induces the identity on its internal hom into a trivial representation.

theorem MonoidHom.ihomTrivialPrecomp_comp {k : Type u} [CommRing k] {G : Type v} {H : Type w} [Group G] [Group H] (f : G →* H) {A : Rep k G} {B : Rep k H} (N : Type t) [AddCommGroup N] [Module k N] {K : Type u_1} [Group K] (g : H →* K) {C : Rep k K} (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) : (g.comp f).ihomTrivialPrecomp N (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) = CategoryTheory.CategoryStruct.comp ((Rep.resFunctor f).map (g.ihomTrivialPrecomp N ψ)) (f.ihomTrivialPrecomp N φ)

Change of group and precomposition reverse composites of compatible coefficient maps.

theorem MonoidHom.ihomTrivialPrecomp_comp_assoc {k : Type u} [CommRing k] {G : Type v} {H : Type w} [Group G] [Group H] (f : G →* H) {A : Rep k G} {B : Rep k H} (N : Type t) [AddCommGroup N] [Module k N] {K : Type u_1} [Group K] (g : H →* K) {C : Rep k K} (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) {Z : Rep k G} (h : A.ihom.obj (Rep.trivial k G N) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((g.comp f).ihomTrivialPrecomp N (CategoryTheory.CategoryStruct.comp φ (Rep.resMap f ψ))) h = CategoryTheory.CategoryStruct.comp (Rep.resMap f (g.ihomTrivialPrecomp N ψ)) (CategoryTheory.CategoryStruct.comp (f.ihomTrivialPrecomp N φ) h)

Change of group and precomposition reverse composites of compatible coefficient maps.