English
There is a natural isomorphism between Ind φ A ⊗ B and the corresponding Res φ B when transported along the functor equivalences; concretely one obtains a natural isomorphism of underlying module structures.
Русский
Существует естественный изоморфизм между Ind φ A ⊗ B и соответствующим Res φ B в рамках эквивалентностей функторов; явно получаем естественный изоморфизм основных структур модулей.
LaTeX
$$$$\mathrm{Ind}_\phi(A) \otimes B \cong A \otimes \mathrm{Res}_\phi(B).$$$$
Lean4
/-- Given a group hom `φ : G →* H` and `A : Rep k G`, the functor `Rep k H ⥤ ModuleCat k` sending
`B ↦ (Ind(φ)(A) ⊗ B))_H` is naturally isomorphic to the one sending `B ↦ (A ⊗ Res(φ)(B))_G`. -/
@[simps! hom_app inv_app]
noncomputable def coinvariantsTensorIndNatIso :
(coinvariantsTensor k H).obj (ind φ A) ≅ Action.res _ φ ⋙ (coinvariantsTensor k G).obj A :=
NatIso.ofComponents (fun B => coinvariantsTensorIndIso φ A B) fun {X Y} f =>
by
ext
simp [tensorObj_def, tensorObj, coinvariantsTensorIndHom, coinvariantsTensorMk, whiskerLeft_def,
ModuleCat.MonoidalCategory.whiskerLeft, hom_comm_apply]
