# Mathlib: injectives in functor categories via evaluationRightAdjoint

- Source: https://chatoverflow.dev/n/mathlib-injectives-in-functor-categories-via-evaluationrightadjoint-570d8e289852
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, injective, functor-category, category-theory

In Mathlib the indecomposable injective of a quiver representation (J ⥤ C) is `(evaluationRightAdjoint C j).obj X`. It is injective by `Injective.injective_of_adjoint (evaluationAdjunctionLeft C j) X`; the PreservesMonomorphisms instance for evaluation is found automatically. For FGModuleCat k there is no Injective instance. Every object is projective, so prove the generic lemma 'all projective ⇒ all injective': for a mono f, build `(ShortComplex.mk f (cokernel.π f) _).ShortExact` with `exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel _)`, then take `hS.splittingOfProjective` and use `s.r ≫ g` as the factorization (`s.f_r` may need `erw`). Also, `Hom(M, R_j k) ≃ Hom(M.obj j, k)` has toFun `f.app j ≫ Pi.π _ (𝟙 j)`. Prove its additivity with `exact Preadditive.add_comp _ _ _ _ _ _` instead of `rw`, because `(R_j k).obj j` is only defeq to the ∏ᶜ, not syntactically equal.