ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge 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.

Natural transformations between tensor composites are governed by bimodule maps

Example

Let $A, B, C$ be unital rings, let $M$ be a $(B, A)$ -bimodule and $N$ a $(C, B)$ -bimodule, with further bimodules $M^{'}, N^{'}$ of the same types ( $(S, R)$ -bimodules and commuting left and right scalar actions), and write $T_{M} = M \otimes_{A} -$ and $T_{N} = N \otimes_{B} -$ . By A commuting outer scalar action descends to a tensor product the outer actions make $N \otimes_{B} M$ a $(C, A)$ -bimodule, and the associativity isomorphism $α_{X} : (N \otimes_{B} M) \otimes_{A} X \to N \otimes_{B} (M \otimes_{A} X)$ of Associativity of tensor products for compatible bimodules identifies the composite functor $T_{N} \circ T_{M}$ with the tensor functor $T_{N \otimes_{B} M}$ of that bimodule.

Consequently natural transformations $T_{N} \circ T_{M} \Rightarrow T_{N^{'}} \circ T_{M^{'}}$ correspond bijectively to $(C, A)$ -bimodule maps $N \otimes_{B} M \to N^{'} \otimes_{B} M^{'}$ : conjugating by the two associativity isomorphisms reduces the classification to Natural transformations between tensor functors are bimodule maps. Each pair of bimodule maps $g : N \to N^{'}$ and $f : M \to M^{'}$ yields the transformation with components

$α_{X}^{'} \circ ((g \otimes f) \otimes 1_{X}) \circ α_{X}^{- 1} : n \otimes (m \otimes x) ⟼ g (n) \otimes (f (m) \otimes x),$

and the classification covers all bimodule maps, not only those of the form $g \otimes f$ : the verification below exhibits a bimodule map between tensor products of bimodules that is not induced by any pair $(g, f)$ .

Facts & Assumptions

Given: Unital rings $A, B, C$ , a $(B, A)$ -bimodule $M$ , a $(C, B)$ -bimodule $N$ , bimodules $M^{'}, N^{'}$ of the same types, and a field $k$ for the witness.

[F1]

The associativity map $α : (N \otimes_{B} M) \otimes_{A} X \to N \otimes_{B} (M \otimes_{A} X)$ , $α ((n \otimes m) \otimes x) = n \otimes (m \otimes x)$ , is a natural isomorphism in $X$ and respects compatible outer actions (Associativity of tensor products for compatible bimodules).

[F2]

Outer actions: if $N$ is a $(C, B)$ -bimodule and $M$ a left $B$ -module, then $N \otimes_{B} M$ carries a left $C$ -action $c (n \otimes m) = (c n) \otimes m$ ; if $N$ is a right $B$ -module and $M$ a $(B, A)$ -bimodule, then $N \otimes_{B} M$ carries a right $A$ -action $(n \otimes m) a = n \otimes (m a)$ ; when both are present they commute, so $N \otimes_{B} M$ is a $(C, A)$ -bimodule. Over a commutative ring $k$ , every left $k$ -module is a $(k, k)$ -bimodule for the same action (A commuting outer scalar action descends to a tensor product, $(S, R)$ -bimodules and commuting left and right scalar actions).

[F3]

Natural transformations are families of components satisfying the naturality equation, and their vertical composites are componentwise and natural (Natural transformation and its components, Identity natural transformation and vertical composition, Vertical composites of natural transformations satisfy naturality).

[F4]

Induced tensor maps satisfy $(f \otimes g) (n \otimes m) = f (n) \otimes g (m)$ and $(f^{'} \circ f) \otimes (g^{'} \circ g) = (f^{'} \otimes g^{'}) \circ (f \otimes g)$ , with $id \otimes id = id$ (Module homomorphisms induce tensor-product homomorphisms functorially).

[F5]

For $(C, A)$ -bimodules $K, K^{'}$ the assignment $f \mapsto (f \otimes 1_{X})$ is a bijection ${Hom}_{C - A} (K, K^{'}) \to Nat (T_{K}, T_{K^{'}})$ compatible with vertical composition (Natural transformations between tensor functors are bimodule maps).

[F6]

$ρ : k \otimes_{k} k \to k$ , $ρ (x \otimes y) = x y$ , is a group isomorphism, so every element of $k \otimes_{k} k$ is detected by its image under $ρ$ (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

[F7]

Every balanced map into an abelian group factors uniquely through the tensor product: a map $\overline{β}$ with $\overline{β} (m \otimes n) = β (m, n)$ exists exactly for balanced $β$ (Universal property of the tensor product for balanced maps into abelian groups).

[F8]

Over a commutative ring, a bilinear map is balanced (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring).

[F9]

The module $k^{2}$ is the direct sum $k \oplus k$ with coordinate inclusions $ȷ_{1}, ȷ_{2}$ ; for every family of maps $k \to P$ there is a unique map $k^{2} \to P$ with the prescribed composites, and the empty case is the zero module (The direct sum of an indexed family of modules, Universal property of a direct sum of modules).

Verification

Given: The data of the Example, and for the witness a field $k$ with $e_{1} = ȷ_{1} (1)$ , $e_{2} = ȷ_{2} (1)$ the standard generators of $k^{2}$ .

1.1F1F2

The associativity maps $α_{X} : (N \otimes_{B} M) \otimes_{A} X \to N \otimes_{B} (M \otimes_{A} X) = (T_{N} \circ T_{M}) (X)$ are natural isomorphisms in $X$ by [F1], and $N \otimes_{B} M$ is a $(C, A)$ -bimodule by [F2], so $α$ is a natural isomorphism of functors $T_{N \otimes_{B} M} \Rightarrow T_{N} \circ T_{M}$ .

1.2F7F8F9

Witness data: take $A = B = C = k$ , $M = N = k^{2}$ , $M^{'} = N^{'} = k$ , all regarded as bimodules via the field action by [F2]. Define $β : k^{2} \times k^{2} \to k$ by $β (m, n) = m_{1} n_{1} + m_{2} n_{2}$ for $m = m_{1} e_{1} + m_{2} e_{2}$ , $n = n_{1} e_{1} + n_{2} e_{2}$ . The map $β$ is bilinear, hence balanced by [F8], so by [F7] there is a unique group homomorphism $\overline{β} : k^{2} \otimes_{k} k^{2} \to k$ with $\overline{β} (m \otimes n) = β (m, n)$ ; it is $k$ -linear because $\overline{β} (c (m \otimes n)) = β (c m, n) = c β (m, n)$ on generators, and $β (e_{i}, e_{j}) = δ_{i j}$ since $e_{1}, e_{2}$ are the standard generators.

2.1F3step 1.1

Conjugation by $α$ and by the corresponding isomorphism $α^{'}$ for the primed bimodules is a bijection from $Nat (T_{N} \circ T_{M}, T_{N^{'}} \circ T_{M^{'}})$ to $Nat (T_{N \otimes_{B} M}, T_{N^{'} \otimes_{B} M^{'}})$ : for $η$ in the first set put $η_{X}^{'} : = (α_{X}^{'})^{- 1} \circ η_{X} \circ α_{X}$ , a natural transformation by [F3], and the assignment $ξ \mapsto (α_{X}^{'} \circ ξ_{X} \circ α_{X}^{- 1})$ is inverse to it by the componentwise cancellation of inverse natural isomorphisms.

3.1F1F3F4step 2.1

A pair of bimodule maps $g : N \to N^{'}$ , $f : M \to M^{'}$ gives the natural transformation $T_{N} \circ T_{M} \Rightarrow T_{N^{'}} \circ T_{M^{'}}$ with components $(g \otimes 1_{M^{'} \otimes_{A} X}) \circ (1_{N} \otimes (f \otimes 1_{X}))$ , equal to $α_{X}^{'} \circ ((g \otimes f) \otimes 1_{X}) \circ α_{X}^{- 1}$ by [F1] and agreement on every $n \otimes (m \otimes x)$ ; this is natural by [F3] and [F4], and under the conjugations of step 2.1 it corresponds to the bimodule map $g \otimes f : N \otimes_{B} M \to N^{'} \otimes_{B} M^{'}$ with $(g \otimes f) (n \otimes m) = g (n) \otimes f (m)$ of [F4].

4.1F5step 2.1step 3.1

By [F5] the natural transformations $T_{N \otimes_{B} M} \Rightarrow T_{N^{'} \otimes_{B} M^{'}}$ correspond bijectively to $(C, A)$ -bimodule maps $N \otimes_{B} M \to N^{'} \otimes_{B} M^{'}$ ; composing with the bijection of step 2.1 classifies the transformations between the composites, and step 3.1 identifies the image of every pair $(g, f)$ .

5.1F4F6step 1.2step 4.1

The element $τ : = ρ^{- 1} \circ \overline{β} \in {Hom}_{k - k} (k^{2} \otimes_{k} k^{2}, k \otimes_{k} k)$ is a bimodule map by [F6] and step 1.2. Suppose that $τ = g \otimes f$ for $k$ -linear $g, f : k^{2} \to k$ , i.e. $τ (m \otimes n) = g (m) \otimes f (n)$ by [F4]; applying the isomorphism $ρ$ of [F6] and evaluating on the four elementary tensors $e_{i} \otimes e_{j}$ gives $g (e_{i}) f (e_{j}) = ρ (τ (e_{i} \otimes e_{j})) = β (e_{i}, e_{j}) = δ_{i j}$ . These four equations are contradictory: $g (e_{1}) f (e_{1}) = 1$ forces $g (e_{1}) \neq 0$ and $f (e_{1}) \neq 0$ , then $g (e_{1}) f (e_{2}) = 0$ forces $f (e_{2}) = 0$ , and then $g (e_{2}) f (e_{2}) = 0$ contradicts $g (e_{2}) f (e_{2}) = 1$ . Hence no pair $(g, f)$ produces $τ$ , while step 4.1 classifies $τ$ as a genuine bimodule map $N \otimes_{B} M \to N^{'} \otimes_{B} M^{'}$ .

6.1step 1.1step 3.1step 4.1step 5.1∎

Steps 1.1 and 4.1 identify $T_{N} \circ T_{M}$ with $T_{N \otimes_{B} M}$ and classify all natural transformations between the composites by all $(C, A)$ -bimodule maps of kernels, step 3.1 gives the components $α_{X}^{'} \circ ((g \otimes f) \otimes 1_{X}) \circ α_{X}^{- 1}$ for pairs $(g, f)$ , and steps 1.2 and 5.1 exhibit a bimodule map not of the form $g \otimes f$ . No basis of an infinite-dimensional space and no presentation is chosen, and no commutativity of the rings is assumed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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

M. Kamensky, Non-Commutative Algebra (BGU course notes, Spring 2017), §5.1, Theorem 5.1.43, Proposition 5.1.40, Lemma 5.1.46, Corollaries 5.1.48-5.1.49 (standard reference, not scraped)
A. Nyman and S. P. Smith, A Generalization of Watts's Theorem: Right Exact Functors on Module Categories, arXiv:0806.0832, Theorem 1.1-1.2, Propositions 3.2-3.3, Lemma 3.4 (standard reference, not scraped)