http://www.math.jhu.edu/~eriehl/weighted.pdf
bimoduleの\otimesを定義する。
J:A \otimes B^op \to VとK:B \otimes C^op \to Vに対し、J \otimes K:A \otimes C^op \to Vを次のように定義する。
まず対象の対応は(a,c) \in (A \otimes C^op)_0 = A_0 \times C_0の行き先を、V-functor J(a,-):B \to V; b \mapsto J(a,b)とK(-,c):B^op \to V; b \mapsto K(b,c)にたいし、前に定義したJ(a,-) \otimes_B K(-,c) \in V_0により定める。これを[J \otimes_B K](a,c)と書く。
次に射の対応を定める。
Vの射(A \otimes C^op)( (a,c), (a',c')) \to V([J \otimes_B K](a,c), [J \otimes_B K](a',c'))を自然に定める必要がある。
この射はhomと\otimesの随伴からA(a,a') \otimes C(c,c') \otimes [J \otimes_B K](a,c) \to [J \otimes_B K](a',c')を定めればよい。
J(-,b):A \to Vが定める射J(-,b)_a,a':A(a,a') \to V(J(a,b), J(a',b))から、homと\otimesの随伴によりJ(-,b)_a,a'#:A(a,a') \otimes J(a,b) \to J(a',b)が定まる。
またK(b,-)についても同様にK(b,-)_c,c'#:C(c',c) \otimes K(b,c) \to K(b,c')が定まる。
これらを用いることで、A(a,a') \otimes C(c',c) \otimes J(a,b) \otimes K(b,c) \to J(a',b) \otimes K(b,c')が定まり、これによりcoequalizerの図式に射が定まる。
よってV-funの\otimesの普遍性により、射(A \otimes C^op)( (a,c), (a',c')) \to V([J \otimes_B K](a,c), [J \otimes_B K](a',c'))が定義できる。
これによりV-functor J \otimes_B Kが定義でき、A-C-bimoduleになる。
