Homotopy Type Theory Seminar
Carnegie Mellon University
Categories and modalities for smoothness

Categories and modalities for smoothness

Greg Langmead

Differential cohesion and modal HoTT promise to give access to constructions from differential geometry. In this series of talks I will tell a story that takes us from the classical definition of a smooth manifold to differential cohesion in a category where we can interpret modal HoTT. I will assume only basic topology and category theory and will provide details that are sometimes waved away. I will also motivate the study of smooth manifolds as a worthy field with surprising results and tough open questions such as the smooth four-dimensional Poincaré conjecture.

1 Introduction

As someone “classically trained” in differential geometry, my recent adventures in homotopy type theory have made me very excited to explore an entirely new angle on a topic I love. It is the case today that modal HoTT allows us to access smoothness and prove theorems about manifolds, Lie groups and more. In order to participate in this new and exciting field, someone like me needs a bridge. More than one, in fact. The current document is intended as one of those bridges. Starting from the classical definition of a smooth manifold and the category containing these objects and the smooth maps between them, we will define several enlargements of the category until we arrive at something where modal HoTT can be interpreted.

To make the most of this process, we will always try to keep track of where smoothness is entering in. It’s not always obvious!

Definition 1.

A smooth manifold is a Hausdorff topological space M with countable basis, and with a maximal smooth atlas. An atlas is a covering of M by open sets Ui, each of which is the image of a homeomorphism fi:RnM (called a chart), such that fj-1fi is smooth wherever it is defined. Two atlases are compatible if their union is again an atlas. The maximal atlas is the union of all compatible atlases.

Note that this definition expresses M as a colimit of a diagram of arrows from nM, more specifically a pushout. More on this shortly.

A continuous function f:MN between two smooth manifolds is defined to be smooth if the appropriate composition with charts is a smooth function between cartesian spaces.

The category SmoothMfd has objects the smooth manifolds of any finite dimension, and morphisms the smooth maps.

This category, innocuous though it seems, has some strange properties! There are topological manifolds that are missing from it, and some that are way over-represented! You can’t just take a topological manifold and assume you can give it a unique maximal smooth atlas and stick it into SmoothMfd.

The table below contains some examples.

kind of manifold number of inequivalent smooth atlases
dim 3 1
dim 5 0, finite
n,n4 1
4 uncountably many
S4 unknown, 1
dim =4, compact without boundary 0, at most countably many
dim =4, otherwise 1, at most uncountably many

The claim that S4 has exactly one smooth structure is known as the four-dimensional smooth Poincaré conjecture. Its status is “extremely unknown”. For more of the beautiful story around four-dimensional topology and smooth structures see the accessible and detailed book by Scorpan [7].

The spheres behave surprisingly as well.

n number of inequivalent smooth atlases on Sn
1 1
2 1
3 1
4 1
5 1
6 1
7 28
8 2
9 8
10 6
11 992
12 1
13 3
14 2
15 16256
16 2
17 16
18 16
19 523264
20 24


Is SmoothMfd a nice category? It does have finite products (cartesian product) and coproducts (disjoint unions). Manifolds are themselves certain colimits. However in this category does not have all limits or colimits, nor is it cartesian closed.

For example, consider the equalizer {(x,y)|xy=0}2. As a set this must be equal to the union of the x-axis and y-axis. But this cannot be given the structure of a topological manifold nor a smooth one, due to the failure to be homeomorphic to any n at the origin. Full argument: the forgetful functor U:𝖲𝗆𝗈𝗈𝗍𝗁𝖬𝖿𝖽𝖲𝖾𝗍 preserves limits and colimits as it has both left and right adjoints. The equalizer as a set is this union of axes, and so the manifold must have that underlying set. But this set cannot be promoted to a smooth manifold.

Consider the coequalizer (2)/(0,0)0. Similarly this cannot be given the structure of a topological manifold nor a smooth one, also at the origin.

Is SmoothMfd cartesian closed, i.e. does it contain function spaces of smooth maps? This has been attempted with some success, but we’ll skip over that story because we’re going to do it with sheaves later. In fact right now.

2 Sheaves on CartSp

My take on presheaves and sheaves is inspired by Daniel Dugger’s informal notes Sheaves and Homotopy Theory[3]. His analogy to generators and relations is the one that clicked for me in this context.

Define CartSp to be the full subcategory of SmoothMfd containing just the n for finite n (recall that “full” means include every morphism). In the case of 4 let’s just bring the standard smooth structure. We can try to build the fake 4s later on with surgery and such.

Due to the existence of real-valued functions such as 11+e-x we can map all of  to the open interval (0,1). So note that this category is not as pitifully empty as I, at least, thought at first. You can cover n with balls each of which is a diffeomorphic image of n. We’ll be doing just that.

To generalize SmoothMfd we’ll use CartSp in a new way. In the original atlas-based definition of a smooth manifold we were characterizing manifolds by the slogan “locally isomorphic to n.” This is a way to cash out the more general concept “modeled on n.” But we will now shift to the paradigm “can be probed by n” or equivalently “has specified maps from the test spaces n.” In this framework we will specify probes from all dimensions of cartesian spaces, not just the one that has the same dimension as the manifold (if any such concept as dimension survives our shenanigans).

A presheaf on CartSp is a functor


Think of one presheaf M (suggestive name) as a would-be space together with the specification of what probing functions are smooth. Sometimes these probes are called plots. These are different from charts. Charts are specific homeomorphisms that cover M. Here we must provide the entire set of all possible smooth functions into M from n, for all n.

The category Psh(CartSp) consists of all such functors, together with the natural transformations between them. This is an interesting category! If C is any locally small category, there is an embedding (a full and faithful functor that is injective on objects) C𝖯𝗌𝗁(C) called the Yoneda embedding. In fact Psh(C) is the free cocompletion of C, meaning it freely adds all colimits from C. In fact Psh(C) is a topos which is a checklist of wonderful properties, and we’ll be using them all by the end because HoTT and toposes are closely related. In a nutshell, Psh(C) inherits these nice properties from 𝖲𝖾𝗍.


If C already has some colimits, Psh(C) will not respect these. It is too free.

Consider two subobjects of n in CartSp, say two disjoint open balls U and V.

Following Duggers we think of sheaves as the subcategory of presheaves that preserve the existing colimits that we had. There is an analogy to specifying a group as the quotient of a free group by a subgroup generated by some relations.

It’s illustrative to understand the layers of exoticness that are introduced by moving from SmoothMfd to sheaves. Manifolds embed in diffeological spaces which are the concrete sheaves (see Baez and Hoffnung [2]).

3 The algebra of functions

For a smooth manifold M the set of smooth real-valued maps f:M has the structure of a vector space, a ring, and in fact a commutative algebra. An algebra is a vector space over a base field (hence it has a commutative addition operation) which also has a multiplication operation that satisfies the distributive law when it interacts with addition. If the multiplication is commutative then we say the algebra is commutative. In this case the operations are all pointwise and so inherited from . For example fg(x)=f(x)g(x) where the right hand side is multiplication in .

Proposition 1.

Taking the algebra C(M) of smooth functions of a smooth manifold M gives a functor 𝖲𝗆𝗈𝗈𝗍𝗁𝖬𝖿𝖽C𝖢𝖠𝗅𝗀Rop.

There are important subcategories of 𝖢𝖠𝗅𝗀 that themselves contain the image of this functor, notably the “smooth algebras” but we won’t make use of their special properties, so we might as well use the simpler larger category.

Crucially this functor is actually faithful, meaning if you fix two manifolds then the functor is injective on the hom set between them. Said another way, any algebra homomorphism C(N)C(M) comes from a smooth map MN. Therefore we can embed SmoothMfd into 𝖢𝖠𝗅𝗀 and treat its image as an equivalent copy of SmoothMfd and find new ways to extend it and build new categories!

The proof of faithfulness is interesting and we will explore it fully because it’s challenging to piece it together from the references that exist easily to hand today. Since we have a couple other such “smooth facts” to make use of let’s handle them together.

4 The lemmas about smoothness

Lemma 1.

(“Milnor’s Exercise”) The map MevHom(C(M),R)=Hom(C(M),C(R0)) given by evaluation at a point of M is a bijection.


See also Kolář, Michor and Slovák [5], especially the preamble before section 35 and Corollary 35.9. Let ϕHom(C(M),). Then ker(ϕ) is an ideal of codimension 1. (An ideal of an algebra is a vector subspace which is closed under multiplication by an arbitrary element of the algebra.) Consider the collection of zero sets Zf,fker(ϕ). This collection of sets is closed under intersection: given Zf,Zg then Z(f2+g2)=ZfZg and f2+g2ker(ϕ). We have satisfied some of the hypotheses of the following topological lemma:

Lemma 2.

If X is Hausdorff and CX compact, and F={Ci} any collection of closed subsets of C with the property that Ci,CjFCiCjF, then iCi.

We have a collection of sets closed under intersection, so to satisfy the hypotheses of this new lemma it suffices to show that there is some Zf compact and nonempty, for then we can use this as the set C.

Suppose for a moment that we had this Zf. Let’s see how we can finish proving Milnor’s exercise. Suppose fker(ϕ)Zf, and so it contains some point x. Now consider an arbitrary gC(M,). Construct the function g=g-ϕ(g)1 where the latter term means the constant function with value ϕ(g). Then gker(ϕ), so g(x)=0, i.e. g(x)-ϕ(g)1(x)=0 and hence ϕ(g)=g(x), and so ϕ=evx as desired.

Now to construct the function f whose zero set is compact and nonempty. Back in Definition 1 we assumed all our smooth manifolds are Hausdorff with countable basis. This in turn implies paracompactness, a property that was put on this Earth to supply the existence of a partition of unity, a countable collection of smooth bump functions, each with compact support, and with the collective property that in a neighborhood of any point only finitely many of them are nonzero, and they sum everywhere to the constant function 1. So let’s fix a partition of unity {fi}i. Consider the function


This function is everywhere positive. We claim that for every c>0 that U=g-1([0,c]) is compact. By continuity U is closed. And it must lie in the union of finitely many supports, as the terms nfn grow beyond c eventually. So U is closed and contained in a finite union of compact sets, which is compact, and so U is compact. One more trick: this argument works for g2 as well, possibly with a different value of c. Since the codimention of ker(ϕ) is 1, some linear combination f=ag+bg2=0,a,b. This f carves out a compact nonempty zero set. GCLTODO – what was the gap here at the end? That a, b might be negative? Surely one of them *is* negative? ∎

It is perhaps notable that there is a larger class of topological manifolds for which Milnor’s exercise holds, which goes by the name realcompact.

Lemma 3.

For two smooth manifolds M1 and M2 the map

C(M1,M2) Hom(C(M2),C(M1)) (1)
f (ggf) (2)

given by precomposition is a bijection, i.e. 𝖲𝗆𝗈𝗈𝗍𝗁𝖬𝖿𝖽C𝖢𝖠𝗅𝗀Rop is faithful.


Given ϕHom(C(M2),C(M1)) and x1M1 we need to produce a point x2M2 and to show that this mapping x1x2 is smooth. Consider evx1ϕHom(C(M2),):


By Lemma 1 this is equal to evaluation at some point x2M2, so define f:M1M2 by x1x2. We have shown that ϕ(g)=gf and so gf is smooth for all g, which suffices to prove that f is smooth. ∎

Note that Lemma 3 is a generalization of Lemma 1 but that we used the latter to prove the former.

For our purposes these lemmas serve to allow us to pass to the image of C in the category of algebras and proceed to enlarge it in new ways that ar emade possible by the algebraic setting. We will do that by extending the algebras with nilpotent elements!

5 Nilpotents

An element xA of a real algebra is nilpotent if some power of it is zero. For example in the 4-dimensional algebra of 2x2 real matrices the element


satisfies M2=0. A more important example for us is [x]/x2, which is the polynomial algebra over  modulo the ideal generated by x2, which is equivalent to adding the relation x2=0. This truncates the polynomials to have degree at most 1, so this is a 2-dimensional real algebra. (Contrast this with [x]/x2+1 which is also 2-dimensional but does not add any nilpotent elements; it in fact is isomorphic to .) What if we add nilpotents to the story about algebras of smooth functions?

Now is a good time to expand our list of facts about smoothness with two more.

Lemma 4.

(Hadamard) If f:RnR is smooth then in some open neighborhood U(0,,0)


for smooth functions gi satisfying

Lemma 5.

Hom(C(M),[x]/x2) is in bijection with TM, the tangent bundle of M.

How the power is about the jet degree and the number of variables is about the dimension of the probing vector space. Remember 1?

6 The Kan extention

For an elementary introduction to the adjunctions we are discussing between presheaf categories see Awodey [1].

7 The modality

Differential cohesion is most gently introduced by Khavkine and Schreiber in [4] and plays a large role in Schreiber’s magnum opus [6].


  • [1] S. Awodey (2010) Introduction to category theory. Oxford University Press, Oxford; New York (English). Note: OCLC: 214305948 External Links: ISBN 978-0-19-923718-0 Cited by: §6.
  • [2] J. C. Baez and A. E. Hoffnung (2008-07) Convenient Categories of Smooth Spaces. (en). External Links: Link Cited by: §2.
  • [3] D. Dugger (1999) Sheaves and Homotopy Theory. (en). External Links: Link Cited by: §2.
  • [4] I. Khavkine and U. Schreiber (2017-01) Synthetic geometry of differential equations: I. Jets and comonad structure. (en). External Links: Link Cited by: §7.
  • [5] I. Kolář, P. W. Michor and J. Slovák (1993-01) Natural Operations in Differential Geometry. 1993 edition edition, Springer, Berlin ; New York (English). External Links: ISBN 978-3-540-56235-1 Cited by: §4.
  • [6] U. Schreiber (2013-10) Differential cohomology in a cohesive infinity-topos. (en). External Links: Link Cited by: §7.
  • [7] A. Scorpan (2005-05) The Wild World of 4-Manifolds. American Mathematical Society, Providence, R.I (English). External Links: ISBN 978-0-8218-3749-8 Cited by: §1.
Greg Langmead
Machine Learning Engineer

I am a software engineer and mathematician. I work on NLP algorithms for Apple News, and research homotopy type theory in CMU’s philosophy department.