Alphabeta MathHow 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.
The underlying category of a Cat-enriched category forgets the 2-cells
Example
Let be a strict 2-category with a set of objects and small hom-categories, viewed as a -enriched category. Then its underlying ordinary category has the same objects and the same 1-morphisms, but no nonidentity 2-cells.
Facts & Assumptions
Given: A strict 2-category with a set of objects and small hom-categories.
Strict 2-categories and -enriched categories are the same data in the present size range (A Cat-enriched category is exactly a strict 2-category with a set of objects and small hom-categories).
The underlying ordinary category of a Cat-enriched category keeps only the objects of each hom-category (The underlying category can lose genuinely enriched information).
Verification
Read as a -enriched category using [L1].
Then [L2] says that the hom-set in the underlying category is the set of objects of the corresponding hom-category of . Those objects are the 1-morphisms, while the 2-morphisms are morphisms inside the hom-category and are forgotten.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
6 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
- Emily Riehl, Categorical Homotopy Theory, Sections 3.1 and 3.4 (standard reference, not scraped)