TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

A module-valued coend is the direct sum of the diagonal values modulo the dinaturality submodule

Statement

Let $R$ be a unital ring, let $C$ be a small category (Small, locally small, and large categories) and let $T : C^{o p} \times C \to R - M o d$ be a functor (Left modules over a fixed ring and module homomorphisms form the large locally small category $R - M o d$ ). Write $ȷ_{c} : T (c, c) \to ⨁_{c} T (c, c)$ for the coordinate inclusions of the direct sum (The direct sum of an indexed family of modules) and let

$S : = ⟨ ȷ_{c} (T (f, 1_{c}) (x)) - ȷ_{c^{'}} (T (1_{c^{'}}, f) (x)) : f : c \to c^{'} in C, x \in T (c^{'}, c) ⟩_{R}$

be the submodule generated by those elements (Submodule of a module, Generated submodule, cyclic and finitely generated modules, module basis and free module).

Then $T$ has a coend, and it is the direct sum of the diagonal values modulo the dinaturality submodule (The end and the coend of a functor $C^{o p} \times C \to D$ , Quotient module $M / N$ with scalar multiplication on additive cosets):

$\int^{c} T (c, c) = (⨁_{c} T (c, c)) / S, ρ_{c} = π \circ ȷ_{c},$

where $π$ is the quotient homomorphism. As in the set-valued case, the generating element $x$ lies in the off-diagonal value $T (c^{'}, c)$ , and the two terms of the generator sit in the summands at $c$ and at $c^{'}$ respectively.

Facts & Assumptions

Given: A unital ring $R$ , a small category $C$ , and a functor $T$ from $C^{o p} \times C$ to left $R$ -modules.

[F5]

For a fixed ring $R$ , left $R$ -modules and module homomorphisms form a large locally small category $R - M o d$ (Left modules over a fixed ring and module homomorphisms form the large locally small category $R - M o d$ ).

[F8]

A category is small when both $Ob (C)$ and $Mor (C)$ are sets. (Small, locally small, and large categories).

[F1]

The direct sum $⨁_{i \in I} M_{i}$ is the submodule of the direct product consisting of the families of finite support, with coordinate inclusions $ȷ_{i}$ ; If $I = \emptyset$ , both product and direct sum are the zero module. (The direct sum of an indexed family of modules).

[F3]

A subset $N \subseteq M$ is a submodule when it is a subgroup of the additive group of $M$ and is closed under scalars: $r \in R, n \in N \Rightarrow r n \in N$ (Submodule of a module).

[F2]

The submodule generated by $S \subseteq M$ is $⟨ S ⟩_{R} : = ⋂ {N \leq M : S \subseteq N}$ , the smallest submodule of $M$ containing $S$ (Generated submodule, cyclic and finitely generated modules, module basis and free module).

[F4]

For $N \leq M$ the quotient module $M / N$ has the cosets $m + N$ as elements and scalar action $r (m + N) : = r m + N$ (Quotient module $M / N$ with scalar multiplication on additive cosets).

[L1]

For every family of homomorphisms $f_{i} : M_{i} \to N$ there is a unique homomorphism $f : ⨁_{i \in I} M_{i} \to N$ such that $f \circ ȷ_{i} = f_{i}$ for every $i$ . It is given by the finite sum of the $f_{i} (m_{i})$ over the support (Universal property of a direct sum of modules).

[L2]

If $f : M \to P$ is a homomorphism and $N \leq M$ satisfies $N \subseteq \ker f$ , there is a unique homomorphism $\overset{ˉ}{f} : M / N \to P$ such that $\overset{ˉ}{f} (m + N) = f (m)$ , equivalently $f = \overset{ˉ}{f} \circ π$ (A module homomorphism vanishing on $N$ factors uniquely through $M / N$ ).

[F7]

A cowedge from $T$ to $d$ is a dinatural transformation from $T$ to a constant functor: a family $ρ_{c} : T (c, c) \to d$ with $ρ_{c} \circ T (f, 1_{c}) = ρ_{c^{'}} \circ T (1_{c^{'}}, f)$ for every $f : c \to c^{'}$ (Wedges and cowedges, and the categories they form).

[F6]

An end of $T$ is a terminal object of the category of wedges over $T$ and a coend an initial object of the category of cowedges under $T$ ; in short, an end is a terminal wedge and a coend an initial cowedge (The end and the coend of a functor $C^{o p} \times C \to D$ ).

Proof

technique · constructive

1.1

Since $C$ is small its objects form a set, so $(T (c, c))_{c \in Ob (C)}$ is a set-indexed family of left $R$ -modules and the direct sum $⨁_{c} T (c, c)$ with its coordinate inclusions $ȷ_{c}$ is formed.

F1F5F8givenconstruct

2.1

The displayed generating elements lie in $⨁_{c} T (c, c)$ , so $S$ is the smallest submodule containing them, and $Q : = (⨁_{c} T (c, c)) / S$ with quotient homomorphism $π$ is a left $R$ -module. The construction is carried out here rather than obtained from a general cocompleteness theorem, which would assert that the coend exists without exhibiting it.

F2F3F4step 1.1construct

3.1

The family $ρ_{c} : = π \circ ȷ_{c}$ is a cowedge from $T$ to $Q$ : for $f : c \to c^{'}$ and $x \in T (c^{'}, c)$ the difference $ρ_{c} (T (f, 1_{c}) (x)) - ρ_{c^{'}} (T (1_{c^{'}}, f) (x))$ is $π$ applied to a generator of $S$ , hence zero, and each $ρ_{c}$ is a homomorphism because the coordinate inclusion $ȷ_{c}$ and the quotient map $π$ are.

F1F4F7step 2.1

4.1

Let $λ_{c} : T (c, c) \to N$ be any cowedge. By [L1] there is a unique homomorphism $λ : ⨁_{c} T (c, c) \to N$ with $λ ȷ_{c} = λ_{c}$ ; the cowedge equations for the family $λ_{c}$ make every displayed generator lie in $\ker λ$ , and $\ker λ$ is a submodule, so $S \subseteq \ker λ$ by [F2]. By [L2] there is a unique $\overset{ˉ}{λ} : Q \to N$ with $\overset{ˉ}{λ} π = λ$ , hence with $\overset{ˉ}{λ} ρ_{c} = λ_{c}$ for every $c$ ; and any homomorphism $μ : Q \to N$ with $μ ρ_{c} = λ_{c}$ satisfies $μ π ȷ_{c} = λ_{c}$ , so $μ π = λ$ by the uniqueness in [L1] and $μ = \overset{ˉ}{λ}$ by the uniqueness in [L2]. So $(Q, ρ)$ is an initial cowedge, that is a coend of $T$ .

F6F7L1L2step 3.1

5.1

If $C$ is empty the index set is empty, so by [F1] the direct sum is the zero module, the generating set is empty, $S$ is the zero submodule and $Q$ is the zero module; step 4.1 then says the zero module is the initial cowedge, which is correct because a cowedge under the empty family is just an object and the zero module is initial in $R - M o d$ . This is the asserted presentation of the coend in every case.

F1step 4.1discharge-construct∎

Remarks

The route is deliberately through the direct-sum and quotient universal properties rather than through a cocompleteness theorem for $R$ -modules: such a theorem says a colimit exists, and what is wanted here is the coequalizer itself, in a form in which an element of the coend can be named as a class of a finite sum.

At $f = 1_{c}$ the generator is $ȷ_{c} (x) - ȷ_{c} (x) = 0$ , so identity morphisms enlarge $S$ by nothing; and if $C$ is discrete there are no non-identity morphisms at all, $S$ is the zero submodule and the coend is the direct sum of the diagonal values.

Depends on

Used by

A module-valued coend computed as a quotient of a direct sum Example

Dependency tree · two levels

27 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

B. Richter, From Categories to Homotopy Theory (author's draft), Example 4.4.7 (standard reference, not scraped)