ct.category theory – Relative cocompletion of a category

$newcommand{k}{mathbf k}$
$newcommand{A}{mathcal A}$
$newcommand{B}{mathcal B}$
$newcommand{C}{mathcal C}$
I’m wondering if anyone knows a reference for the following construction: let $k$ be a field, say, and assume for convenience everything below is $k$-linear, and that every category is essentially small. Hereafter “right exact” means “which commutes with finite colimits”.

Let $A$ be a finitely cocomplete category, and $B$ be an arbitrary (still $k$-linear and essentially small) category. Suppose we are given a functor
iota :A longrightarrow B$$

which I’m happy to assume essentially surjective if that helps. Define the relative $A$-cocompletion of $B$ to be a category $B_A$ equipped with a functor $nu:Brightarrow B_A$, universal for the following properties:

  1. $B_A$ is finitely cocomplete
  2. for any finitely cocomplete $C$, restriction along $nu$ induces a natural equivalence between: (a) right exact functors $B_A rightarrow C$ and (b) just functors $B rightarrow C $ such that the composition $A rightarrow B rightarrow C$ is right exact.

In words, I want to complete $B$ under finite colimit, without duplicating those already existing in the image of $A$. If $A$ is $Vect$ this should just be the free finite cocompletion.

Remember that the finite cocompletion of $B$ is the full-subcategory of (linear) presheaves on $B$ which are finite colimits of representables. I believe $B_A$ is then the full subcategory of that, of those presheaves having the property that their restriction along $iota$ is representable. An example which is an inspiration for this definition is the construction of the category of modules over a monad, from the category of free modules, see e.g. https://ncatlab.org/nlab/show/Eilenberg-Moore+category#AsColimitCompletionOfKleisliCategory.

I’m in the process of checking that myself, and it’s probably just formal, but I would much rather have a reference where it’s done properly.