TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

An end and a coend are unique up to a unique isomorphism compatible with every component

Statement

Let $T : C^{o p} \times C \to D$ be a functor.

If $(e, ω)$ and $(e^{'}, ω^{'})$ are ends of $T$ (The end and the coend of a functor $C^{o p} \times C \to D$ ), there is exactly one isomorphism $u : e \to e^{'}$ satisfying $ω_{c}^{'} \circ u = ω_{c}$ for every object $c$ of $C$ . If $(q, ρ)$ and $(q^{'}, ρ^{'})$ are coends of $T$ , there is exactly one isomorphism $v : q \to q^{'}$ satisfying $v \circ ρ_{c} = ρ_{c}^{'}$ for every $c$ .

An end and a coend of $T$ are therefore unique up to a unique isomorphism compatible with every component.

Facts & Assumptions

Given: A functor $T : C^{o p} \times C \to D$ , together with two ends of $T$ and two coends of $T$ .

[L1]

Any two initial objects in a category are joined by a unique isomorphism. Any two terminal objects are likewise joined by a unique isomorphism (Initial and terminal objects are unique up to a unique isomorphism).

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

[F2]

A morphism of wedges $(d, ω) \to (d^{'}, ω^{'})$ is a morphism $h : d \to d^{'}$ with $ω_{c}^{'} \circ h = ω_{c}$ for every $c$ , a morphism of cowedges $(d, ρ) \to (d^{'}, ρ^{'})$ is a morphism $h : d \to d^{'}$ with $h \circ ρ_{c} = ρ_{c}^{'}$ for every $c$ , and wedges over $T$ and their morphisms form a category $Wd (T)$ , cowedges under $T$ and their morphisms the category $Cwd (T)$ (Wedges and cowedges, and the categories they form).

Proof

technique · direct

1.1

The two ends $(e, ω)$ and $(e^{'}, ω^{'})$ are two terminal objects of the one category $Wd (T)$ , and the two coends are two initial objects of the one category $Cwd (T)$ .

F1F2

2.1

Applying the terminal clause of [L1] in $Wd (T)$ gives a unique isomorphism $(e, ω) \to (e^{'}, ω^{'})$ of wedges.

L1F1step 1.1

2.2

Applying the initial clause of [L1] in $Cwd (T)$ gives a unique isomorphism $(q, ρ) \to (q^{'}, ρ^{'})$ of cowedges.

L1F1step 1.1

3.1

An isomorphism of $Wd (T)$ is by [F2] an isomorphism $u : e \to e^{'}$ of $D$ with $ω_{c}^{'} \circ u = ω_{c}$ for every $c$ , and an isomorphism of $Cwd (T)$ is an isomorphism $v : q \to q^{'}$ with $v \circ ρ_{c} = ρ_{c}^{'}$ for every $c$ ; so the two isomorphisms produced in steps 2.1 and 2.2 are exactly the ones the Statement asserts, and their uniqueness is the uniqueness given there.

F2step 2.1step 2.2∎

Remarks

The compatibility clause is not an extra verification: it is what being a morphism in $Wd (T)$ or $Cwd (T)$ means, so the published uniqueness of terminal and initial objects delivers it already. This is why the definition of an end is stated as a universal property in a category of wedges rather than as a family of morphisms with an ad hoc uniqueness clause.

An isomorphism of wedges is in particular an isomorphism of $D$ : its inverse in $Wd (T)$ is a morphism of $D$ satisfying the displayed equation, and the two composites are the identities of $e$ and $e^{'}$ .

Depends on

Used by

Fubini: an end over a product index category and the two iterated ends exist together and agree Theorem

Dependency tree · two levels

11 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

F. Loregian, (Co)end Calculus (arXiv:1501.02503v7), Definition 1.1.6 and Remark 1.1.5 (standard reference, not scraped)