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 functor preserving twisted-arrow limits preserves ends, and dually for coends
Statement
Let be a functor and let be a functor.
Ends. If preserves -limits (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors, The twisted arrow category and its projection to ) and is an end of (The end and the coend of a functor ), then is an end of ; so a functor preserving twisted-arrow limits preserves ends.
Coends. If preserves -colimits and is a coend of , then is a coend of .
Small index. If in addition is small (Small, locally small, and large categories), then every continuous satisfies the first hypothesis and every cocontinuous the second, so a continuous functor carries an end over a small index category to an end and a cocontinuous functor carries such a coend to a coend.
Facts & Assumptions
Given: Functors and , and an end or a coend of where one is assumed.
The wedges over are exactly the cones over , by and , so an end is the limit over the twisted arrow category; dually the cowedges under are the cocones under and a coend is a colimit over (An end is a limit over the twisted arrow category, and a coend is a colimit over its opposite).
preserves -limits if the image under of every limiting cone over is limiting over ; the terms for colimits use cocones (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).
A functor is continuous if it preserves all small limits and cocontinuous if it preserves all small colimits (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).
The objects of are the morphisms of , and a morphism is a pair of morphisms of subject to one equation (The twisted arrow category and its projection to ).
An end of is a terminal object of the category of wedges over and a coend an initial object of the category of cowedges under ; in short, an end is a terminal wedge and a coend an initial cowedge (The end and the coend of a functor ).
A category is small when both and are sets. (Small, locally small, and large categories).
Proof
By [L1] the wedge over with vertex corresponds to the cone over with , and is an end of exactly when is a limiting cone; dually the cowedge corresponds to the cocone under with , and is a coend exactly when is a colimiting cocone.
Suppose preserves -limits. Then is a limiting cone over . Functoriality gives , so is exactly the cone that [L1] attaches to the family , which is therefore a wedge over ; being limiting, it makes an end of .
Suppose preserves -colimits. Then is a colimiting cocone under , and is the cocone that [L1] attaches to ; so is a cowedge under and is a coend of .
If is small then is small, since its objects are the morphisms of and its morphisms form a subclass of a fourfold product of with itself; the opposite of a small category is small. So a continuous , which by [F2] preserves all small limits, preserves -limits and step 2.1 applies, and a cocontinuous preserves -colimits and step 2.2 applies.
Remarks
The hypothesis is stated at the strength the proof uses, preservation of limits indexed by , and not as continuity: in this library a continuous functor is one preserving all small limits, and is small only when is. A blanket claim that continuous functors preserve all ends would be false for a large index category, and no such claim is made here.
Dropping the hypothesis altogether is not possible: FALSE: every functor preserves the ends that exist in its domain exhibits two finite witnesses, both monotone maps of finite posets, that carry an end to something other than the end of the composite.
Depends on
- An end is a limit over the twisted arrow category, and a coend is a colimit over its opposite
- Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors
- The end and the coend of a functor $\mathcal C^{\mathrm{op}}\times\mathcal C\to\mathcal D$
- The twisted arrow category and its projection to $\mathcal C^{\mathrm{op}}\times\mathcal C$
- Small, locally small, and large categories
Used by
Dependency tree · two levels
17 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)