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.
A functor is an isomorphism of categories exactly when its object and morphism maps are bijective
Statement
A functor is an isomorphism of categories, meaning that it has a two-sided inverse functor, exactly when its object map and its total morphism map are bijective.
For large categories, these are bijective definable class maps under Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why is not formed.
Facts & Assumptions
Given: A functor .
Functors preserve domains, codomains, identities, and composition (Covariant functor, identity functor, composite functor, and contravariant functor), while the Statement defines a category isomorphism by a two-sided inverse functor.
A set function is bijective exactly when it has a two-sided inverse ( is a bijection if and only if there is a function with and ; such a is unique, equals the inverse relation , and is itself a bijection). Under the Statement's definable-class convention, the same pointwise statement defines a bijective class map and its uniquely determined inverse class map.
Proof
If has an inverse functor, the object maps and morphism maps are pointwise inverse maps and hence bijective by [L2].
Conversely, use the uniquely determined inverse set functions or definable class maps on objects and morphisms supplied by [L2]. The inverse morphism map preserves domain and codomain because applying injective reduces each assertion to the corresponding assertion for .
The same injectivity argument shows that the inverse sends identities to identities and preserves composition; it is therefore an inverse functor, so is a category isomorphism.
Depends on
- Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why $\mathbf{CAT}$ is not formed
- Covariant functor, identity functor, composite functor, and contravariant functor
- $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = \Delta_A$ and $f \circ g = \Delta_B$; such a $g$ is unique, equals the inverse relation $f^{-1}$, and is itself a bijection
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 33 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Emily Riehl, Category Theory in Context, Chapter 1 (standard reference, not scraped)