TheoremStatement: AI-adaptedProof: 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.

Morita equivalence is invertibility of a bimodule

Statement

Let $A$ and $B$ be unital rings, and say that $A$ and $B$ are Morita equivalent when there is an equivalence of categories $A -Mod \to B -Mod$ that is additive.

The following are equivalent: (a) $A$ and $B$ are Morita equivalent; (b) there are bimodules $_{B} M_{A}$ and $_{A} N_{B}$ with isomorphisms $N \otimes_{B} M ≅_{A} A_{A}$ and $M \otimes_{A} N ≅_{B} B_{B}$ of bimodules; (c) there is an invertible 1-cell between $A$ and $B$ in the Morita bicategory of The Morita bicategory of rings and bimodules.
If $F : A -Mod \to B -Mod$ is such an equivalence, then $F ≅ T_{M}$ for $M = F (_{A} A)$ with the $(B, A)$ -bimodule structure $m a = F (r_{a}) (m)$ , its quasi-inverse is $T_{N}$ for $N = G (_{B} B)$ , and the isomorphisms in 1(b) arise from the unit and counit of $F, G$ .
If $A$ and $B$ are Morita equivalent, then for any equivalence $F$ the module $P = F (_{A} A)$ is a small projective generator of $B -Mod$ and $a \mapsto F (r_{a})$ is a ring isomorphism $A ≅ {End}_{B} (P)^{o p}$ (The endomorphism ring ${End}_{R} (M)$ under addition and composition, Module endomorphisms form a ring under pointwise addition and composition); conversely, if $P$ is a left $B$ -module that is a progenerator and if $A ≅ {End}_{B} (P)^{o p}$ is a ring isomorphism making $P$ a $(B, A)$ -bimodule, then $T_{P} = P \otimes_{A} -$ is an equivalence $A -Mod \to B -Mod$ whose right adjoint is ${Hom}_{B} (P, -) ≅ P^{\lor} \otimes_{B} -$ with $P^{\lor} = {Hom}_{B} (P, B)$ ; in particular $P^{\lor}$ is the inverse $(A, B)$ -bimodule of $P$ . No commutativity of the rings is assumed and no choice is used.

Facts & Assumptions

Given: Unital rings $A$ and $B$ ; $A$ and $B$ are Morita equivalent when there is an additive equivalence of categories $A -Mod \to B -Mod$ .

[F1]

In the Morita bicategory of The Morita bicategory of rings and bimodules a 1-cell $A \to B$ is a $(B, A)$ -bimodule $M$ , composition is $N \otimes_{B} M$ , and a 1-cell is invertible exactly when there are bimodules $_{B} M_{A}$ and $_{A} N_{B}$ with isomorphisms $N \otimes_{B} M ≅_{A} A_{A}$ and $M \otimes_{A} N ≅_{B} B_{B}$ of bimodules (The Morita bicategory of rings and bimodules, Bicategories, pseudofunctors, and biequivalences).

[F2]

An equivalence between abelian categories is exact, preserves and reflects all existing colimits, and hence is additive cocontinuous; conversely every additive cocontinuous functor $F : A -Mod \to B -Mod$ is naturally isomorphic to $T_{F (A)}$ , where $F (A)$ carries the $(B, A)$ -bimodule structure $m a = F (r_{a}) (m)$ , and $T_{M} = M \otimes_{A} -$ is additive cocontinuous for every $(B, A)$ -bimodule $M$ (An equivalence between abelian categories is exact, Equivalences preserve, reflect, and create limits and colimits in the isomorphism-invariant sense, Eilenberg-Watts theorem for arbitrary unital rings, Additive cocontinuous module functors and their schematic category).

[F3]

For $(B, A)$ -bimodules $M, M^{'}$ the correspondence $f \mapsto f \otimes 1$ is a bijection ${Hom}_{B - A} (M, M^{'}) ≅ Nat (T_{M}, T_{M^{'}})$ compatible with identities and composition, so an invertible natural transformation corresponds to an isomorphism of bimodules (Natural transformations between tensor functors are bimodule maps).

[F4]

The canonical associativity and unitor isomorphisms give natural isomorphisms $T_{N} \circ T_{M} ≅ T_{N \otimes_{B} M}$ and $T_{A} ≅ 1_{A - M o d}$ , $T_{B} ≅ 1_{B - M o d}$ (Tensoring defines a schematic pseudofunctor with interchange, Associativity of tensor products for compatible bimodules, The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

[F5]

The regular module $_{A} A$ is a small projective generator of $A -Mod$ , and small projective generators are preserved and reflected by equivalences; a left $B$ -module is a small projective generator of $B -Mod$ exactly when it is a progenerator, i.e. finitely generated, projective and a generator (Small projective modules are exactly finitely generated projective modules; the progenerator identification, Equivalences preserve small projective generators, Small projective generators and progenerators).

[F6]

Evaluation at $1$ gives a ring isomorphism ${End}_{A} (_{A} A) ≅ A^{o p}$ , and for a left $R$ -module $M$ the endomorphisms form a unital ring under pointwise addition and composition ( ${End}_{R} (_{R} R) ≅ R^{o p}$ , Module endomorphisms form a ring under pointwise addition and composition, The endomorphism ring ${End}_{R} (M)$ under addition and composition).

[F7]

With supplied definable copower and cokernel assignments, a small projective generator $P$ of a locally small cocomplete abelian category $C$ with $A ≅ {End}_{C} (P)^{o p}$ yields an equivalence $H = C (P, -) : C \to A -Mod$ with a quasi-inverse $L$ (Module reconstruction from a small projective generator with supplied copowers and cokernels, The copower presentation construction is left adjoint to the generator Hom functor).

[F8]

For a $(B, A)$ -bimodule $P$ the tensor functor $T_{P} = P \otimes_{A} -$ is left adjoint to ${Hom}_{B} (P, -)$ with the left $A$ -module structure $(a φ) (p) = φ (p a)$ , and a left adjoint of a functor is unique up to a unique compatible natural isomorphism (Tensor-Hom adjunction for bimodules over arbitrary unital rings, Adjoints are unique up to a unique natural isomorphism compatible with the adjunction data).

[F9]

For a finitely generated projective left $B$ -module $P$ the evaluation map gives a natural isomorphism ${Hom}_{B} (P, -) ≅ {Hom}_{B} (P, B) \otimes_{B} -$ with $P^{\lor} = {Hom}_{B} (P, B)$ , and $P^{\lor}$ is an $(A, B)$ -bimodule when $P$ is a $(B, A)$ -bimodule (The dual-basis isomorphism for a finitely generated projective bimodule).

[F10]

Every equivalence can be equipped as an adjoint equivalence, but the two arbitrary initial isomorphisms witnessing invertibility of a bimodule need not themselves be the unit and counit of that adjoint equivalence (Every equivalence of categories can be equipped as an adjoint equivalence, Equivalence, quasi-inverse, and adjoint equivalence of categories).

Proof

technique · direct

1.1F2F4given

(Set-up.) An additive equivalence $F : A -Mod \to B -Mod$ has a quasi-inverse $G$ , and by [F2] both are additive cocontinuous, so $F ≅ T_{M}$ with $M : = F (_{A} A)$ carrying the $(B, A)$ -bimodule structure $m a = F (r_{a}) (m)$ , and $G ≅ T_{N}$ with $N : = G (_{B} B)$ carrying the $(A, B)$ -bimodule structure. The unit and counit of the equivalence give natural isomorphisms $G \circ F ≅ 1_{A - M o d}$ and $F \circ G ≅ 1_{B - M o d}$ .

1.2F4given

((b) implies (a).) Suppose $_{B} M_{A}$ and $_{A} N_{B}$ satisfy $N \otimes_{B} M ≅_{A} A_{A}$ and $M \otimes_{A} N ≅_{B} B_{B}$ as bimodules. Then [F4] gives natural isomorphisms $T_{N} \circ T_{M} ≅ T_{N \otimes_{B} M} ≅ T_{A} ≅ 1_{A - M o d}$ and $T_{M} \circ T_{N} ≅ T_{B} ≅ 1_{B - M o d}$ , so $T_{M}$ and $T_{N}$ are mutually quasi-inverse functors and $T_{M}$ is an additive equivalence; hence $A$ and $B$ are Morita equivalent.

1.3F2F5F6givenalgebra

(Forward direction of (3).) Let $F$ be an additive equivalence. By [F5] the regular module $_{A} A$ is a small projective generator and $P : = F (_{A} A)$ is again one, hence a progenerator of $B -Mod$ . Full faithfulness of $F$ makes $f \mapsto F (f)$ a ring isomorphism ${End}_{A} (_{A} A) \to {End}_{B} (P)$ , and [F6] identifies ${End}_{A} (_{A} A)$ with $A^{o p}$ through evaluation at $1$ ; composition of these identifications is exactly $a \mapsto F (r_{a})$ , whose image is the right $A$ -action $m a = F (r_{a}) (m)$ of [F2]. Hence $A ≅ {End}_{B} (P)^{o p}$ and $P$ is a $(B, A)$ -bimodule.

1.4F5F7F8F9given

(Converse direction of (3).) Let $P$ be a left $B$ -module that is a progenerator, suppose $A ≅ {End}_{B} (P)^{o p}$ is a ring isomorphism making $P$ a $(B, A)$ -bimodule. By [F5] $P$ is a small projective generator. In $B -Mod$ the finite-support direct sums of copies of $P$ and the quotients by images supply definable copower and cokernel assignments; thus [F7] gives an equivalence $H = {Hom}_{B} (P, -) : B -Mod \to A -Mod$ with quasi-inverse $L$ . By [F8] the tensor functor $T_{P} = P \otimes_{A} -$ is left adjoint to $H$ , so by uniqueness of left adjoints $L ≅ T_{P}$ and $T_{P}$ is an equivalence with right adjoint $H$ ; since $P$ is finitely generated projective as a left $B$ -module, [F9] identifies $H = {Hom}_{B} (P, -)$ with $P^{\lor} \otimes_{B} -$ for the $(A, B)$ -bimodule $P^{\lor} = {Hom}_{B} (P, B)$ .

2.1F3F4step 1.1given

((a) implies (b).) Let $F$ be an additive equivalence with quasi-inverse $G$ , and let $M = F (_{A} A)$ , $N = G (_{B} B)$ be as in step 1.1. Composing the natural isomorphism $G \circ F ≅ 1$ with the comparisons $G \circ F ≅ T_{N} \circ T_{M} ≅ T_{N \otimes_{B} M}$ of [F4] gives an invertible natural transformation $T_{N \otimes_{B} M} ≅ T_{A}$ , which by [F3] corresponds to an isomorphism of $(A, A)$ -bimodules $N \otimes_{B} M ≅_{A} A_{A}$ ; symmetrically $F \circ G ≅ 1$ yields $M \otimes_{A} N ≅_{B} B_{B}$ . Hence a Morita equivalence produces inverse bimodules.

2.2step 1.3step 1.4given

(Proof of (3).) Steps 1.3 and 1.4 prove the two directions: an equivalence sends the regular module to a progenerator whose endomorphism ring is $A^{o p}$ , and conversely a progenerator with $A ≅ {End}_{B} (P)^{o p}$ has $T_{P}$ as an equivalence with right adjoint ${Hom}_{B} (P, -) ≅ P^{\lor} \otimes_{B} -$ , so $P^{\lor}$ is the inverse $(A, B)$ -bimodule of $P$ .

3.1F1step 1.2step 2.1given

(Proof of (1).) Step 1.2 gives (b) $\Rightarrow$ (a) and step 2.1 gives (a) $\Rightarrow$ (b), so (a) and (b) are equivalent; condition (c) is the same statement in the language of the Morita bicategory, where an invertible 1-cell is one admitting a two-sided inverse up to invertible 2-cells, which are exactly the bimodule isomorphisms of (b) by [F1]. Hence (a), (b), (c) are equivalent.

3.2step 1.1step 2.1given

(Proof of (2).) Let $F$ be an equivalence. Step 1.1 exhibits $F ≅ T_{M}$ with $M = F (_{A} A)$ and the $(B, A)$ -bimodule structure $m a = F (r_{a}) (m)$ , and its quasi-inverse $G ≅ T_{N}$ with $N = G (_{B} B)$ ; step 2.1 derives the two bimodule isomorphisms from the unit and counit of the equivalence. This is exactly assertion (2).

4.1F10step 3.1step 3.2step 2.2∎

Steps 3.1, 3.2 and 2.2 prove the three assertions; if triangle identities are wanted, replace the equivalence by an adjoint equivalence as in [F10] — the initial bimodule isomorphisms of step 2.1 need not themselves be the unit and counit of that adjoint equivalence. No commutativity of the rings is assumed and no choice is used.

Depends on

Used by

Dependency tree · two levels

96 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

W. Crawley-Boevey, Noncommutative Algebra, §3.12, Theorem (Morita) (i)-(iii) and examples (i)-(ii), printed pp.68-69 (standard reference, not scraped)
nLab, Morita equivalence, Classical Morita theorem (bimodule inverses; R = End of a finitely generated projective generator) (standard reference, not scraped)
N. Johnson and D. Yau, 2-Dimensional Categories, Example 6.3.6 (M is a left adjoint iff finitely generated projective; Hom_R(M,R) is its right adjoint), together with the tensor-Hom adjunction of the HA-25 page (standard reference, not scraped)