LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Bilinear right exact functors are determined by their value on the regular modules

Statement

Let $k$ be a field, let $R$ and $S$ be finite-dimensional unital $k$ -algebras (Algebras over a commutative ring, central structure maps, and algebra homomorphisms, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis) with $R - m o d$ and $S - m o d$ the categories of finite-dimensional left modules (Unital left and right modules over a ring; unqualified module means left module), let $E$ be a $k$ -linear abelian category (Abelian category, k-linear categories and k-linear functors), and let $H : R - m o d \times S - m o d \to E$ be $k$ -linear and right exact in each variable (Product category and its projection functors, Left exact and right exact functors). Put $T = R \otimes_{k} S$ (The tensor product of $R$ -algebras has multiplication $(a \otimes b) (a^{'} \otimes b^{'}) = a a^{'} \otimes b b^{'}$ ) and $W = H (R, S)$ . Right multiplications in the two variables make $W$ a right $R$ -module and a right $S$ -module by endomorphisms, with commuting actions, hence a right $T$ -module, and this structure is functorial in $H$ . Then (i) the finite free presentations of $T - m o d$ construct a functor $\overset{ˉ}{H} : T - m o d \to E$ from that right $T$ -module structure, and a canonical natural isomorphism (Natural isomorphism) $\overset{ˉ}{H} (X \otimes_{k} Y) ≅ H (X, Y)$ , natural in $X \in R - m o d$ and $Y \in S - m o d$ , where $X \otimes_{k} Y$ carries the commuting $R$ - and $S$ -actions; and (ii) every natural transformation (Natural transformation and its components) $η : H \Rightarrow H^{'}$ between two such bifunctors is determined by its component $η_{R, S}$ , and $η \mapsto η_{R, S}$ is a bijection onto the compatible maps of right $T$ -modules. The lemma asserts no existence of a Deligne product (existence is established on this page); it identifies how every such bifunctor is computed from its value on $(R, S)$ , The simultaneous selection of presentations and cokernels uses the Axiom of Choice (The Axiom of Choice); morphisms and comparison isomorphisms are independent of those selections.

Module and functor categories are formed on chosen small module representatives. A right $T$ -module object $W$ in $E$ means a $k$ -linear anti-homomorphism $T \to {End}_{E} (W)$ ; no underlying set of elements of $W$ is assumed.

Facts & Assumptions

Given: A field $k$ , finite-dimensional unital $k$ -algebras $R, S$ , the $k$ -algebra $T = R \otimes_{k} S$ (Algebras over a commutative ring, central structure maps, and algebra homomorphisms), a $k$ -linear abelian category $E$ , and a bifunctor $H : R - m o d \times S - m o d \to E$ that is $k$ -linear and right exact in each variable (k-linear categories and k-linear functors, Left exact and right exact functors), where $R - m o d$ and $S - m o d$ are the categories of finite-dimensional left modules (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis); write $W = H (R, S)$ . Assume the Axiom of Choice (The Axiom of Choice). A second such bifunctor $H^{'}$ with $W^{'} = H^{'} (R, S)$ is used in part (ii).

[F1]

For a finite-dimensional $k$ -algebra $A$ and a finite-dimensional left $A$ -module $M$ : $M$ is finitely generated, and every quotient of a free module gives a surjection from a free module (Generated submodule, cyclic and finitely generated modules, module basis and free module, Every module is a quotient of a free module); a finite $k$ -basis generates $M$ over $A$ , its kernel in $A^{n}$ is a submodule of a finite-dimensional module and hence is again finitely generated, so $M$ has a finite free presentation $A^{m} \to A^{n} \to M \to 0$ , and in any such presentation the image of the first map is the kernel of the second.

[F2]

A right $A$ -module carries an action satisfying the right-handed axioms, and $T = R \otimes_{k} S$ is the $k$ -algebra with multiplication $(a \otimes b) (a^{'} \otimes b^{'}) = a a^{'} \otimes b b^{'}$ , so a right action of $T$ is given by a formula on elementary tensors that is well defined and multiplicative (Unital left and right modules over a ring; unqualified module means left module, The tensor product of $R$ -algebras has multiplication $(a \otimes b) (a^{'} \otimes b^{'}) = a a^{'} \otimes b b^{'}$ ).

[F3]

A $k$ -linear functor between $k$ -linear categories is additive on hom-groups, and an additive functor between additive categories preserves finite biproducts; the categories involved here are additive (An additive functor preserves finite biproducts, Abelian category).

[F4]

Morphisms between finite biproducts are given by matrices and compose by matrix multiplication (Morphisms between finite biproducts correspond to matrices, Biproduct).

[F5]

In a category with zero morphisms the cokernel $q : B \to coker (f)$ of $f : A \to B$ satisfies $q f = 0$ and is universal with this property, and in a module category the cokernel is the quotient by the image (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers, Module homomorphism and isomorphism, kernel, image and cokernel).

[F6]

The tensor product of a right module and a left module carries the induced outer action and is functorial in both arguments, with the universal property that balanced bilinear maps factor uniquely through it (A commuting outer scalar action descends to a tensor product, Module homomorphisms induce tensor-product homomorphisms functorially, Universal property of the tensor product for balanced maps into abelian groups).

[F7]

A natural transformation between functors has components satisfying the naturality equation for every morphism, and a natural isomorphism is a natural transformation with a two-sided inverse (Natural transformation and its components, Natural isomorphism).

Proof

technique · direct

1.1givenF2F3F7

Put $ρ (a) = H (r_{a}, 1_{S})$ and $σ (c) = H (1_{R}, r_{c})$ , where $r_{a} (x) = x a$ and $r_{c} (y) = y c$ . These are $k$ -linear in $a, c$ , unital, and satisfy $ρ (a b) = ρ (b) ρ (a)$ and $σ (c c^{'}) = σ (c^{'}) σ (c)$ . The two families commute by functoriality on the product category, so the bilinear map $(a, c) \mapsto σ (c) ρ (a)$ descends through $R \otimes_{k} S$ to a unital anti-homomorphism $τ : T \to End (W)$ . This is the right $T$ -action on $W$ . Naturality shows that $η_{R, S}$ commutes with $τ (t)$ for every $t$ .

2.1step 1.1F3F4

On finite free left $T$ -modules put $K (T^{n}) = W^{n}$ . A left-linear map $φ : T^{m} \to T^{n}$ is determined by $φ (e_{j}) = \sum_{i} p_{i j} e_{i}$ , hence $φ (x)_{i} = \sum_{j} x_{j} p_{i j}$ . Define $K (φ)$ to have $(i, j)$ -entry $τ (p_{i j})$ . If $ψ$ has entries $q_{ℓ i}$ , then $ψ φ$ has entries $\sum_{i} p_{i j} q_{ℓ i}$ , and $τ (p_{i j} q_{ℓ i}) = τ (q_{ℓ i}) τ (p_{i j})$ , proving $K (ψ φ) = K (ψ) K (φ)$ . Identities are preserved, so this is a $k$ -linear functor on free modules.

3.1step 2.1F1F5

For a presentation $P = (T^{m} \overset{δ}{\to} T^{n} \overset{π}{\to} Z \to 0)$ put $K (P) = coker K (δ)$ , with projection $q_{P}$ . A map $u : Z \to Z^{'}$ lifts to $g : T^{n} \to T^{n^{'}}$ by lifting its finitely many generator images through $π^{'}$ . The map $g δ$ lands in $im δ^{'}$ , so lifting the finitely many generator images again gives $g δ = δ^{'} v$ . Thus $q_{P^{'}} K (g) K (δ) = 0$ , and $K (g)$ descends to a map $K (P) \to K (P^{'})$ . Two lifts differ by $δ^{'} v^{'}$ for the same reason, so their descended maps agree. Identity lifts and composites of lifts give identities and composition.

4.1step 3.1F1F5given

Applying step 3.1 to the identity of $Z$ gives canonical mutually inverse comparisons between $K (P)$ and $K (P^{'})$ for any two presentations. On the small module source, choose one presentation per object and one cokernel per resulting map, and put $\overset{ˉ}{H} (Z) = K (P_{Z})$ . These simultaneous choices use The Axiom of Choice, not merely the finite choice used for each lift. For a class-sized definable target, collection first bounds a set of witnesses for this set-indexed family and AC selects them. The lift-independent maps of step 3.1 define a $k$ -linear functor; other choices give a canonical natural isomorphism. Fix these presentation and cokernel data for the construction.

5.1step 4.1F1F6given

Choose presentations $R^{s} \overset{d}{\to} R^{r} \to X \to 0$ and $S^{s^{'}} \overset{d^{'}}{\to} S^{r^{'}} \to Y \to 0$ . Then $X \otimes_{k} Y$ has the presentation $T^{s r^{'}} \oplus T^{r s^{'}} \overset{(d \otimes 1, 1 \otimes d^{'})}{\to} T^{r r^{'}} ⟶ X \otimes_{k} Y ⟶ 0.$ Indeed its last term is the quotient of $R^{r} \otimes_{k} S^{r^{'}}$ by the two images: sending $(\overset{ˉ}{x}, \overset{ˉ}{y})$ to the class of $x \otimes y$ is well defined and bilinear, and the tensor universal property gives an inverse to the induced quotient map. The identifications $R^{a} \otimes_{k} S^{b} ≅ T^{a b}$ preserve the left $T$ -actions.

6.1step 2.1step 3.1step 4.1step 5.1F3F4F5

Right exactness and additivity in each variable identify $H (R^{a}, S^{b})$ with $W^{a b}$ and compute $H (X, Y)$ as the successive cokernel of the maps induced by $d^{'}$ and $d$ . Their entries are precisely the action endomorphisms in step 1.1. These successive cokernels are the cokernel of the pair of maps in step 5.1 after applying $K$ : a map out of $W^{r r^{'}}$ factors through either description exactly when it kills both maps. The universal property [F5] therefore gives $\overset{ˉ}{H} (X \otimes_{k} Y) ≅ H (X, Y)$ . Lifting maps between the presentations shows that both sides use the same matrices; step 3.1 removes dependence on the lifts. The comparison is consequently natural in both variables.

7.1step 1.1step 3.1step 6.1F3F4F5F7

Naturality against biproduct injections and projections determines $η_{R^{a}, S^{b}}$ from $η_{R, S}$ . Naturality against the presentation surjections, which $H, H^{'}$ send to epimorphisms, then determines $η_{X, Y}$ , proving injectivity. Conversely a morphism $f : W \to W^{'}$ commuting with the right $T$ -actions gives componentwise maps $W^{a b} \to W^{' a b}$ commuting with all free-pair matrices. They descend through the successive cokernels of step 6.1. Lifts as in step 3.1 show these components are independent of presentations and natural in $X, Y$ , and the component at $(R, S)$ is $f$ . Thus evaluation is a bijection onto compatible morphisms of right $T$ -module objects.

8.1step 4.1step 6.1step 7.1given∎

Steps 4.1 and 6.1 prove (i), and step 7.1 proves (ii). The construction uses AC for its set-indexed object data; all lift choices are finite and induce unique maps on cokernels. No commutativity of $R$ or $S$ is used.

Depends on

Used by

Finite Deligne products exist via tensor-product algebras Theorem

Dependency tree · two levels

79 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.