The Deligne product of finite linear categories

Let $k$ be a field and let $\mathcal{C},\mathcal{D}$ be finite $k$-linear abelian categories (Finite k-linear abelian categories, k-linear categories and k-linear functors, Abelian category). A Deligne product of $\mathcal{C}$ and $\mathcal{D}$ is a $k$-linear abelian category $\mathcal{C}⊠\mathcal{D}$ together with a functor $⊠:\mathcal{C}\times \mathcal{D}\to \mathcal{C}⊠\mathcal{D}$ (Product category and its projection functors) that is $k$-linear in each variable, right exact in each variable (Left exact and right exact functors), and universal with these properties: for every $k$-linear abelian category $\mathcal{E}$ the restriction functor $G\mapsto G\circ ⊠$, from $k$-linear right exact functors $\mathcal{C}⊠\mathcal{D}\to \mathcal{E}$ with all natural transformations to $k$-linear functors $\mathcal{C}\times \mathcal{D}\to \mathcal{E}$ right exact in each variable with all natural transformations (Functor category $[\mathcal{C},\mathcal{D}]$, Natural transformation and its components), is an equivalence of categories (Equivalence, quasi-inverse, and adjoint equivalence of categories). The universal property is an equivalence of categories, not merely a bijection on functor objects; existence is not asserted here but is supplied by Finite Deligne products exist via tensor-product algebras ↗, and uniqueness means an equivalence respecting the universal bifunctor. Bilinearity is expressed through the action of finite-dimensional $k$-vector spaces that every $k$-linear abelian category carries by the finite copowers of Finite vector-space copowers in a $k$-linear abelian category; the class and size bookkeeping is that of Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why $\mathbf{C}\mathbf{A}\mathbf{T}$ is not formed, and no choice beyond the supplied finite universal-object data is made.

• The definition asserts no existence. It fixes data $(\mathcal{C}⊠\mathcal{D},⊠)$ and a property, and it postulates rather than constructs them; the finite construction and the verification of the equivalence of functor categories are the content of the justified_by supplier Finite Deligne products exist via tensor-product algebras ↗. The universal property is required for every $k$-linear abelian $\mathcal{E}$, including $\mathcal{E}=\mathcal{C}⊠\mathcal{D}$, where restriction also classifies right exact endofunctors together with their transformations.

• Reading the universal property. "With all natural transformations" means the restriction functor is an equivalence between the two categories of functors, so it is full, faithful and essentially surjective: transformations of bifunctors correspond bijectively to natural transformations of the induced functors on $\mathcal{C}⊠\mathcal{D}$, and every $k$-linear right exact functor out of $\mathcal{C}⊠\mathcal{D}$ is induced up to natural isomorphism by such a bifunctor. Uniqueness is uniqueness of the pair up to an equivalence of $k$-linear abelian categories compatible with the universal bifunctors; no literal equality of objects, of categories, or of chosen representatives is asserted.

• Bilinearity and size. $k$-linearity in each variable is expressed by the partial functors $\mathcal{C}\to \mathcal{E}$ and $\mathcal{D}\to \mathcal{E}$ being $k$-linear (k-linear categories and k-linear functors), and every $k$-linear abelian category carries the finite vector-space action $V\odot Y$ supplied by Finite vector-space copowers in a $k$-linear abelian category; right exactness is the exactness convention of Left exact and right exact functors. The sources of functor categories are chosen small representatives of the finite categories, as required by Functor category $[\mathcal{C},\mathcal{D}]$; transport along supplied equivalences is understood. No category of all proper-class-sized functors is formed. The definition performs no selection; the existence theorem states its choice assumption separately.