LemmaStatement: 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 kernels: explicit end and coend universal maps

Statement

Let $A, B$ be finite $k$ -linear abelian categories, identified with chosen small models $R - m o d$ and $S - m o d$ for finite-dimensional $k$ -algebras, and let $M$ be a finite $(B, A)$ -bimodule with $F = Φ^{l} (M) = {Hom}_{A} (M^{*}, -) \in Lex (A, B)$ and $G = Φ^{r} (M) = M \otimes_{A} - \in Rex (A, B)$ (Categorical Eilenberg–Watts equivalences for finite linear categories). Then (i) the coend $\int^{a \in A} \overset{ˉ}{a} ⊠ F (a)$ (The end and the coend of a functor $C^{o p} \times C \to D$ , Dinatural transformation between functors on $C^{o p} \times C$ , Wedges and cowedges, and the categories they form) exists; computed in the bimodule model it is the coend of $a \mapsto F (a) \otimes_{k} a^{*}$ , and the explicit cowedge $ρ_{a} : F (a) \otimes_{k} a^{*} \to M$ , $ρ_{a} (f \otimes λ) = λ \circ f \in M ≅ (M^{*})^{*}$ (Linear functionals and the algebraic dual $V^{*} = L (V, F)$ , Linear map between vector spaces over the same field, Vector space over a field), is universal: every cowedge $t$ into $Z$ factors uniquely as $t^{'} \circ ρ$ with $t^{'} : M \to Z$ . (ii) The end $\int_{a \in A} \overset{ˉ}{a} ⊠ G (a)$ exists; computed in the model it is the end of $a \mapsto G (a) \otimes_{k} a^{*} ≅ {Hom}_{k} (a, G (a))$ , with universal wedge $ω_{a} : M \to {Hom}_{k} (a, G (a))$ , $ω_{a} (m) (x) = m \otimes x$ , and the symmetric universal property for wedges. (iii) The resulting assignments $Ψ^{l} (F) = \int^{a} \overset{ˉ}{a} ⊠ F (a)$ and $Ψ^{r} (G) = \int_{a} \overset{ˉ}{a} ⊠ G (a)$ are functorial in $F$ and $G$ (a natural transformation $η : F \Rightarrow F^{'}$ induces a morphism of the universal cowedges, Natural transformation and its components, A natural transformation of functors induces a unique morphism of their ends and of their coends) and satisfy $Ψ^{l} Φ^{l} ≅ 1$ and $Ψ^{r} Φ^{r} ≅ 1$ as natural isomorphisms (Natural isomorphism, An end and a coend are unique up to a unique isomorphism compatible with every component); hence they are quasi-inverse to $Φ^{l}, Φ^{r}$ . The existence is proved from the finite-dimensional data; it is not inferred from unrestricted completeness or cocompleteness.

Facts & Assumptions

Given: Finite $k$ -linear abelian categories $A, B$ identified with $R - m o d$ and $S - m o d$ , a finite $(B, A)$ -bimodule $M$ , and the functors $F = Φ^{l} (M) = {Hom}_{A} (M^{*}, -)$ and $G = Φ^{r} (M) = M \otimes_{A} -$ .

[F1]

Under the identification of $A^{o p} ⊠ B$ with finite $(B, A)$ -bimodules of Categorical Eilenberg–Watts equivalences for finite linear categories the external object $\overset{ˉ}{a} ⊠ b$ corresponds to $b \otimes_{k} a^{*}$ , and $Φ^{l}, Φ^{r}$ are the transport of the functors $M \mapsto {Hom}_{A} (M^{*}, -)$ and $M \mapsto M \otimes_{A} -$ .

[F2]

The $k$ -dual of a finite-dimensional module is an exact contravariant equivalence and evaluation is a natural isomorphism $M \to M^{* *}$ , so with $U = M^{*}$ one has $M ≅ U^{*}$ and ${Hom}_{k} (a, W) ≅ W \otimes_{k} a^{*}$ naturally; all objects occurring are finite-dimensional (Finite module duality is exact with commuting bimodule actions, Linear functionals and the algebraic dual $V^{*} = L (V, F)$ , Vector space over a field).

[F3]

A wedge $ω_{c} : d \to T (c, c)$ satisfies $T (1_{c}, f) \circ ω_{c} = T (f, 1_{c^{'}}) \circ ω_{c^{'}}$ and a cowedge $ρ_{c} : T (c, c) \to d$ satisfies $ρ_{c} \circ T (f, 1_{c}) = ρ_{c^{'}} \circ T (1_{c^{'}}, f)$ for every $f : c \to c^{'}$ ; an end is a terminal wedge and a coend an initial cowedge, so factorizations through the universal (co)wedge are unique (Wedges and cowedges, and the categories they form, Dinatural transformation between functors on $C^{o p} \times C$ , The end and the coend of a functor $C^{o p} \times C \to D$ ).

[F4]

The tensor product is functorial and universal for balanced maps, and the outer actions on a tensor product are the induced ones, $(y \otimes λ) \cdot r = y \otimes (λ \cdot r)$ and $s \cdot (y \otimes λ) = (s \cdot y) \otimes λ$ (Module homomorphisms induce tensor-product homomorphisms functorially, Universal property of the tensor product for balanced maps into abelian groups, A commuting outer scalar action descends to a tensor product, $(S, R)$ -bimodules and commuting left and right scalar actions).

[F5]

A natural transformation $η : F \Rightarrow F^{'}$ induces a morphism of the universal cowedges and of the universal wedges, and ends and coends are unique up to a unique compatible isomorphism (A natural transformation of functors induces a unique morphism of their ends and of their coends, An end and a coend are unique up to a unique isomorphism compatible with every component, Natural transformation and its components, Natural isomorphism).

Proof

technique · direct

1.1givenF1F2F4

Work in the bimodule model $A = R - m o d$ , $B = S - m o d$ ; put $U = M^{*} = {Hom}_{k} (M, k)$ , a finite $(R, S)$ -bimodule, so that $F (a) = {Hom}_{R} (U, a)$ for $a \in R - m o d$ and the isomorphism $M ≅ U^{*}$ of [F2] is the evaluation. The coend diagram is the functor $T^{l} (a, b) = F (b) \otimes_{k} a^{*}$ on $R - {m o d}^{o p} \times R - m o d$ with values in finite $(S, R)$ -bimodules, where $a^{*}$ carries the right $R$ -action $(λ \cdot r) (x) = λ (r x)$ , the functoriality in $a$ is precomposition $u^{*} : a^{' *} \to a^{*}$ for $u : a \to a^{'}$ and that in $b$ is $F$ , and the tensor over $k$ carries the left $S$ -action from $F (b)$ and the right $R$ -action from $a^{*}$ [F1, F2, F4]; the end diagram is the functor $T^{r} (a, b) = G (b) \otimes_{k} a^{*}$ with $G (b) = M \otimes_{R} b$ , identified with ${Hom}_{k} (a, G (b))$ through ${Hom}_{k} (b, W) ≅ W \otimes_{k} b^{*}$ [F1, F2].

2.1step 1.1F2F3F4

Put $U = M^{*}$ and define $ρ_{a} (f \otimes λ) = λ \circ f \in U^{*} ≅ M$ . For $v : a \to a^{'}$ , $f : U \to a$ and $λ^{'} \in a^{' *}$ , one has $ρ_{a} (f \otimes v^{*} λ^{'}) = (λ^{'} \circ v) \circ f = ρ_{a^{'}} ((v \circ f) \otimes λ^{'})$ , the cowedge equation of [F3]. The maps are right $R$ -linear since $f (r u) = r f (u)$ and left $S$ -linear since $(s f) (u) = f (u s)$ and $(s μ) (u) = μ (u s)$ on $U^{*}$ . For a cowedge $t$ into a finite $(S, R)$ -bimodule $Z$ , define $t^{'} (μ) = t_{U} (1_{U} \otimes μ)$ . Its right $R$ -linearity follows from that of $t_{U}$ . For left $S$ -linearity let $R_{s} : U \to U$ be $u \mapsto u s$ ; dinaturality gives $t_{U} (1_{U} \otimes (μ \circ R_{s})) = t_{U} (R_{s} \otimes μ) = s t_{U} (1_{U} \otimes μ)$ , so $t^{'}$ is a bimodule map. Dinaturality at $f : U \to a$ gives $t_{a} (f \otimes λ) = t_{U} (1_{U} \otimes λ \circ f) = t^{'} (ρ_{a} (f \otimes λ))$ . Uniqueness follows because $ρ_{U} (1_{U} \otimes μ) = μ$ . Thus $(M, ρ)$ is the coend.

3.1step 2.1F2F3F4

For (ii) define $ω_{a} : M \to {Hom}_{k} (a, G (a))$ , $ω_{a} (m) (x) = m \otimes x$ , using the identification of step 1.1; $ω_{a}$ is left $S$ -linear and right $R$ -linear by the balancedness of $M \otimes_{R} -$ and the outer actions [F4]. It is a wedge: for $f : a \to a^{'}$ one has $T^{r} (1_{a}, f) \circ ω_{a} = T^{r} (f, 1_{a^{'}}) \circ ω_{a^{'}}$ because both sides send $m$ to the map $x \mapsto m \otimes f (x)$ [F3]. For universality let $t$ be a wedge from $Z$ and define $h : Z \to M$ by $h (z) = t_{R} (z) (1_{R})$ under $G (R) ≅ M$ ; dinaturality of $t$ at the maps $ℓ_{x} : R \to a$ , $ℓ_{x} (r) = r \cdot x$ , gives $t_{a} (z) (x) = h (z) \otimes x$ , so $t$ factors through $h$ ; an element of ${Hom}_{k} (a, G (a))$ is determined by its values, so the factorization is unique, and $h$ is a bimodule map because the components $t_{a}$ are and $t_{R} (z \cdot r) (1_{R}) = t_{R} (z) (r)$ by right $R$ -linearity of $t_{R}$ , while dinaturality at $r_{r} : R \to R$ identifies $t_{R} (z) (r)$ with $h (z) \cdot r$ under $G (R) ≅ M$ [F3, F4]. Hence $(M, ω)$ is the end $\int_{a} \overset{ˉ}{a} ⊠ G (a)$ , and $Ψ^{r} Φ^{r} (M) ≅ M$ .

4.1step 2.1step 3.1F1F5∎

A natural transformation $η : F \Rightarrow F^{'}$ induces a natural transformation of diagrams with components $η_{b} \otimes 1_{a^{*}}$ . For coends its induced map $q \to q^{'}$ is uniquely characterized by $ρ_{a}^{'} (η_{a} \otimes 1) = (q \to q^{'}) ρ_{a}$ ; for ends it is characterized by the dual projection equation [F5]. Uniqueness proves the identity and composition laws in both cases. For a bimodule map $j : M \to M^{'}$ , the formula for $ρ$ intertwines precomposition by $j^{*}$ with $j$ , and that for $ω$ intertwines $m \mapsto j (m)$ with $j \otimes 1_{a}$ . Hence the comparisons $Ψ^{l} Φ^{l} ≅ 1$ and $Ψ^{r} Φ^{r} ≅ 1$ are natural in $M$ . Every Lex or Rex functor has the corresponding model form by [F1], so these explicit chosen kernel objects also supply the (co)ends for arbitrary such functors; transporting the universal maps along their natural comparison isomorphisms proves this. The equivalences in [F1] then give the other quasi-inverse comparisons. No unrestricted (co)completeness or new choice is required beyond the supplied models and equivalence data.

Depends on

Used by

Dependency tree · two levels

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