ExampleConstruction: AI-generatedVerification: 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 coend of the hom-bifunctor

Example

Let $C$ be a small category (Category, object, morphism, domain, codomain, identity, composition, and hom-collection, Small, locally small, and large categories) and let $C (-, -)$ be its hom-bifunctor (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor). Then

$\int^{c} C (c, c) = (∐_{c} C (c, c)) / ⁣ \sim,$

where $\sim$ is the least equivalence relation (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ) containing $(c, x \circ f) \sim (c^{'}, f \circ x)$ for every $f : c \to c^{'}$ and every $x : c^{'} \to c$ (The end and the coend of a functor $C^{o p} \times C \to D$ ).

Two evaluations: on the walking arrow the coend has two elements, and on the one-object category of a monoid $M$ (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible) it is the quotient of $M$ by the least equivalence relation containing $x f \sim f x$ , which when $M$ is a group is the set of conjugacy classes.

Facts & Assumptions

Given: A small category $C$ and its hom-bifunctor as the integrand.

[F5]

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

[F4]

Composition in a category is associative and unital: $h \circ (g \circ f) = (h \circ g) \circ f, 1_{B} \circ f = f = f \circ 1_{A}$ (Category, object, morphism, domain, codomain, identity, composition, and hom-collection).

[F2]

The hom-assignment sends $(a, b)$ to $C (a, b)$ , and a morphism of the product category consisting of $h : a^{'} \to a$ and $u : b \to b^{'}$ acts by $C (h, u) : C (a, b) ⟶ C (a^{'}, b^{'}), f ⟼ u \circ f \circ h$ (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[L2]

For every locally small category $C$ , the hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a functor (The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor).

[F3]

A binary relation on a set is an equivalence relation when it is reflexive, symmetric and transitive; the quotient set is the set of its classes (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ).

[F1]

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

[L3]

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

[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

Take $T = C (-, -)$ , a functor into $S e t$ by [L2], with $T (c, c) = C (c, c)$ and off-diagonal value $T (c^{'}, c) = C (c^{'}, c)$ . By [F2] the two legs act on $x \in C (c^{'}, c)$ as $T (f, 1_{c}) (x) = 1_{c} \circ x \circ f = x \circ f$ and $T (1_{c^{'}}, f) (x) = f \circ x \circ 1_{c^{'}} = f \circ x$ , using [F4]. So the generating pairs of [L1] are exactly the displayed ones, and the description of the coend follows from [L1] and [F3].

F2F3F4F5L1L2given

2.1

On the walking arrow, with objects $0$ and $1$ and one non-identity morphism $u : 0 \to 1$ , the disjoint union is ${(0, 1_{0}), (1, 1_{1})}$ . A generating pair needs a morphism $f : c \to c^{'}$ together with an element $x$ of $C (c^{'}, c)$ ; the only non-identity morphism is $u : 0 \to 1$ and $C (1, 0)$ is empty, so it contributes none, while an identity $f = 1_{c}$ gives $x \circ 1_{c} = 1_{c} \circ x$ and hence only reflexive pairs. The relation is therefore equality and the coend has two elements.

F1F4step 1.1

2.2

On the one-object category $C_{M}$ of a monoid $M$ , the disjoint union has one summand and is $M$ itself, every value of the integrand being $M$ ; and by step 1.1 the generating pairs are $x \circ f$ against $f \circ x$ for $x, f \in M$ . So the coend is $M$ modulo the least equivalence relation containing $x f \sim f x$ . Nothing further is claimed for a general monoid.

F1F3L3step 1.1

3.1

If $M$ is a group, that quotient is the set of conjugacy classes. Each generating pair is a conjugation, since $f x = f (x f) f^{- 1}$ , and conjugacy is an equivalence relation, so the least equivalence relation containing the generators is contained in conjugacy; conversely, for $g$ and $h$ in $M$ the choice $x : = g h^{- 1}$ and $f : = h$ gives $x f = g$ and $f x = h g h^{- 1}$ , so every conjugate pair is a generating pair and conjugacy is contained in the relation. The two therefore agree. Without inverses this second half is unavailable, which is why the general case of step 2.2 is stated only as the quotient by that relation.

F3L3step 2.2∎

Remarks

On the walking arrow the coend is larger than the end, which is a one-element set: nothing is identified, because the identification would have to be indexed by an element of an empty hom-set. This is the same emptiness that makes the convention for which category computes a coend worth stating carefully.

The monoid clause is where the temptation to overstate lies. "Conjugacy class" is the right name only when every element has an inverse. For a general monoid the quotient is still defined by the same generators, but the monoid supplies no conjugation action whose orbits are those classes; calling them conjugacy classes would assert more than the computation gives. Abstractly, as for every equivalence relation, some subgroup of a symmetric group can be chosen to have the classes as its orbits.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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