English
There is a natural isomorphism between the coinvariants of Ind φ A and the restriction-on-Res construction applied to A, observed as a natural isomorphism of functors.
Русский
Существует естественный изоморфизм между коинвариантами Ind φ A и ограничением Res φ применительно к A, рассматриваемый как естественный изоморфизм функторов.
LaTeX
$$$$\mathrm{coinvariantsTensorIndNatIso}_{\phi} : (Ind_φ A) \, ⊗ \, - \, ≅ \, - \, ⊗ \, Res_φ A.$$$$
Lean4
/-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear
isomorphism `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧`
for all `h : H`, `a : A`, and `b : B`. -/
@[simps]
noncomputable def coinvariantsTensorIndIso :
((coinvariantsTensor k H).obj (ind φ A)).obj B ≅ ((coinvariantsTensor k G).obj A).obj ((Action.res _ φ).obj B)
where
hom := coinvariantsTensorIndHom φ A B
inv := coinvariantsTensorIndInv φ A B
hom_inv_id := by
ext h a b
simpa [tensorObj_def, tensorObj, coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom,
Coinvariants.mk_eq_iff] using Coinvariants.mem_ker_of_eq h (IndV.mk φ _ h a ⊗ₜ[k] b) _ <| by simp
inv_hom_id := by
ext
simp [tensorObj_def, tensorObj, coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]