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.
Closed Monoidal Categories and the Internal Hom - Examples
1 · Prerequisites
- Adjunctions Units and Counits
- Binary Operations, Monoids, Groups and Subgroups
- Cardinal Arithmetic, Cofinality and the Alephs
- Categories, Functors and Natural Transformations
- Closed Monoidal Categories and the Internal Hom
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Group Homomorphisms and the Isomorphism Theorems
- Limits and Colimits
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monoidal Categories and Monoidal Functors
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Reflective Subcategories and the Adjoint Functor Theorems
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Set Theory Beyond Choice: Recorded, Not Proved Here
- Suprema and Infima
- Tensor Products of Modules
- The ZFC Axioms and the Basic Set Constructions
- Universal Properties, Representables and the Yoneda Lemma
2 · Summary
These examples compute the universal maps from the A page in concrete settings: function sets in Set, the Hom-tensor adjunction in Ab, exponential objects in Cat, dependent products in slices of Set, and a subobject classifier in a small presheaf category.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A function set computed as an exponential object
Example
Take and . Then is the four-element set of functions :
where, for instance, means and .
Facts & Assumptions
Given: The sets , , and .
In , function sets are exponential objects (Set is cartesian closed).
Verification
The evaluation map is , . For example, and .
Let . A map is just a function , so it is exactly one of the four displayed elements of . Hence maps biject with maps by sending the unique point of to the corresponding function.
This is the exponential universal property in the concrete case, matching Set is cartesian closed.
Currying for sets of three variables
Example
Let and . Define
where the sum is taken in the integers.
Facts & Assumptions
Given: The concrete map on .
Currying and uncurrying are mutually inverse, and repeated currying is associative up to reassociation (Currying and uncurrying are mutually inverse).
Verification
Currying in the -variable sends to the function . Currying again in the -variable sends to the function .
Uncurrying the result reverses those two assignments: from recover the map , then evaluate at to recover .
So the twice-curried and twice-uncurried maps return the original , exactly as Currying and uncurrying are mutually inverse predicts.
The internal hom of abelian groups
Example
In , viewed as , the internal hom from to is the abelian group .
Facts & Assumptions
Given: Abelian groups .
In a right-closed monoidal category, an internal hom is determined by its evaluation-transposition bijection (The internal hom and its evaluation morphism).
The Hom-tensor adjunction holds for modules over a commutative ring, hence for abelian groups (Hom-tensor adjunction: ).
Verification
The evaluation morphism is the group homomorphism , . It is bilinear, so it is well defined.
By Hom-tensor adjunction: , for every abelian group there is a natural isomorphism . This is exactly the transposition property from The internal hom and its evaluation morphism.
Therefore is the internal hom in .
The exponential of two small categories computed on a walking-arrow source
Example
Let be the walking-arrow category with objects and one nonidentity arrow . For any small category , a functor is exactly an arrow of .
Facts & Assumptions
Given: The walking-arrow category and a small category .
In , the exponential by is the functor category (The category of small categories is cartesian closed).
Verification
To give a functor is to choose the two objects and the image . Thus the objects of the exponential are precisely the arrows of .
A morphism between two such functors is a natural transformation, so it is exactly a commutative square in . Therefore is the arrow category of .
This is the concrete exponential object described by The category of small categories is cartesian closed: functors curry to functors .
A slice of Set computed as a locally cartesian closed category
Example
Let be the function with , , and
Let have fibers , , and .
Facts & Assumptions
Given: The displayed finite sets and maps over and .
is locally cartesian closed, so each pullback functor has a right adjoint (Set is locally cartesian closed).
Slice objects and pullback functors are defined as in Slice categories, composition, and pullback along a morphism.
Verification
The dependent product has fiber over equal to and fiber over equal to . So has three elements in total, two over and one over .
If is the singleton fiber over , then is the singleton fiber over , and a map over is exactly a choice of an element of , namely . This matches maps over , which must choose the unique element over .
This concrete fiber computation realizes the pullback/right-adjoint pattern guaranteed by Set is locally cartesian closed, using the slice formalism of Slice categories, composition, and pullback along a morphism.
The subobject classifier in a presheaf category on the walking arrow
Example
Let be the walking-arrow category , and work in the presheaf category . The subobject classifier sends an object to its set of sieves:
- ,
- .
The truth morphism selects the maximal sieve at each object. For any presheaf and subpresheaf , its characteristic morphism is
Facts & Assumptions
Given: The walking-arrow category , the sieve presheaf , and the subpresheaf defined below.
A subobject classifier classifies subobjects by pullback of truth (Subobject classifier).
Verification
On the walking arrow, the arrows into are only , so its sieves are and . The arrows into are and , and downward closure forces any sieve containing also to contain , giving exactly the three displayed sieves on . Pullback of sieves makes a presheaf, and the maximal sieves define the natural truth morphism above.
Consider the representable presheaf (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding) and the subpresheaf defined by and . Its characteristic map sends the unique element to the maximal sieve , and sends to the sieve .
For a general subpresheaf , the displayed formula defines a sieve and is natural under restriction. Moreover is maximal exactly when : the forward implication tests , and the reverse follows from closure of the subpresheaf under restriction. Thus pulling back along recovers , and this condition uniquely determines . By [L1], is a subobject classifier.
For the concrete of step 2.1, that pullback includes at object because is maximal, and excludes at object because is not maximal. Hence the general classifier calculation gives exactly the displayed example.
Sources
- Emily Riehl, Category Theory in Context, 2nd ed., Example 4.4.9
- S. Mac Lane, Categories for the Working Mathematician, 2nd ed., IV.6
- Emily Riehl, Category Theory in Context, 2nd ed., Example 4.4.15
- Hom-tensor adjunction for modules
- Tom Leinster, Basic Category Theory, Example 6.3.17
- Emily Riehl, Category Theory in Context, 2nd ed., Section 4.6
- Tom Leinster, Basic Category Theory, Exercise 6.3.27
- S. Mac Lane, Categories for the Working Mathematician, 2nd ed., IV.9