LemmaStatement: Literature-sourcedProof: 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.

Tensor-Hom adjunction for bimodules over arbitrary unital rings

Statement

Let $A$ and $B$ be unital rings, let $M$ be a $(B, A)$ -bimodule, let $X$ be a left $A$ -module and let $Y$ be a left $B$ -module. Then ${Hom}_{B} (M, Y)$ is a left $A$ -module under

$(a φ) (m) = φ (m a),$

and currying

$Θ : {Hom}_{B} (M \otimes_{A} X, Y) \to {Hom}_{A} (X, {Hom}_{B} (M, Y)), Θ (F) (x) = [m \mapsto F (m \otimes x)],$

is a bijection, natural in $X$ and $Y$ , whose inverse sends $φ$ to the $B$ -linear map determined on elementary tensors by $Ψ (φ) (m \otimes x) = φ (x) (m)$ . The unit $η_{X} : X \to {Hom}_{B} (M, M \otimes_{A} X)$ , $η_{X} (x) (m) = m \otimes x$ , and counit $ε_{Y} : M \otimes_{A} {Hom}_{B} (M, Y) \to Y$ , $ε_{Y} (m \otimes φ) = φ (m)$ , satisfy the triangle identities of Adjunction by unit, counit, and the triangle identities. Consequently $T_{M} = M \otimes_{A} -$ is left adjoint to ${Hom}_{B} (M, -)$ . No commutativity is assumed and no choice is used.

Facts & Assumptions

Given: Unital rings $A, B$ , a $(B, A)$ -bimodule $M$ , a left $A$ -module $X$ and a left $B$ -module $Y$ .

[F1]

Module laws: $m (a + a^{'}) = m a + m a^{'}$ , $(m a) a^{'} = m (a a^{'})$ , $m 1 = m$ for the right $A$ -module $M$ , and dually for left modules over $A$ and $B$ (Unital left and right modules over a ring; unqualified module means left module).

[F2]

In a $(B, A)$ -bimodule the two actions commute: $b (m a) = (b m) a$ for all $b \in B$ , $m \in M$ , $a \in A$ ( $(S, R)$ -bimodules and commuting left and right scalar actions).

[F3]

${Hom}_{B} (M, Y)$ is an abelian group under pointwise addition, and postcomposition and precomposition by module maps are group homomorphisms (The abelian group ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition).

[F4]

An $A$ -balanced map $b : M \times X \to Z$ is additive in each variable and satisfies $b (m a, x) = b (m, a x)$ (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring).

[F5]

Every balanced map $M \times X \to Z$ into an abelian group factors uniquely as $\overline{b} \circ τ$ through the universal balanced map $τ (m, x) = m \otimes x$ (Universal property of the tensor product for balanced maps into abelian groups).

[F6]

For a $(B, A)$ -bimodule $M$ and a left $A$ -module $X$ there is a unique left $B$ -module structure on $M \otimes_{A} X$ with $b (m \otimes x) = (b m) \otimes x$ (A commuting outer scalar action descends to a tensor product).

[F7]

Module maps induce maps on tensor products, functorially: $id \otimes id = id$ and $(f^{'} \circ f) \otimes (g^{'} \circ g) = (f^{'} \otimes g^{'}) \circ (f \otimes g)$ (Module homomorphisms induce tensor-product homomorphisms functorially).

[F8]

An adjunction $F ⊣ G$ is a unit and counit satisfying the triangle identities (Adjunction by unit, counit, and the triangle identities).

Proof

technique · direct

1.1F1F2F3

For $a \in A$ and $φ \in {Hom}_{B} (M, Y)$ the map $m \mapsto φ (m a)$ is additive and $B$ -linear, since $φ (b (m a)) = φ ((b m) a) = b φ (m a)$ by [F2] and $B$ -linearity of $φ$ . Hence $(a φ) (m) : = φ (m a)$ defines an element of ${Hom}_{B} (M, Y)$ , and the resulting action satisfies the left $A$ -module axioms, inherited pointwise from the right $A$ -module laws of $M$ and the group structure of ${Hom}_{B} (M, Y)$ : $(a + a^{'}) φ = a φ + a^{'} φ$ , $(a a^{'}) φ = a (a^{'} φ)$ , $1 φ = φ$ and $a (φ + ψ) = a φ + a ψ$ .

1.2F1F3F6

For $F \in {Hom}_{B} (M \otimes_{A} X, Y)$ set $Θ (F) (x) (m) : = F (m \otimes x)$ . For fixed $x$ the map $m \mapsto F (m \otimes x)$ is additive and $B$ -linear, because $b (m \otimes x) = (b m) \otimes x$ by [F6] and $F$ is $B$ -linear, so $Θ (F) (x) \in {Hom}_{B} (M, Y)$ ; moreover $Θ (F) (x + x^{'}) = Θ (F) (x) + Θ (F) (x^{'})$ and $Θ (F) (a x) = a Θ (F) (x)$ because $m \otimes (a x) = (m a) \otimes x$ , so $Θ (F) \in {Hom}_{A} (X, {Hom}_{B} (M, Y))$ , and $Θ$ is additive.

2.1F1F3F4F5F6step 1.1

For $φ \in {Hom}_{A} (X, {Hom}_{B} (M, Y))$ the pairing $u (m, x) : = φ (x) (m)$ is balanced: it is additive in each variable, and $u (m a, x) = φ (x) (m a) = (a φ (x)) (m) = φ (a x) (m) = u (m, a x)$ by step 1.1 and $A$ -linearity of $φ$ . By [F5] it induces a unique group homomorphism $Ψ (φ) : M \otimes_{A} X \to Y$ with $Ψ (φ) (m \otimes x) = φ (x) (m)$ , and $Ψ (φ)$ is $B$ -linear because $Ψ (φ) (b (m \otimes x)) = φ (x) (b m) = b (φ (x) (m))$ by [F6] and $B$ -linearity of each $φ (x)$ .

2.2F3F7step 1.2

Naturality: for $A$ -linear $g : X^{'} \to X$ one has $Θ (F \circ (1_{M} \otimes g)) (x^{'}) (m) = F (m \otimes g (x^{'})) = Θ (F) (g (x^{'})) (m)$ , so $Θ$ is natural in $X$ ; for $B$ -linear $h : Y \to Y^{'}$ one has $Θ (h \circ F) (x) (m) = h (F (m \otimes x)) = h_{*} (Θ (F) (x)) (m)$ , so $Θ$ is natural in $Y$ .

3.1F5step 1.2step 2.1

$Θ$ and $Ψ$ are mutually inverse: $Θ (Ψ (φ)) (x) (m) = Ψ (φ) (m \otimes x) = φ (x) (m)$ , and $Ψ (Θ (F))$ agrees with $F$ on every elementary tensor, so the two $B$ -linear maps are equal by the uniqueness clause of [F5].

4.1F5F7step 1.2step 2.1step 3.1

Put $η_{X} : = Θ (1_{M \otimes_{A} X})$ , so $η_{X} (x) (m) = m \otimes x$ , and $ε_{Y} : = Ψ (1_{{Hom}_{B} (M, Y)})$ , so $ε_{Y} (m \otimes φ) = φ (m)$ . The triangle identities hold: $ε_{M \otimes_{A} X} \circ (1_{M} \otimes η_{X})$ and $1_{M \otimes_{A} X}$ agree on every elementary tensor, since $ε_{M \otimes_{A} X} (m \otimes η_{X} (x)) = η_{X} (x) (m) = m \otimes x$ ; and ${Hom}_{B} (M, ε_{Y}) \circ η_{{Hom}_{B} (M, Y)}$ and the identity agree on every $φ$ , since $ε_{Y} (m \otimes φ) = φ (m)$ for all $m$ .

5.1F8step 4.1∎

By step 4.1 the functors $T_{M} = M \otimes_{A} -$ and ${Hom}_{B} (M, -)$ carry a unit and counit satisfying the triangle identities, so $T_{M}$ is left adjoint to ${Hom}_{B} (M, -)$ in the sense of [F8].

Depends on

Used by

Dependency tree · two levels

19 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)