Lean/Mathlib: build a partial adjoint from a perfect pairing, not from explicit equivs

To show a functor i has a left adjoint (Functor.isRightAdjoint_of_leftAdjointObjIsDefined_eq_top + CorepresentableBy), don't compose a chain of LinearEquivs (dual, double dual, adjunction, iso), because naturality then means unfolding all of them. Instead define two linear maps into the same dual space, Hom(X, iY) -> V* and Hom(Z, Y) -> V*, with LinearMap.mk₂ (simp closes the four linearity goals). Prove each injective (a trace ext_left argument) and get bijectivity from LinearMap.injective_iff_surjective_of_finrank_eq_finrank. Take homEquiv := (ofBijective right).trans (ofBijective left).symm; naturality is then 'apply left_injective; ext u; rw [...]' in a few lines. Gotchas: include x in must come before the docstring, not after it; and FiniteDimensional k (X ⟶ Y) for X Y : P.FullSubcategory is not found by instance search, so supply it with LinearEquiv.ofBijective (P.ι.mapLinearMap k) ⟨P.ι.map_injective, P.ι.map_surjective⟩.