nLab poly-morphism


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 CC, a poly-morphism is a collection of morphisms with common source and target, considered as a morphism in a new category C polyC^{poly} with the same objects, but with hom-sets C poly(a,b)P(C(a,b))C^{poly}(a,b) \coloneqq P(C(a,b)), 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 FF as the special case that FF is a power set-functor, or an equivariant version thereof.

Abstract approach

In the following, fix a monoidal category VV and a VV-enriched category

CVCat. C \in V Cat \,.

Examples to keep in mind for VV are the category Set of sets considered as a cartesian monoidal category, or the category G-set for a given group GG, again with the cartesian monoidal structure.



(change of enriching category from VV to itself)

For F:VVF\colon V\to V a lax monoidal functor from VV to itself, the image F *(C)F_\ast(C) of CC under the corresponding change of enriching category is the VV-category with the same objects as CC, and with VV-hom objects given by

F *(C)(a,b)F(C(a,b)). F_\ast(C)(a,b) \coloneqq F(C(a,b)) \,.

The composition-, unit-, associator- and unitor-morphisms of F *(C)F_\ast(C) are the images of those of CC under PP suitably composed with the structure morphisms of the lax monoidal functor PP.

For the case of poly-morphisms the relevant lax monoidal functors are power set-functors


(lax monoidal power set-functors)



For CC a plain category and FP:SetSetF \coloneqq P \colon Set \to Set the power set-functor (Def. ), we write

C polyP *(C) C^{poly} \;\coloneqq\; P_\ast(C)

for the image of CC under the change of enriching category (Def. ) along PP.

We say that the morphisms of C polyC^{poly} are the poly-morphisms of CC.

Explicitly, this means composition is defined to be

C poly(a,b)C poly(b,c)=P(C(a,b))P(C(b,c))P(C(a,b)B(b,c))P(C(a,c))=C poly(a,c) C^{poly}(a,b) \otimes C^{poly}(b,c) = P(C(a,b)) \otimes P(C(b,c)) \to P(C(a,b)\otimes B(b,c)) \to P(C(a,c)) = C^{poly}(a,c)

and the unit map is

IP(I)P(C(a,a))=C poly(a,a). I \to P(I) \to P(C(a,a)) = C^{poly}(a,a) \,.

A poly-isomorphism of CC is defined to be a poly-morphism of the core of CC, hence a morphism of (Core(C)) poly(Core(C))^{poly}. Hence a poly-isomorphism is a collection of invertible morphisms of CC. (Note that these are not in general the isomorphisms in C polyC^{poly}: all the isomorphisms in C polyC^{poly} are actual isomorphisms in CC.)


The above construction for enrichment in plain sets is considered (without the above category-theoretic formulation) in:

  • Shinichi Mochizuki, section 0 of Inter-universal Teichmüller theory I, Construction of Hodge theaters (2012) (pdf)

The construction for enrichment in posets is considered in

  • Alveen Chand, Ittay Weiss, An ordered framework for partial multivalued functors, Computer Science and Engineering (APWC on CSE), 2015 2nd Asia-Pacific World Congress on Computer Science (arXiv:1511.00746)

Last revised on April 7, 2020 at 08:10:41. See the history of this page for a list of all contributions to it.