Algebraic linear duality on ModuleCat

Basic bundles Mathlib's Module.Dual and LinearMap.dualMap as a contravariant additive functor; Exact proves it exact over a field. Both extend Mathlib/Algebra/Category/ModuleCat/, which is where ModuleCat is defined, so both live here. The derived lift is Algebra/Homology/DerivedCategory/LinearDual.lean.