CorollaryStatement: 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.

Finite Eilenberg–Watts is a biequivalence

Statement

Throughout, a bimodule over $k$ -algebras means a $k$ -vector space with $k$ -bilinear commuting actions and agreeing scalar actions: $(c 1_{B}) m = m (c 1_{A}) = c m$ for $c \in k$ in a $(B, A)$ -bimodule. This compatibility is an additional requirement beyond the ring-bimodule definition $(S, R)$ -bimodules and commuting left and right scalar actions.

For assertions forming categories of functors, fix a set of allowed finite-dimensional $k$ -vector space structures containing $k$ and the underlying spaces of the algebras considered, and closed under finite biproducts, subspaces, quotients, $k$ -tensor products, $k$ -duals and spaces of linear maps. Allow every compatible algebra, module and bimodule structure on these spaces. The resulting module categories are small, so their functors and natural transformations are set-coded as required by Functor category $[C, D]$ . The objectwise formulas apply without this size restriction; no category of proper-class functors is asserted.

Let $A, B$ range over finite-dimensional unital algebras over a field $k$ , and consider the assignment $Φ (A) = A - m o d$ , $Φ (M) = T_{M} = M \otimes_{A} -$ , $Φ (f) = f \otimes 1$ on finite-dimensional bimodules and bimodule maps. (i) For all $A, B$ the assignment $M \mapsto T_{M}$ is an equivalence of categories between finite-dimensional $(B, A)$ -bimodules with bimodule maps and $k$ -linear right exact functors $A - m o d \to B - m o d$ with all natural transformations, so it is full, faithful and essentially surjective. (ii) The composition and unit comparisons of the pseudofunctor Tensoring defines a schematic pseudofunctor with interchange restrict to finite-dimensional algebras and finite-dimensional modules: the associativity isomorphism $N \otimes_{B} (M \otimes_{A} -) ≅ (N \otimes_{B} M) \otimes_{A} -$ with components $N \otimes_{B} (M \otimes_{A} X) ≅ (N \otimes_{B} M) \otimes_{A} X$ and the inverse unit isomorphism $X ≅ A \otimes_{A} X$ are natural isomorphisms of finite-dimensional modules, and the pseudofunctor coherence equations remain satisfied. Consequently these data define a biequivalence from the bicategory of finite-dimensional algebras, finite-dimensional bimodules and bimodule maps to the 2-category of finite-dimensional module categories, $k$ -linear right exact functors and natural transformations. No commutativity and no choice are used.

Facts & Assumptions

Given: A field $k$ and the assignment $Φ$ on finite-dimensional unital $k$ -algebras, finite-dimensional bimodules and bimodule maps described in the statement.

[F1]

For finite-dimensional unital $k$ -algebras $A, B$ , the assignment $M \mapsto T_{M}$ is an equivalence of categories between finite-dimensional $(B, A)$ -bimodules with bimodule maps and $k$ -linear right exact functors $A - m o d \to B - m o d$ with all natural transformations; in particular it is full and faithful with $Nat (T_{M}, T_{M^{'}}) ≅ {Hom}_{B - A} (M, M^{'})$ and essentially surjective (Finite Eilenberg–Watts for right exact linear functors, Equivalence, quasi-inverse, and adjoint equivalence of categories, Natural transformation and its components).

[F2]

The explicit tensor comparison maps in Tensoring defines a schematic pseudofunctor with interchange have composition comparison $T_{N} \circ T_{M} ≅ T_{N \otimes_{B} M}$ built from the associativity isomorphism $N \otimes_{B} (M \otimes_{A} X) ≅ (N \otimes_{B} M) \otimes_{A} X$ , identity comparison the inverse unit isomorphism $X ≅ A \otimes_{A} X$ , and coherence given by the pentagon and triangle diagrams; horizontal composition corresponds to tensoring bimodule maps (Tensoring defines a schematic pseudofunctor with interchange, The Morita bicategory of rings and bimodules, Bicategories, pseudofunctors, and biequivalences).

[F3]

The finite-dimensional module categories $A - m o d$ are well formed and the right exact $k$ -linear functors between them with all natural transformations form a strict 2-category, with composition of functors and identity transformations as structure (Finite-dimensional module categories satisfy the intrinsic finiteness conditions, Strict 2-category, Functor category $[C, D]$ , Natural transformation and its components, Left exact and right exact functors); the restriction of the Morita bicategory to finite-dimensional algebras and finite-dimensional bimodules is a bicategory, since tensor products of finite-dimensional bimodules over finite-dimensional algebras are again finite-dimensional and the associators and unitors are the same isomorphisms (The Morita bicategory of rings and bimodules, $(S, R)$ -bimodules and commuting left and right scalar actions).

[F4]

A pseudofunctor is a biequivalence when each local functor on hom-categories is an equivalence of categories and every object of the target is equivalent to $F Y$ for some object $Y$ of the source (Bicategories, pseudofunctors, and biequivalences).

Proof

technique · direct

1.1F1

(i) By [F1] the assignment $M \mapsto T_{M}$ on finite-dimensional $(B, A)$ -bimodules is full and faithful and essentially surjective onto the $k$ -linear right exact functors $A - m o d \to B - m o d$ , so it is an equivalence of categories for the given $A, B$ .

1.2F2F3

(ii, restriction of the pseudofunctor.) Let $A, B, C$ be finite-dimensional unital $k$ -algebras and let $M$ be a finite-dimensional $(B, A)$ -bimodule, $N$ a finite-dimensional $(C, B)$ -bimodule. Use the explicit maps of [F2]: the comparison 2-cells of $Φ$ are the associativity isomorphism $N \otimes_{B} (M \otimes_{A} X) ≅ (N \otimes_{B} M) \otimes_{A} X$ and the inverse unit isomorphism $X ≅ A \otimes_{A} X$ ; for finite-dimensional $X$ all objects occurring are quotients of finite tensor products of finite-dimensional spaces, hence finite-dimensional, and tensoring finite-dimensional bimodules over finite-dimensional algebras gives a finite-dimensional bimodule, so the source and target data together with these comparisons lie in the smaller bicategory and 2-category of [F3]. The coherence equations hold directly: on an elementary tensor every associativity path sends each nested tensor to the same reassociation of its factors, and every unit path multiplies the same adjacent unit factor. Elementary tensors generate the iterated tensor products, so equality there proves the required equations. Horizontal composition corresponds to tensoring bimodule maps under these comparisons, since both send $n \otimes m \otimes x$ to $g (n) \otimes f (m) \otimes x$ . The set-sized construction here uses the supplier's explicit maps and componentwise equations.

2.1F3F4step 1.1step 1.2

(ii, biequivalence.) The restricted assignment is a pseudofunctor by step 1.2. Its local functor at $(A, B)$ is the equivalence of step 1.1, so every local functor is an equivalence of categories; and every object $A - m o d$ of the target is $Φ (A)$ for the finite-dimensional algebra $A$ itself, so essential surjectivity holds trivially. Hence by [F4] the restriction is a biequivalence between the bicategory of finite-dimensional algebras, finite-dimensional bimodules and bimodule maps and the 2-category of finite-dimensional module categories, $k$ -linear right exact functors and natural transformations.

3.1step 1.1step 1.2step 2.1given∎

Steps 1.1 and 2.1 prove (i) and (ii). All algebras, bimodules, modules and comparison isomorphisms occurring above are finite-dimensional, no commutativity of any ring was used, and no choice is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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.

Sources

Etingof, Gelaki, Nikshych, Ostrik, Tensor Categories, §1.8 (Definitions 1.8.1–1.8.6, Proposition 1.8.10, Corollary 1.8.11, Remark 1.8.7), printed pp.9–11 (standard reference, not scraped)
Fuchs, Schaumann, Schweigert, Eilenberg–Watts calculus for finite categories and a bimodule Radford S^4 theorem, arXiv:1612.04561v3, §2.1 (Lemma 2.1, Lemma 2.2, Corollary 2.3) (standard reference, not scraped)