In category theory, the hom-sets between two objects can often be equipped with some extra structure which is respected
by identities and composition. For example, the set of group homomorphisms between two abelian groups is itself an abelian group by defining
the operations pointwise. Similarly, the set of monotonic functions between two partially ordered sets (posets) is a poset
again by defining the ordering pointwise. Linear functions between vector spaces form a vector space. The set of functors
between small categories is a small category. Of course, the structure
on the hom-sets can be different than the objects. Trivially, with the earlier examples a vector space is an abelian group, so we could
say that linear functions form an abelian group instead of a vector space. Likewise groups are monoids. Less trivially, the set of relations
between two sets is a partially ordered set via inclusion. There are many cases where instead of hom-sets we have hom-objects that
aren’t naturally thought of as sets. For example, we can have hom-objects be non-negative (extended) real numbers from which
the category laws become the laws of a generalized metric space. We can identify posets with categories who hom-objects are elements
of a two element set or, even better, a two element poset with one element less than or equal to the other.
This general process is called enriching a category in some other
category which is almost always called in the generic
case. We then talk about having -categories and -functors, etc. In a specific case, it will be something
like -categories for an -enriched category, where is the category of abelian groups.
Unsurprisingly, not just any category will do for . However, it turns out very little structure is needed to define
a notion of -category, -functor, -natural transformation, and -profunctor. The
usual “baseline” is that is a monoidal category. As mentioned in the previous
post, paraphrasing Bénabou, notions of “families of objects/arrows” are ubiquitous and fundamental in category theory. It is useful for
our purposes to make this structure explicit. For very little cost, this will also provide a vastly more general notion that will readily
capture enriched categories, indexed categories, and categories that are simultaneously
indexed and enriched, of which internal categories are an example. The tool for this is
a (Grothendieck) fibration aka a fibered category or the mostly equivalent concept
of an indexed category.1
To that end, instead of just a monoidal category, we’ll be using indexed monoidal categories.
Typically, to get an experience as much like ordinary category theory as possible, additional structure is assumed on . In
particular, it is assumed to be an (indexed) cosmos which means
that it is an indexed symmetric monoidally closed category with indexed coproducts preserved by and indexed products
and fiberwise finite limits and colimits (preserved by the indexed structure). This is quite a lot more structure which I’ll introduce
in later parts. In this part, I’ll make no assumptions beyond having an indexed monoidal category.
Basic Category Theory in Indexed Monoidal Categories
The purpose of the machinery of the previous posts is to make this section seem boring and pedestrian. Other than being
a little more explicit and formal, for most of the following concepts it will look like we’re restating the usual definitions
of categories, functors, and natural transformations. The main exception is profunctors which will be presented in a quite different
manner, though still in a manner that is easy to connect to the usual presentation. (We will see how to recover the usual presentation
in later parts.)
While I’ll start by being rather explicit about indexes and such, I will start to suppress that detail over time as most of it
is inferrable. One big exception is that right from the start I’ll omit the explicit dependence of primitive terms on indexes.
For example, while I’ll write for the first functor law, what the syntax of the previous
posts says I should be writing is .
To start, I want to introduce two different notions of -category, small -categories and large -categories,
and talk about what this distinction actually means. I will proceed afterwards with the “large” notions, e.g. -functors between
large -categories, as the small case will be an easy special case.
Small -categories
The theory of a small -category consists of:
an index type ,
a linear type ,
a linear term , and
a linear term
satisfying
In the notation of the previous posts, I’m saying , ,
, and
are primitives added to the signature of the theory. I’ll continue to use the earlier, more pointwise presentation above to
describe the signature.
A small -category for an -indexed monoidal category is then an interpretation of
this theory. That is, an object of as the interpretation of , and an
object of as the interpretation of . The interpretation of
is an arrow of , where is the diagonal
arrow in . The interpretation of is an
arrow of
where are the appropriate projections.
Since we can prove in the internal language that the choice of for ,
for , for ,
and for
satisfies the laws of the theory of a small -category, we know we have a -category which I’ll call
for any 2.
For , is a set of objects. is an -indexed family of objects of
which we can write . The interpretation of is an -indexed family of arrows
of , . Finally, the interpretation of is a family of arrows
of , . This is exactly
the data of a (small) -enriched category. One example is when which
produces (strict) -categories.
For , is an object of . is an arrow of into , i.e.
an object of . I’ll write the object part of this as as well, i.e. . The idea
is that the two projections are the target and source of the arrow. The interpretation of is an arrow
such that , i.e. the arrow produced by should have the same target and source. Finally, the interpretation
of is an arrow from the pullback of and to . The source of this arrow is the
object of composable pairs of arrows. We further require to produce an arrow with the appropriate target and source of the
composable pair. This is exactly the data for a category internal to . An interesting case for contrast with the
previous paragraph is that a category internal to is a double category.
For , the above data is exactly the data of a monoid object
in . This is a formal illustration that a (-enriched) category is just an “indexed monoid”.
Indeed, -functors will be monoid homomorphisms and -profunctors
will be double-sided monoid actions. In particular, when , we get rings, ring homomorphisms,
and bimodules of rings. The intuitions here are the guiding ones for the construction we’re realizing.
One aspect of working in a not-necessarily-symmetric (indexed) monoidal category is the choice of the standard
order of composition or diagrammatic order is not so trivial since it is not possible to even state what it
means for them to be the equivalent. To be clear, this definition isn’t really taking a stance on the issue.
We can interpret as the type of arrows and then will be the standard
order of composition, or as the type of arrows and then will be the diagrammatic order.
In fact, there’s nothing in this definition that stops us from having being the type
of arrows while still having be standard order composition as usual. The issue comes up
only once we consider -profunctors as we will see.
Large -categories
A large -category is a model of a theory of the following form. There is
a collection of index types ,
for each pair of index types and , a linear type ,
for each index type , a linear term , and
for each triple of index types, , , and , a linear term
satisfying the same laws as small -categories, just with some extra subscripts. Clearly, a small -category
is just a large -category where the collection of index types consists of just a single index type.
Small versus Large
The typical way of describing the difference between small and large (-)categories would be to say something like: “By
having a collection of index types in a large -category, we can have a proper class of them. In a
small -category, the index type of objects is interpreted as an object in a category, and a proper class can’t
be an object of a category3.” However, for us, there’s
a more directly relevant distinction. Namely, while we had a single theory of small -categories, there is no
single theory of large -categories. Different large -categories correspond to models of (potentially) different theories.
In other words, the notion of a small -category is able to be captured by our notion of theory but not the concept
of a large -category. This extends to -functors, -natural transformations,
and -profunctors. In the small case, we can define a single theory which captures each of these concepts,
but that isn’t possible in the large case. In general, notions of “large” and “small” are about what we can internalize
within the relevant object language, usually a set theory. Arguably, the only reason we speak of “size” and of proper
classes being “large” is that the Axiom of Specification
outright states that any subclass of a set is a set, so proper classes in ZFC can’t be subsets of any set.
As I’ve mentioned elsewhere, you can definitely have set theories with proper classes that are
contained in even finite sets, so the issue isn’t one of “bigness”.
The above discussion also explains the hand-wavy word “collection”. The collection is a collection in the meta-language in
which we’re discussing/formalizing the notion of theory. When working within the theory of a particular
large -category, all the various types and terms are just available ab initio and are independent. There is
no notion of “collection of types” within the theory and nothing indicating that some types are part of a “collection” with others.
Another perspective on this distinction between large and small -categories is that small -categories have
a family of arrows, identities, and compositions with respect to the notion of “family” represented by our internal
language. If we hadn’t wanted to bother with formulating the internal language of an indexed monoidal category, we
could have still defined the notion of -category with respect to the internal language of a (non-indexed) monoidal
category. It’s just that all such -categories (except for monoid objects) would have to be large -categories. That is,
the indexing and notion of “family” would be at a meta-level. Since most of the -categories of interest will be
large (though, generally a special case called a -fibration which reins in the size a bit), it may seem that there
was no real benefit to the indexing stuff. Where it comes in, or rather where small -categories come in, is that
our notion of (co)complete means “has all (co)limits of small diagrams” and small diagrams are -functors from
small -categories.4 There are several other places, e.g. the notion
of presheaf, where we implicitly depend on what we mean by “small -category”. So while we won’t usually be
focused on small -categories, which -categories are small impacts the structure of the whole theory.
-functors
The formulation of -functors is straightforward. As mentioned before, I’ll only present the “large” version.
Formally, we can’t formulate a theory of just a -functor, but rather we need to formulate a
theory of “a pair of -categories and a -functor between them”.
A -functor between (large) -categories and is a model of
a theory consisting of a theory of a large -category, of which is a model, and a theory
of a large -category which I’ll write with primes, of which is a model, and model of
the following additional data:
for each index type , an index type and
an index term, , and
for each pair of index types, and , a linear term
satisfying
The assignment of for is, again, purely metatheoretical. From within the theory, all we know
is that we happen to have some index types named and and some data relating them. The fact
that there is some kind of mapping of one to the other is not part of the data.
Next, I’ll define -natural transformations . As before, what we’re really doing is defining -natural transformations
as a model of a theory of “a pair of (large) -categories with a pair of -functors between them and a -natural transformation
between those”. As before, I’ll use primes to indicate the types and terms of the second of each pair of subtheories. Unlike
before, I’ll only mention what is added which is:
for each index type , a linear term
satisfying
In practice, I’ll suppress the subscripts on all but index types as the rest are inferrable. This makes the above equation the
much more readable
-profunctors
Here’s where we need to depart from the usual story. In the usual story, a -enriched profunctor
is
a -enriched functor (or, often, the opposite
convention is used ). There are many problems with this
definition in our context.
Without symmetry, we have no definition of opposite category.
Without symmetry, the tensor product of -enriched categories doesn’t make sense.
is not itself a -enriched category, so it doesn’t make sense to talk
about -enriched functors into it.
Even if it was, we’d need some way of converting between arrows of as a category and
arrows of as a -enriched category.
The equation requires symmetry. (This is arguably
2 again.)
All of these problems are solved when is a symmetric monoidally closed category.
Alternatively, we can reformulate the notion of a -profunctor so that it works in our context
and is equivalent to the usual one when it makes sense.5 To this end, at a low level a -enriched profunctor is a family of
arrows which
satisfies in the internal language of a symmetric
monoidally closed category among other laws. We can uncurry to eliminate the need for closure,
getting
satisfying We see that we’re always going to need
to permute and past unless we move the third argument to the second producing the
nice and the
law which no longer requires symmetry. This is
also where the order of the arguments of drives the order of the arguments of -profunctors.
A -profunctor, , is a model of the theory (containing
subtheories for and etc. as in the -functor case) having:
for each pair of index types and ,
a linear type , and
for each quadruple of index types , , , and ,
a linear term
satisfying
This can also be equivalently presented as a pair of a left and a right action satisfying bimodule laws. We’ll make
the following definitions
and .
A -presheaf on is a -profunctor . Similarly,
a -copresheaf on is a -profunctor .
Of course, we have the fact that the term witnesses the interpretation of as a -profunctor
for any -category, , which we’ll call the hom -profunctor. More generally, given
a -profunctor , and -functors
and , we have the -profunctor
defined as In particular, we have the representable -profunctors when is the hom -profunctor and
either or is the identity -functor, e.g. or .
Multimorphisms
There’s a natural notion of morphism of -profunctors which we could derive either via passing the notion of
natural transformation of the bifunctorial view through the same reformulations as above, or by generalizing the notion of
a bimodule homomorphism. This would produce a notion like: a -natural transformation from
is a satisfying . While there’s nothing wrong
with this definition, it doesn’t quite meet our needs. One way to see this is that it would be nice to have a bicategory
whose -cells were -categories, -cells -profunctors, and -cells -natural
transformations as above. The problem there isn’t the -natural transformations but the -cells. In particular,
we don’t have composition of -profunctors. In the analogy with bimodules, we don’t have tensor products so we
can’t reduce multilinear maps to linear maps; therefore, linear maps don’t suffice, and we really want a notion of multilinear maps.
So, instead of a bicategory what we’ll have is a virtual bicategory (or, more generally, a virtual double category).
A virtual bicategory is to a bicategory what a multicategory is to a monoidal category, i.e. multicategories are “virtual monoidal
categories”. The only difference between a virtual bicategory and a multicategory is that instead of our multimorphisms having
arbitrary lists of objects as their sources, our “objects” (-cells) themselves have sources and targets (-cells) and our
multimorphisms (-cells) have composable sequences of -cells as their sources.
A -multimorphism from a composable sequence of -profunctors to
the -profunctor is a model of the theory consisting of the various necessary subtheories and:
a linear term,
satisfying
except for the case in which case the only law is
The laws involving the action of are called external equivariance, while the remaining law is called internal
equivariance. We’ll write for the set of -multimorphisms from the
composable sequence of -profunctors to the -profunctor .
As with multilinear maps, we can characterize composition via a universal property. Write
for the composite -profunctor (when it exists) of the composable sequence . We then have
for any pair of composable sequences and which compose with ,
where the forward direction is induced by precomposition with a -multimorphism
. A -multimorphism with this property
is called opcartesian. The case is particularly important and, for a -category ,
produces the unit -profunctor, as the composite
of the empty sequence. When we have all composites, becomes an actual bicategory rather
than a virtual bicategory. always has all units, namely the hom -profunctors. Much like we
can define the tensor product of modules by quotienting the tensor product of their underlying abelian groups by internal
equivariance, we will find that we can make composites when we have enough (well-behaved) colimits6.
Related to composites, we can talk about left/right closure of . In this case we have the
natural isomorphisms: Like composites, this merely characterizes these constructs; they need not exist in general.
These will be important when we talk about Yoneda and (co)limits in -categories.
A -natural transformation is the same as .
Example Proof
Just as an example, let’s prove a basic fact about categories for arbitrary -categories. This will use an informal
style.
The fact will be that full and faithful functors reflect isomorphisms. Let’s go through the typical proof for the ordinary
category case.
Suppose we have an natural transformation natural in and such that
is an inverse to , i.e. the action of the functor on arrows. If and , then by the naturality
of , and similarly with and switched.
We now just need to show that but , so .
Now in the internal language. We’ll start with the theory of a -functor, so we have , , , , and .
While the previous paragraph talks about a natural transformation, we can readily see that it’s really a multimorphism. In our case, it
is a -multimorphism from to . Before we do that though, we need to show that
itself is a -multimorphism. This corresponds to the naturality of the action on arrows of which we took for granted in the previous
paragraph. This is quickly verified: the external equivariance equations are just the functor law for composites. The additional data we have
is two linear terms and such that
and . Also, .
The result follows through almost identically to the previous paragraph.
,
we apply external equivariance twice to get . The functor law for
gives . A quick glance verifies that all these
equations use their free variables linearly as required.
As a warning, in the above and are not free variables but constants, i.e. primitive linear terms. Thus
there is no issue with an equation like as both sides have no free variables.
This is a very basic result but, again, the payoff here is how boring and similar to the usual case this is. For contrast, the definition
of an internal profunctor is given here. This definition is easier to
connect to our notion of -presheaf, specifically a -presheaf, than it is to the usual -valued
functor definition. While not hard, it would take me a bit of time to even formulate the above proposition, and a proof in terms
of the explicit definitions would be hard to recognize as just the ordinary proof.
For fun, let’s figure out what the case of this result says explicitly.
A -category is a ring, a -functor is a ring homomorphism, and
a -profunctor is a bimodule. Let and be rings
and be a ring homomorphism. An isomorphism in viewed as a -category is just
an invertible element. Every ring, , is an --bimodule. Given any --bimodule , we have
an --bimodule via restriction of scalars, i.e. has the same elements as and for ,
. In particular, gives rise to a bimodule homomorphism, i.e. a linear function,
which corresponds to its action on arrows from the perspective of as a -functor. If this
linear transformation has an inverse, then the above result states that when is invertible so is . So to restate this
all in purely ring theoretic terms, given a ring homomorphism and an abelian group homomorphism
satisfying and , then if is invertible so is .
Indexed categories are equivalent to cloven fibrations and, if you have the Axiom of Choice, all fibrations can
be cloven. Indexed categories can be viewed as presentations of fibrations.↩︎
This
suggests that we could define a small -category where and
are small -categories. Start formulating a definition of such a -category. You will get stuck. Where? Why? This implies
that the (ordinary, or better, 2-)category of small -categories does not have a monoidal product with as
unit in general.↩︎
With a good understanding of what a class is, it’s clear that it doesn’t even make
sense to have a proper class be an object. In frameworks with an explicit notion of ”class”, this is often manifested by
saying that a class that is an element of another class is a set (and thus not a proper class).↩︎
This suggests that it might be interesting to consider categories that are (co)complete with
respect to this monoid notion of “small”. I don’t think I’ve ever seen a study of such categories. (Co)limits of
monoids are not trivial.↩︎
This is one of the main things I like about working
in weak foundations. It forces you to come up with better definitions that make it clear what is and is not
important and eliminates coincidences. Of course, it also produces definitions and theorems that are inherently
more general too.↩︎
This connection isn’t
much of a surprise as the tensor product of modules is exactly the (small) case of this.↩︎