Many structures whose “traditional” definition takes place in Set (or some other familiar category) can be formulated “internally” to any other category (or categorical structure) $C$ with “enough structure.”
The structure required on $C$ is often referred to as a doctrine. The question of what exactly a “doctrine” is is a tricky one, but for purposes of this page, we take a “doctrine” to mean a certain type of structure (or property-like structure) with which a category can be equipped. For example, there is a doctrine of monoidal categories, a doctrine of categories with finite limits, a doctrine of cartesian closed categories, and so on.
Like categorification or oidification, there is currently no completely general formal definition of this process, although there are one or two fairly general theorems. However, its reverse is precise: given a doctrine $D$ to which $\Set$ (or some canonical Set-like category) belongs and a definition of foo internalized in the doctrine $D$, if this definition of foo in $\Set$ reduces to the usual definition of foo, then the definition is acceptable; foos are a deinternalisation of internal foos.
Monoids can be internalized in the doctrine of monoidal categories. For example:
Since any category with finite products is a cartesian monoidal category, monoids can also be internalized in the doctrine of categories with finite products.
Groups can also be internalized in the doctrine of categories with finite products, but not in the doctrine of monoidal categories, since diagonal maps are necessary to define what it means to have inverses.
Monoids can also be internalized in the doctrine of multicategories.
Commutative monoids can be internalized in the doctrine of symmetric monoidal categories.
Categories and groupoids can be internalized in the doctrine of lex categories, producing the notion of internal category.
Rings can be internalized in the doctrine of categories with finite products.
More generally, the algebras for any Lawvere theory can be internalized in the doctrine of categories with finite products, and the algebras for any (symmetric) operad (in $Set$) can be internalized in the doctrine of (symmetric) monoidal categories.
Pretty much any structure at all in mathematics can be internalized in a topos. Note, though, that since the internal logic of a topos is constructive, differences in axiomatization that make no difference classically can result in actual differences in behavior in a topos. See constructive mathematics for some examples. On the other hand, if the topos satisfies the axiom of choice (and in particular is Boolean), then this complication won't happen.
Categories themselves can be internalised, as algebras of an essentially algebraic theory (giving strict categories), in any finitely complete category; see internal category.
In the case of categories, there is a dichotomy between internal categories and enriched categories, both of which are ways of generalizing the notion of category. In some cases, one is a special case of the other, but in general they are incomparable.
As described on this page, internalization is a quite general phenomenon, of which internal categories are a particular case. However, the distinction between “internalization” and “enrichment” becomes less clear in generality. For example, in addition to categories enriched over a monoidal category, one can define categories enriched over a bicategory or an virtual double category. It then turns out that a category enriched over the bicategory (or virtual double category) of spans in a lex category $C$ which has one object is precisely an internal category in $C$.
Perhaps from the perspective of this page, internal categories and enriched categories are just two different ways of internalizing the notion of category in two different doctrines?
Often, the structure on the ambient category $C$ allowing a certain type of structure to be internalized in it is itself a categorified version of that same structure (for example, monoids in monoidal categories). This is an example of the microcosm principle.
As one formal result along these lines, Tom Leinster has shown that for any cartesian monad $T$, $T$-algebras can be naturally internalized/enriched in $T$-multicategories, and in particular in $T$-structured categories. For example, when $T$ is the monad whose algebras are monoids, this says that monoids can be internalized in multicategories and monoidal categories.
On the other hand, this is not always true. For example, the categorification of a rig is a rig category, but it is difficult to see how to define a rig internal to a rig category, and the usual definition of rig in $Set$ does not use the rig-category structure of $Set$ but only that it has finite products.
A very different sort of general result has to do with the internal logic of certain categories. If a category has enough structure to interpret a certain fragment of first-order logic, then any first-order theory definable in that fragment can be internalized in that category. For example, the theory of categories can be formulated in cartesian logic and thus is interpretable in any cartesian (= lex) category. The statement that almost anything can be internalized in a topos is the high-end case of this, since the internal logic of a topos is full intuitionistic type theory.
Last revised on May 13, 2019 at 16:56:03. See the history of this page for a list of all contributions to it.