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 bijection on underlying hom-sets need not exhibit a cotensor
Statement refuted
A bijection between the underlying hom-sets in the defining formula of a cotensor is enough to prove that the object is a cotensor.
Facts & Assumptions
Given: The Cat-enriched setting, the discrete two-object category , and the one-object category whose endomorphism monoid is .
A cotensor requires an isomorphism of enriched hom-objects, not merely a bijection of their underlying sets (Tensor and cotensor in a V-category).
The underlying-category construction can forget morphisms inside a hom-object (The underlying category can lose genuinely enriched information).
Counterexample
Give its strict monoidal structure induced by addition: it has one object, both composition and tensor of endomorphisms are addition in , and commutativity gives the interchange law. Hence there is a one-object -enriched category with sole object , hom-category , and enriched composition given by this tensor.
The underlying category has one object and one morphism, since the objects of form a singleton. Thus, for its only test object , there is a bijection both sides are singletons, because a functor from the discrete two-object category to the one-object category is unique on objects and identities. This bijection is automatically natural in the one-object category .
If were its own cotensor by , [L1] would require an isomorphism of categories But the endomorphism monoids of the unique objects are respectively and , which are not isomorphic: the former has one indecomposable nonzero generator and the latter has two. Hence the natural underlying hom-set bijection of step 2.1 does not exhibit a cotensor.
Depends on
Used by
- A bijection of hom-sets that does not exhibit a cotensor Counterexample
Dependency tree · two levels
7 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
- G. M. Kelly, Basic Concepts of Enriched Category Theory, equation (3.45) (standard reference, not scraped)
- Emily Riehl, Categorical Homotopy Theory, Section 3.7 (standard reference, not scraped)