This page is about the notion of poly-morphism considered by Shinichi Mochizuki. For the concept in computer science see polymorphism. Or see universe polymorphism for the concept in type theory.
For a category , a poly-morphism is a collection of morphisms with common source and target, considered as a morphism in a new category with the same objects, but with hom-sets , the power set of the original hom-sets.
These play a substantive rôle in Shinichi Mochizuki‘s inter-universal Teichmüller theory (Mochizuki 12, section 0). Here we put these into the broader context of change of enriching categories along lax monoidal functors as the special case that is a power set-functor, or an equivariant version thereof.
In the following, fix a monoidal category and a -enriched category
Examples to keep in mind for are the category Set of sets considered as a cartesian monoidal category, or the category G-set for a given group , again with the cartesian monoidal structure.
Recall:
(change of enriching category from to itself)
For a lax monoidal functor from to itself, the image of under the corresponding change of enriching category is the -category with the same objects as , and with -hom objects given by
The composition-, unit-, associator- and unitor-morphisms of are the images of those of under suitably composed with the structure morphisms of the lax monoidal functor .
For the case of poly-morphisms the relevant lax monoidal functors are power set-functors
(lax monoidal power set-functors)
For Set equipped with its cartesian monoidal category structure, an arbitrary locally small category, take to be the covariant power set functor. This is lax monoidal since every pair of subsets and gives a subset .
For a group, GSet with the cartesian monoidal category structure, a category enriched in G-sets, let also be the covariant power set functor, but for a -set, equip with the -action
(poly-morphisms)
For a plain category and the power set-functor (Def. ), we write
for the image of under the change of enriching category (Def. ) along .
We say that the morphisms of are the poly-morphisms of .
Explicitly, this means composition is defined to be
and the unit map is
A poly-isomorphism of is defined to be a poly-morphism of the core of , hence a morphism of . Hence a poly-isomorphism is a collection of invertible morphisms of . (Note that these are not in general the isomorphisms in : all the isomorphisms in are actual isomorphisms in .)
The above construction for enrichment in plain sets is considered (without the above category-theoretic formulation) in:
The construction for enrichment in posets is considered in
Last revised on April 7, 2020 at 08:10:41. See the history of this page for a list of all contributions to it.