English
Given a linear map f: A →ₗ[R] B, the dual map f⋆: CharacterModule(B) →ₗ[R] CharacterModule(A) is defined by (f⋆)(L) = L ∘ f for L ∈ CharacterModule(B).
Русский
Для линейного отображения f: A → B задаётся дуальное отображение f⋆: CharacterModule(B) → CharacterModule(A) таким образом, что (f⋆)(L) = L ∘ f.
LaTeX
$$$\mathrm{dual}(f): \mathrm{CharacterModule}(B) \to \mathrm{CharacterModule}(A),\quad (\mathrm{dual}(f))(L) = L \circ f$$$
Lean4
/-- Given an abelian group homomorphism `f : A → B`, `f⋆(L) := L ∘ f` defines a linear map
from `B⋆` to `A⋆`.
-/
@[simps]
def dual (f : A →ₗ[R] B) : CharacterModule B →ₗ[R] CharacterModule A
where
toFun L := L.comp f.toAddMonoidHom
map_add' := by aesop
map_smul' r c := by ext x; exact congr(c $(f.map_smul r x)).symm
