internalization and categorical algebra
algebra object (associative, Lie, …)
internal category ($\to$ more)
Any mathematical structure whose traditional Bourbaki-style definition is formulated within set theory can be formulated internally to any category that admits all those types of operations (typically: universal constructions) on its objects that the traditional definition applies to sets, hence to the objects of the base category of Sets.
There is a diagrammatic and a syntactic way of making this precise, the former is essentially the topic of categorical algebra (in terms of Lawvere theories or sketches or the like), the latter of categorical semantics (of type theories).
An archetypical example of internalization is the notion of internal groups, which easily serves to illustrate the general idea:
Where the Bourbaki-style definition of a group is, of course:
one observes that here:
sets and functions are the objects and morphisms in the category of Sets;
in invoking the singleton set $\ast$ and the Cartesian product set $G \times G$ one is making use of the fact that Sets admit the universal construction of finite products;
and that this is only structure on Sets that the definition of groups is making use of. Therefore, we may abstract away from Sets, consider any category $\mathcal{C}$ with finite products and declare that:
An internal group in $\mathcal{C}$ is an object $G$ of $\mathcal{C}$ equipped with morphisms $e \colon \ast \to G$ (i.e. out of the terminal object) and $M \colon G \times G \to G$ (i.e. out of the Cartesian product-object) and $(-)^{-1} \colon G \to G$ such that the following diagrams commute in $\mathcal{C}$:
If here $\mathcal{C} =$ Sets then this recovers the Bourbaki-definition of plain groups, while if $\mathcal{C} =$ TopologicalSpaces this yields the notion of topological groups; for $\mathcal{C} =$ SmoothManifolds it yields Lie groups, for $\mathcal{C} =$ Varieties it yields algebraic groups, etc.
Similarly one defines internal actions of internal groups, formally principal actions, etc.
In fact, realizing that groups are equivalently pointed connected groupoids one may readily generalize the example of internal groups to a notion of internal groupoids and then of internal categories. This way category theory and with it much of mathematics may be considered internally to suitable ambient categories $\mathcal{C}$ (see also at internal logic and internal language).
Moreover, if the ambient category is in fact a higher category, then internalization goes along with (vertical) categorification. For example an internal group in the 2-category of Groupoids is a 2-group (a strict 2-group if one considers just the three diagrams shown above, or a general 2-group of one adds higher coherence-diagrams.)
How much mathematics/internal logic actually exists in a given ambient category depends on how much extra properties this has. For example if $\mathcal{C}$ is a topos then all constructive mathematics has an internal incarnation in $\mathcal{C}$. For more on this see also at relation between type theory and category theory.
Here is a list matching some extra structure/property of the ambient category $\mathcal{C}$ to the kind of mathematics that exists internal to it:
If the ambient category is equipped with the structure of a site, then geometrical notions, such as defining morphisms locally on the domain with patching conditions (or more generally descent theory), exist inside it.
If it is a finitely complete category, the existence of finite products and terminal objects means that varieties of algebras can be defined.
If the category is a topos with a natural numbers object, then one can do a certain sort of “ordinary” mathematics inside it, specifically impredicative constructive mathematics without the fancier tools of model theory or (ironically) category theory.
Further extra conditions on the category, such as being a Boolean topos or being a superextensive site, bring the internal mathematics closer to that of $Set$.
If the category is a (infinity,1)-topos, then one could do most of ordinary constructive mathematics inside of it, including category theory, set theory, model theory, and higher category theory. Adding the principle of excluded middle or the axiom of choice set/0-groupoids results in internal classical mathematics.
The extra structure required on the ambient category $\mathcal{C}$ is sometimes referred to as a doctrine for internalization. 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 the process of internalization in a doctrine, although there are one or two fairly general theorems. However, its reverse is precise: given a doctrine $\mathcal{D}$ to which Sets (or some canonical Set-like category) belongs and a definition of foo internalized in the doctrine $\mathcal{D}$, if this definition of foo in $Sets$ 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 (monoid objects). 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.
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.
internal category, internal diagram, internal groupoid, groupoid object in an (∞,1)-category, category object in an (∞,1)-category
The notion of internalization with focus on H-spaces, internal monoids and internal groups (and proving the Eckmann-Hilton argument) originates with:
Beno Eckmann, Peter Hilton, Structure maps in group theory, Fundamenta Mathematicae 50 (1961), 207-221 (doi:10.4064/fm-50-2-207-221)
Beno Eckmann, Peter Hilton, Group-like structures in general categories I. Multiplications and comultiplications, Math. Ann. 145, 227–255 (1962) (doi:10.1007/BF01451367)
Beno Eckmann, Peter J. Hilton, Group-like structures in general categories II. Equalizers, limits, lengths. Mathematische Annalen 151:2 (1963), 150–186. doi:10.1007/bf01344176.
Beno Eckmann, Peter Hilton, Group-like structures in general categories III. Primitive categories, Math. Ann. 150 165–187 (1963) (doi:10.1007/BF01470843)
Highlighting the role of the Yoneda lemma in internalization:
Moreover with discussion of action objects:
Saunders Mac Lane, Ieke Moerdijk, Section V.6 of: Sheaves in Geometry and Logic, Springer 1992 (doi:10.1007/978-1-4612-0927-0)
Francis Borceux, George Janelidze, Gregory Maxwell Kelly, around p. 8 of: Internal object actions, Commentationes Mathematicae Universitatis Carolinae (2005) Volume: 46, Issue: 2, page 235-255 (dml:249553)
Discussion of internal categories is often attributed to originate around (though the simple idea can hardly be recognized here):
Basics of modern internal category theory (internal categories, internal functors, internal limits, internal sites) is discussed (without any attribution as to its origins) in:
Francis Borceux, Chapter 8 in Vol 1 Basic Category Theory of: Handbook of Categorical Algebra, Cambridge University Press (1994) (doi:10.1017/CBO9780511525858)
Peter Johnstone, Chapter B2 in: Vol. 1 of: Sketches of an Elephant – A Topos Theory Compendium, Oxford University Press (2002)(ISBN:9780198534259)
More general internalization via sketches:
Andrée Bastiani, Charles Ehresmann, Categories of sketched structures, Cahiers de Topologie et Géométrie Différentielle Catégoriques, Tome 13 (1972) no. 2, pp. 104-214 (numdam:CTGDC_1972__13_2_104_0)
Michael Barr, Charles Wells, Section 4 of: Toposes, Triples, and Theories, Originally published by: Springer-Verlag, New York, 1985, republished in: Reprints in Theory and Applications of Categories, No. 12 (2005) pp. 1-287
For more see at:
Last revised on April 16, 2021 at 10:03:43. See the history of this page for a list of all contributions to it.