English
For f: A →ₗ[R] A', the canonical identifications between maps into a character module and linear composiion with f commute with the rTensor and homEquiv structures; explicitly, a certain diagram involving homEquiv, dual, f.rTensor, and lcomp commutes.
Русский
Для f: A → A' существует каноническое соответствие между отображениями в характеристики и линейными композициями, совместимое с rTensor и homEquiv (диаграмма коммутирует).
LaTeX
$$$\text{homEquiv}^{-1} \circ (\mathrm{dual}(f \otimes B)) \circ \text{homEquiv} = \mathrm{lcomp}_R(\,. , f)$$$
Lean4
/-- Linear maps into a character module are exactly characters of the tensor product.
-/
@[simps!]
noncomputable def homEquiv : (A →ₗ[R] CharacterModule B) ≃ₗ[R] CharacterModule (A ⊗[R] B) :=
.ofLinear uncurry curry (by ext _ z; refine z.induction_on ?_ ?_ ?_ <;> aesop) (by aesop)
