English
There are canonical isomorphisms between different constructions of invariants and coinvariants that intertwine Ind, Res and tensor operations; in particular, canonical identifications exist between (Ind φ A) ⊗ B and A ⊗ Res φ B.
Русский
Существуют канонические изоморфизмы между различными конструктами инвариантов и ко-инвариантов, которые сопрягают Ind, Res и тензорные операции; в частности, канонические идентификации между (Ind φ A) ⊗ B и A ⊗ Res φ B.
LaTeX
$$$$ (Ind_\phi A \otimes B) \cong (A \otimes \mathrm{Res}_\phi B). $$$$
Lean4
theorem coinvariantsTensorIndHom_mk_tmul_indVMk (h : H) (x : A) (y : B) :
coinvariantsTensorIndHom φ A B (coinvariantsTensorMk _ _ (IndV.mk φ _ h x) y) =
coinvariantsTensorMk _ _ x (B.ρ h y) :=
by simp [tensorObj_def, ModuleCat.MonoidalCategory.tensorObj, coinvariantsTensorIndHom, coinvariantsTensorMk]
