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.
Enrichment in a preorder recovers a preorder, and enrichment in sets recovers a small ordinary category
Statement
Let be a monoidal category that is also a preorder in the sense that between any two objects of there is at most one morphism. Then the underlying ordinary category of every -category is a preorder. If with its cartesian monoidal structure, then a -enriched category is exactly a small ordinary category.
Facts & Assumptions
Given: A -category .
A preorder is a reflexive and transitive relation on a set (Preorder and monotone map).
A category has objects, morphisms, identities, and associative composition (Category, object, morphism, domain, codomain, identity, composition, and hom-collection).
A -category has hom-objects, enriched composition, and enriched identities (Enriched category over a monoidal base).
Proof
Suppose the base is thin. Then for any objects of , the hom-set of the underlying ordinary category is . Because has at most one morphism between any two objects, this hom-set has at most one element. The enriched identities and composition from [L3] become ordinary identities and composition, so the underlying category is a category all of whose hom-sets are subsingletons. Defining when such a morphism exists gives a reflexive and transitive relation by [L2], hence a preorder by [L1].
Now take with cartesian product and singleton unit. Then a hom-object of [L3] is literally a set of morphisms, an identity map chooses an identity element, and the composition morphism is ordinary composition of elements. The associativity and unit diagrams of [L3] are exactly the axioms of [L2]. Conversely, every small ordinary category gives such data by taking its hom-sets as the enriched hom-objects; its object collection is a set as required by [L3].
Therefore thin-base enrichment recovers a preorder on the object set, and Set-enrichment recovers precisely a small ordinary category.
Depends on
Used by
Nothing in the library uses this result yet.
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, Section 1.2 (standard reference, not scraped)
- Emily Riehl, Categorical Homotopy Theory, Sections 3.2 and 3.3 (standard reference, not scraped)