Throughout, let be a BΓ©nabou cosmos for enriched category theory.
(tensoring and cotensoring)
Let be a -enriched category.
A powering (or cotensoring) of over is
a functor
for each a natural isomorphism of the form
A copowering (or tensoring) of over is
a functor
for each a natural isomorphism of the form
If is equipped with a (co-)powering it is called (co-)powered over .
(tensoring left adjoint to cotensoring)
If is both tensored and cotensored over (Def. ), then for fixed the operations of tensoring with and of cotensoring with form a pair of adjoint functors
The hom-isomorphism characterizing the pair of adjoint functors is provided by the composition of the natural isomorphisms (1) and (2):
It follows that:
(in tensored and cotensored categories initial/terminal objects are enriched initial/terminal)
If is both tensored and cotensored over then
an initial object of the underlying category of is also enriched initial, in that the hom-object out of it is the terminal object of
a terminal object of the underlying category of is also enriched terminal, in that the hom-object into it is the terminal object of :
We discuss the first claim, the second is formally dual.
By prop. , tensoring is a left adjoint. Since left adjoints preserve colimits, and since an initial object is the colimit over the empty diagram, it follows that
for all , in particular for . Therefore the natural isomorphism (2) implies for all that
where in the last step we used that the internal hom in sends colimits in its first argument to limits (this prop.) and used that a terminal object is the limit over the empty diagram.
The symmetric closed monoidal category is tensored and cotensored over itself, with tensoring being its tensor product and powering being its internal hom.
For a small -enriched category, the -enriched category of enriched presheaves is tensored and cotensored (this Prop.)
Last revised on June 20, 2023 at 14:38:00. See the history of this page for a list of all contributions to it.