noncomputable def doubleDualFunctor (k : Type u) [Field k] : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)

The double-dual endofunctor on FGModuleCat k, sending V to (V*)* and acting on morphisms by f ↦ f.dualMap.dualMap.

noncomputable def doubleDualNatIso (k : Type u) [Field k] : CategoryTheory.Functor.id (FGModuleCat k) ≅ doubleDualFunctor k

The natural isomorphism between the identity functor on FGModuleCat k and the double-dual functor, given componentwise by the canonical evaluation map.