ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26‡ rests on unproved material (inherited)

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.

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The tensor product of monoid sets as a coend

Example

Let $M$ be a monoid (Semigroup and monoid) and let $C_{M}$ be the one-object category it determines (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible), whose only object is written $*$ and whose morphisms are the elements of $M$ .

A presheaf $P : C_{M}^{o p} \to S e t$ is a set $X : = P (*)$ with a right action $x \cdot m : = P (m) (x)$ , and a covariant functor $F : C_{M} \to S e t$ is a set $Z : = F (*)$ with a left action $m \cdot z : = F (m) (z)$ . Then the functor tensor product (The tensor product of a presheaf and a covariant set-valued functor) is

$P \otimes_{C_{M}} F = (X \times Z) / ⁣ \sim,$

where $\sim$ is the least equivalence relation on the Cartesian product (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ ) containing $(x \cdot m, z) \sim (x, m \cdot z)$ for all $x \in X$ , $z \in Z$ and $m \in M$ .

Facts & Assumptions

Given: A monoid $M$ , a right $M$ -set $X$ and a left $M$ -set $Z$ , presented as a presheaf and a covariant functor on the one-object category of $M$ .

[F4]

A monoid is a set with an associative operation and a two-sided identity (Semigroup and monoid).

[L2]

Every monoid is a one-object category, and under this identification the monoid is a group exactly when every morphism is invertible (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible).

[F5]

The elements of $A \times B$ are exactly the ordered pairs: Thus $z \in A \times B$ holds if and only if $z = (a, b)$ for some $a \in A$ and some $b \in B$ . (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ ).

[F1]

The tensor product of a presheaf $P$ and a covariant set-valued functor $F$ is the coend of the product of a presheaf and a covariant set-valued functor, the integrand being $T (c_{1}, c_{2}) = P (c_{1}) \times F (c_{2})$ (The tensor product of a presheaf and a covariant set-valued functor).

[F3]

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$ ).

[L1]

For small $C$ and a set-valued integrand the coend is the disjoint union of the diagonal values modulo the dinaturality relation, generated by the pairs $(c, T (f, 1_{c}) (x))$ and $(c^{'}, T (1_{c^{'}}, f) (x))$ for $f : c \to c^{'}$ and $x \in T (c^{'}, c)$ (A set-valued coend is the disjoint union of the diagonal values modulo the dinaturality relation).

Verification

technique · direct

1.1

The category $C_{M}$ has one object and its morphism collection is the set $M$ , so it is small; by [F1] the integrand is $T (*, *) = X \times Z$ , and every value of $T$ , on or off the diagonal, is that same set. The disjoint union over the objects therefore has one summand and is $X \times Z$ itself.

F1F4F5L2given

2.1

The generating pairs of [L1] are indexed by a morphism $m$ of $C_{M}$ , that is by an element of $M$ , and by an element of the off-diagonal value, that is by a pair $(x, z) \in X \times Z$ . The first leg $T (m, 1_{*})$ acts by $P (m)$ in the contravariant slot and by the identity in the covariant one, giving $(x \cdot m, z)$ ; the second leg $T (1_{*}, m)$ acts by the identity in the contravariant slot and by $F (m)$ in the covariant one, giving $(x, m \cdot z)$ . So the generating pairs are exactly $(x \cdot m, z)$ against $(x, m \cdot z)$ .

F5L1step 1.1

3.1

By [L1] and [F3] the coend is the quotient of the single summand $X \times Z$ by the least equivalence relation containing those pairs, which is the displayed description of $P \otimes_{C_{M}} F$ . At $m$ the identity of $M$ the two legs agree, so the identity contributes only reflexive pairs.

F3L1step 2.1∎

Remarks

The relation is exactly the one used to define the tensor product of a right and a left module over a ring, with the additive structure removed: an element of $M$ may be moved across the pair from the right-hand factor to the left-hand one. What the coend adds is that this relation is not imposed by hand but is forced by the cowedge equation, whose two legs are the two actions.

The one-object case is where the coproduct of the general description collapses to a single summand, which is why the answer is a quotient of $X \times Z$ rather than of a disjoint union. For a category with more objects the same computation gives one summand per object and identifications running along every morphism.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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