English
The forward map from the dual-tensor construction to the Hom space is identified with the canonical dualTensorHom map.
Русский
Прямое отображение из двойного тензорного конструктора в пространство Hom идентифицируется с каноническим отображением dualTensorHom.
LaTeX
$$$(dualTensorIsoLinHom ρ_V W).hom.hom = ModuleCat.ofHom (dualTensorHom k V W)$$$
Lean4
/-- Let `S ≤ G` be a subgroup and `A` a `k`-linear `S`-representation. This is the `k`-linear map
`Ind_S^G(A) →ₗ[k] Coind_S^G(A)` sending `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`. -/
noncomputable abbrev indToCoind : ind S.subtype A →ₗ[k] coind S.subtype A :=
Representation.Coinvariants.lift _
(TensorProduct.lift <|
linearCombination _ fun g => LinearMap.codRestrict _ (indToCoindAux A g) fun _ _ _ => by simp)
fun _ => by ext; simp
