False statementConstruction: AI-adaptedVerification: 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.

FALSE: every functor preserves the ends that exist in its domain

Statement

False claim: if $T : C^{o p} \times C \to D$ has an end and $G : D \to E$ is any functor, then $G$ carries that end to an end of $G T$ (The end and the coend of a functor $C^{o p} \times C \to D$ , Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

Facts & Assumptions

Given: Two witnesses built from finite posets, regarded as categories, with monotone maps as functors.

[F5]

A preorder is a reflexive transitive relation, a map between preorders is monotone when it respects the order, and every partial order is a preorder (Preorder and monotone map).

[L2]

A preorder determines a category with at most one morphism between any two objects, and functors between such categories are exactly monotone maps (A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps).

[F2]

A product of $(A_{i})_{i \in I}$ is an object $P$ with projections $p_{i}$ such that every family $f_{i} : X \to A_{i}$ has a unique pairing $⟨ f_{i} ⟩_{i \in I} : X \to P, p_{i} ⟨ f_{i} ⟩ = f_{i} (i \in I)$ (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F6]

A limit of a diagram is a terminal cone: explicitly, for every cone $(X, ξ)$ there exists a unique morphism $u : X \to L$ such that $λ_{j} u = ξ_{j}$ for every $j$ ; a product is the limit of a family on a discrete index category (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F3]

A subcategory is full when $A (A, B) = C (A, B)$ for every pair of its objects, so a full subcategory is determined entirely by its objects (Subcategory and full subcategory).

[F4]

$G$ preserves $J$ -limits if the image under $G$ of every limiting cone over $D : J \to C$ is limiting over $G D$ (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

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

[L1]

For $F : C \to D$ and $F^{'} (c_{1}, c_{2}) : = F (c_{2})$ , the end of a functor made mute in its contravariant variable is the ordinary limit of that functor: $\int_{c} F^{'} (c, c) = \lim F$ (The end of a functor made mute in its contravariant variable is the ordinary limit of that functor).

[L3]

If $G$ preserves $Tw (C)$ -limits and $T$ has an end, then $G$ of that end is an end of $G T$ , so a functor preserving twisted-arrow limits preserves ends (A functor preserving twisted-arrow limits preserves ends, and dually for coends).

Refutation

technique · direct

1.1

Regard a poset as a category by [L2] and [F5], so that a morphism $a \to b$ exists exactly when $a \leq b$ and monotone maps are exactly the functors. Let $C$ be the discrete category on two objects and let $F : C \to P$ pick out two elements $x$ and $y$ of a poset $P$ . By [F2] and [F6] a product of $x$ and $y$ in $P$ is an element below both through which every element below both factors, that is a greatest lower bound; and by [L1] that product is the end of the mute functor $F^{'}$ on $C^{o p} \times C$ , since $F^{'}$ has the same limit.

F1F2F5F6L1L2construct

2.1

First witness. Let $P$ be the four-element poset ${⊥, x, y, ⊤}$ with $⊥ < x < ⊤$ , $⊥ < y < ⊤$ and $x, y$ incomparable, and let $Q$ be the two-element chain ${0 < 1}$ . The map $ϕ$ with $ϕ (⊥) = 0$ and $ϕ (x) = ϕ (y) = ϕ (⊤) = 1$ is monotone, hence a functor by [L2]. The greatest lower bound of $x$ and $y$ in $P$ is $⊥$ , so by step 1.1 the end exists and is $⊥$ ; but the greatest lower bound of $ϕ (x) = 1$ and $ϕ (y) = 1$ in $Q$ is $1$ , while $ϕ (⊥) = 0$ . So $ϕ$ carries the end to an element that is not the end of the composite, and by [F4] it does not preserve it.

F4L2step 1.1

2.2

Second witness, with a full and faithful functor. Let $P^{'}$ be the four-element poset ${⊥, m, x, y}$ with $⊥ < m$ , $m < x$ , $m < y$ and $x, y$ incomparable, so that the greatest lower bound of $x$ and $y$ in $P^{'}$ is $m$ . Let $Q^{'}$ be the full subposet on ${⊥, x, y}$ , which by [F3] is a full subcategory, and in which the greatest lower bound of $x$ and $y$ is $⊥$ . The inclusion $Q^{'} \to P^{'}$ is monotone, hence a functor, and it carries the end $⊥$ computed in $Q^{'}$ to $⊥$ , which is not the end $m$ computed in $P^{'}$ .

F3F4L2step 1.1

3.1

Each witness refutes the displayed claim, and neither uses anything infinite: both posets have four elements and every check is a comparison of two named elements. What is true is [L3]: a functor that preserves $Tw (C)$ -limits preserves the ends indexed by $C$ , and a right adjoint has that property for every $C$ . Neither witness is a right adjoint.

F1L3step 2.1step 2.2∎

Remarks

The two witnesses fail in opposite directions and that is deliberate. In the first the image of the end is strictly below the end of the image; in the second it is strictly below as well, but the functor is a full and faithful inclusion, so fullness and faithfulness are not what is missing. What is missing in both cases is a hypothesis about limits, and only that.

A poset is the cheapest place to see the failure because a limit there is an order-theoretic infimum and a functor is a monotone map, so the whole question becomes whether a monotone map carries greatest lower bounds to greatest lower bounds. It plainly need not.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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), Theorem 1.2.7 (standard reference, not scraped)