theorem FGModuleCat.rightAdjointMate_hom_eq_dualMap (k : Type u) [Field k] {V W : FGModuleCat k} (f : V ⟶ W) : ModuleCat.Hom.hom fᘁ.hom = (ModuleCat.Hom.hom f.hom).dualMap

The right adjoint mate of a morphism f : V ⟶ W in FGModuleCat k coincides with the linear dual map f.dualMap between the dual spaces.