nLab
internalization

Contents

Contents

Idea

Any mathematical structure whose traditional Bourbaki-style definition is formulated within set theory can be formulated internally (Grothendieck 1960, 61) 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.

This internalization serves to combine mathematical structures in a compatible way. For example a group object internal to the category Top of topological spaces is a topological group (while internal to Sets it is just a discrete group).

There is a diagrammatic and a syntactic way of systematizing the process of internalization: The former is essentially the topic of categorical algebra, in terms of Lawvere theories (Lawvere 1963) or, more generally, of sketches (Bastiani & Ehresmann 1972), the latter of categorical semantics of type theories.

An archetypical example of internalization is the notion of internal groups (e.g. Eckmann & Hilton 1961), which easily serves to illustrate the general idea:

Where the Bourbaki-style definition of a group is, of course:

  • A group is a set GG equipped with functions e:*Ge \,\colon\,\ast \to G and m:G×GGm \colon G \times G \to G and () 1:GG(-)^{-1} \colon G \to G satisfying three conditions: unitality, associativity, inverses.

one observes that here:

  1. sets and functions are the objects and morphisms in the category of Sets;

  2. in invoking the singleton set *\ast and the Cartesian product set G×GG \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 GG of 𝒞\mathcal{C} equipped with morphisms e:*Ge \colon \ast \to G (i.e. out of the terminal object) and M:G×GGM \colon G \times G \to G (i.e. out of the Cartesian product-object) and () 1:GG(-)^{-1} \colon G \to G such that the following diagrams commute in 𝒞\mathcal{C}:

    • unitality

      G×* id×e G×G m G = G*×G e×id G×G m G = G \array{ G \times \ast & \overset{ id \times e }{\longrightarrow} & G \times G \\ {}^{\mathllap{ \simeq }} \big\downarrow && \big\downarrow {}^{{}_{\mathrlap{ m }}} \\ G &=& G } \;\;\;\;\;\;\;\; \array{ \ast \times G & \overset{ e \times id }{\longrightarrow} & G \times G \\ {}^{\mathllap{ \simeq }} \big\downarrow && \big\downarrow {}^{{}_{\mathrlap{ m }}} \\ G &=& G }
    • associativity

      G×G×G m×id G×G id×m m G×G m G \array{ G \times G \times G &\overset{m \times id}{\longrightarrow}& G \times G \\ {}^{{}_{\mathllap{ id \times m }}} \big\downarrow && \big\downarrow {}^{{}_{m}} \\ G \times G &\underset{ m }{\longrightarrow}& G }
    • inverses

      G diag G×G id×() 1 G×G m * e GG diag G×G () 1×id G×G m * e G \array{ G & \overset{ diag }{ \longrightarrow } & G \times G & \overset{ id \times (-)^{-1} }{\longrightarrow} & G \times G \\ & \searrow & && \big\downarrow {}^{_{\mathrlap{m}}} \\ && \ast & \underset{ e }{\longrightarrow} & G } \;\;\;\;\;\;\;\;\; \array{ G & \overset{ diag }{ \longrightarrow } & G \times G & \overset{ (-)^{-1} \times id }{\longrightarrow} & G \times G \\ & \searrow & && \big\downarrow {}^{_{\mathrlap{m}}} \\ && \ast & \underset{ e }{\longrightarrow} & G }

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:

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 SetsSets reduces to the usual definition of foo, then the definition is acceptable; foos are a deinternalization, or externalization, of internal foos.

Examples

  • Monoids can be internalized in the doctrine of monoidal categories (monoid objects). For example:

    • A ring is a monoid object in Ab with its usual tensor product.

    • An algebra is a monoid internal to Vect, with its usual tensor product.

    • A strict monoidal category is a monoid internal to Cat, with its cartesian product.

  • 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.

    • The classical fact that monoids can be identified with one-object categories has the following internal analogue: monoids in a lex category CC (qua category with finite products) can be identified with categories internal to CC whose object-of-objects is terminal. However, monoids in a non-cartesian monoidal category (such as AbAb or VectVect) cannot, in general, be identified with any sort 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 SetSet) 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.

General Results

Often, the structure on the ambient category CC 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 TT, TT-algebras can be naturally internalized/enriched in TT-multicategories, and in particular in TT-structured categories. For example, when TT 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 SetSet does not use the rig-category structure of SetSet 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.

Examples

References

The general notion of internalization is due to

  • Alexander Grothendieck, p. 370 (3 of 23) in: FGA Technique de descente et théorèmes d’existence en géométrie algébriques. II: Le théorème d’existence en théorie formelle des modules, Séminaire Bourbaki : années 1958/59 - 1959/60, exposés 169-204, Séminaire Bourbaki, no. 5 (1960), Exposé no. 195 (numdam:SB_1958-1960__5__369_0, pdf, English translation: pdf, web version).

with specialization to internal groups, internal actions, internal categories and internal groupoids made explicit in:

Discussion with focus on H-spaces, internal monoids and internal groups and proving the Eckmann-Hilton argument originates with:

Highlighting the role of the Yoneda lemma in internalization:

Moreover with discussion of action objects:

Discussion of internal categories is often attributed to originate around (though the simple idea can hardly be recognized here):

Review of internal category theory (internal categories, internal functors, internal limits, internal sites), typically without attribution to more original sources:

More general internal internal algebraic structures, known as algebras over Lawvere theories originate with:

Yet more general internal structures via sketches:

For more see at:

Last revised on September 3, 2021 at 12:22:55. See the history of this page for a list of all contributions to it.