Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

July 8, 2014

The Categorical Origins of Lebesgue Integration

Posted by Tom Leinster

I’ve just come back from the big annual-ish category theory meeting, Category Theory 2014 in Cambridge, also attended by Café hosts Emily and Simon. The talk I gave there was called The categorical origins of Lebesgue integration — click for slides — and I’ll briefly describe it now.

There are two theorems.

Theorem A The Banach space L 1[0,1]L^1[0, 1] has a simple universal property. This leads to a unique characterization of integration on [0,1][0, 1].

Theorem B The functor L 1:L^1: (finite measure spaces) \to (Banach spaces) has a simple universal property. This leads to a unique characterization of integration on finite measure spaces.

The talk’s pretty simple, and I don’t think I can summarize it much better than by repeating the abstract, which went like this:

Lebesgue integration is a basic, essential component of analysis. Yet most definitions of Lebesgue integrability and integration are rather complicated, typically depending on a series of preliminary definitions. For instance, one of the most popular approaches involves the class of functions that can be expressed as an almost everywhere pointwise limit of an increasing sequence of step functions. Another approach constructs the space of Lebesgue-integrable functions as the completion of the normed vector space of continuous functions; but this depends on already having the definition of integration for continuous functions.

So we might wish for a short, direct description of Lebesgue integrability that reflects its fundamental nature. I will present two theorems achieving this.

The first characterizes the space L 1[0,1]L^1[0, 1] by a simple universal property, entirely bypassing all the usual preliminary definitions. It tells us that once we accept two concepts — Banach space and the mean of two numbers — then the concept of Lebesgue integrability is inevitable. Moreover, this theorem not only characterizes the Lebesgue integrable functions on [0,1][0, 1]; it also characterizes Lebesgue integration of such functions.

The second theorem characterizes the functor L 1L^1 from measure spaces to Banach spaces, again by a simple universal property. Again, the theorem characterizes integration, as well as integrability, of functions on an arbitrary measure space.

Posted at July 8, 2014 12:54 AM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2751

79 Comments & 0 Trackbacks

Re: The Categorical Origins of Lebesgue Integration

Very neat! I’m sad that I missed CT this year.

Of course, in practice it’s important to know that an actual (sufficiently nice) function f:[0,1]f:[0,1]\to\mathbb{R} can be regarded as an element of L 1[0,1]L^1[0,1]. Is there any way to see this from your characterization, short of going through the proof that it coincides with the usual definition?

Posted by: Mike Shulman on July 8, 2014 6:57 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

It’s a shame you couldn’t come, especially as you’d done all the hard work of being on the scientific committee.

You’re asking the million-dollar question, one that I’ve been asked by a few people now. The short answer is “I don’t know”.

One obstruction is that L 1[0,1]L^1[0, 1] isn’t literally a set of functions, only almost-everywhere equivalence classes of functions. If it were a set of functions, we could hope to construct an evaluation map ev x: L 1[0,1] f f(x) \begin{aligned} ev_x: &L^1[0, 1] &\to &\mathbb{R}\\ &f &\mapsto &f(x) \end{aligned} for each x[0,1]x \in [0, 1] by using the universal property. But it’s not, and we can’t.

Posted by: Tom Leinster on July 8, 2014 10:36 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

At the very least there is an “evaluation map” ev A:ev_A : \mathcal{F} \rightarrow \mathbb{R} taking f Aff \mapsto \integral_A f, where AA is an element of \mathcal{F}, your σ\sigma-algebra.

The dual of L 1L^1 is L L^\infty, so perhaps find perhaps finding a characterisation of the latter and its action on L 1L^1 would help?

Posted by: Tom Ellis on July 8, 2014 3:30 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

You mean ev A:L 1[0,1]ev_A: L^1[0, 1] \to \mathbb{R}, right? The thing is, although that’s a map of Banach spaces, it’s not a map in the category I denoted by 𝒜\mathcal{A}, however you choose to give \mathbb{R} the structure of an object of 𝒜\mathcal{A}.

This assertion rests on a little calculation. Suppose we give \mathbb{R} the structure of an object (,u,ξ)(\mathbb{R}, u, \xi) of 𝒜\mathcal{A}. The axioms place various constraints on uu and ξ\xi, and it turns out that in all cases, the unique map to (,u,ξ)(\mathbb{R}, u, \xi) from the initial object (L 1[0,1],I [0,1],γ)(L^1[0, 1], I_{[0, 1]}, \gamma) is a scalar multiple of 0 1\int_0^1.

Posted by: Tom Leinster on July 8, 2014 6:08 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Yes that’s what I meant. I think I’m not sophisticated enough to understand the implications of the map not being in 𝒜\mathcal{A} though …

Posted by: Tom Ellis on July 8, 2014 6:24 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Well, what it means is that the map ev Aev_A can’t be obtained from the initiality of L 1[0,1]L^1[0, 1] in the most obvious way.

But there may be other ways to get at it.

Here’s something similar, due to Mark Meckes. (I very much wanted to include this in my talk, but time constraints prevented it.) Given any integrable function ff on [0,1][0, 1], we get a continuous function FF on [0,1][0, 1]:

F(x)= 0 xf. F(x) = \int_0^x f.

Furthermore, we obviously have F(0)=0F(0) = 0.

Now write C *[0,1]C_\ast[0, 1] for the set of continuous functions on [0,1][0, 1] taking value 00 at 00. Then id:xxid: x \mapsto x is an element of C *[0,1]C_\ast[0, 1], and furthermore there’s a map

ξ:C *[0,1]C *[0,1]C *[0,1] \xi: C_\ast[0, 1] \oplus C_\ast[0, 1] \to C_\ast[0, 1]

of Banach spaces (defined by an elementary two-case formula that I’m too lazy to write down) making (C *[0,1],id,ξ)(C_\ast[0, 1], id, \xi) into an object of 𝒜\mathcal{A}. The unique map

(L 1[0,1],I [0,1],γ)(C *[0,1],id,ξ) (L^1[0, 1], I_{[0, 1]}, \gamma) \to (C_\ast[0, 1], id, \xi)

in 𝒜\mathcal{A} is simply fFf \mapsto F (where as above, F(x)= 0 xfF(x) = \int_0^x f). The formula for ξ\xi is chosen to make this true.

So integration on part of the interval can be obtained from the initiality of L 1L^1. This is similar in flavour to what you wrote, although I don’t currently see how to imitate Mark’s example in your more general context.

Posted by: Tom Leinster on July 8, 2014 6:35 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I see. I am not thinking categorically enough! Perhaps the following approach will be more flavoursome to categorical connoisseurs.

An element of L 1L^1 is determined by its integrals over dyadic intervals, i.e. intervals of the form [k2 n,(k+1)2 n][k2^{-n}, (k+1)2^{-n}]. How can we recover these?

For fixed nn I believe we can extract all 2 n2^n of these at once by representing 2 n2^n \rightarrow \mathbb{R} as an object of 𝒜\mathcal{A}. It’s certainly a Banach space with a suitable “unit” vector uu. What should the “codiagonal” map ξ\xi be? Is taking the arithmetic mean of a vector ff at pairs of neighbouring points (f(0)f(0) and f(1)f(1), f(2)f(2) and f(3)f(3), …) and then squashing horiztontally enough? (This is a discretization of γ\gamma).

If so we can recover the integral over dyadic intervals using the unique map from L 1L^1 to (2 n,1,ξ)(2^n \rightarrow \mathbb{R}, 1, \xi).

Posted by: Tom Ellis on July 8, 2014 6:59 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

In fact I think we can embed L 1L^1 in (L ) *(L^\infty)^* directly.

Take the object of 𝒜\mathcal{A} which is ((L ) *,1,ξ)((L^\infty)^*, 1, \xi) where ξ\xi “undoes” γ\gamma. That is

(1)ξ(f,f)(v)=f(v(x/2))+f(v(1/2+x/2))2 \xi(f, f')(v) = \frac{f(v(x/2)) + f'(v(1/2 + x/2))}{2}

(Here f,f(L ) *f, f' \in (L^\infty)^*, vL v \in L^\infty and x[0,1]x \in [0,1])

Posted by: Tom Ellis on July 8, 2014 7:33 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I was wondering if one of the conditions in the second case can be replaced by the condition that FF preserves coproducts. You’d have to choose an appropriate subcategory of L 1L^1.

Posted by: Tom Ellis on July 8, 2014 8:34 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I thought about this kind of thing, and although there are some ways to recast the conditions on FF, it’s not as simple as you suggest. The trouble is that coproducts in Meas embMeas_{emb} aren’t disjoint unions (and indeed don’t always exist), for the same kind of reason that coproducts in the category of sets and injections don’t behave as you might at first expect.

Posted by: Tom Leinster on July 8, 2014 11:00 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I’m surprised to hear that about coproducts in Meas embMeas_emb. I should work through the details. I tried to do something along the lines I suggested after your talk, but I didn’t get very far.

Posted by: Tom Ellis on July 8, 2014 3:02 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

You mention the “the undergraduate-textbook approach” to Lebesgue integration. Since we’re slow-witted in America, I regularly teach a graduate course on Lebesgue integration. I’m tempted to mention your universal characterization! Unfortunately we do Lebesgue integration in the first quarter and Banach spaces in the second. But maybe I can still somehow slip it in.

Posted by: John Baez on July 8, 2014 10:31 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I’m feeling pretty slow-witted myself right now, but let me see if I can formulate a thought: it’s somehow not coincidence that your teaching is arranged in an order that makes it awkward to mention this theorem. Pedagogically, it’s natural to progress as follows:

  • First study individual functions (such as integrable functions on [0,1][0, 1]).

  • Then study individual spaces of functions (such as the Banach space L 1[0,1]L^1[0, 1]).

  • Then study individual systems of spaces of functions (such as the category BanBan).

…”and so on”, I guess, to ever-higher levels of abstraction and categorical dimensions.

The question on my last slide — can we state precisely why it’s natural to associate a Banach space to a measure space? — belongs on one of those higher levels of abstraction.

In any case, you could tell your class the unique characterization of integration without mentioning the universal characterization of L 1L^1.

Posted by: Tom Leinster on July 8, 2014 11:19 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I don’t have an answer about why it’s natural to associate a Banach space to a measure space, but I can broaden the question: why is it natural to associate a class of metric vector spaces to a measure space?

We don’t just have L 1L^1 arising from the arithmetic mean, (x+y)/2(x + y) / 2. We also have L pL^p for any p1p \ge 1 arising from a different average, (x p+y p) 1/p/2(x^p + y^p)^{1/p} / 2. We also have complete metric vector spaces (not normed spaces) when 0<p<10 \lt p \lt 1 arising from x p+y px^p + y^p (though no one ever seems to care about these). I think convergence in measure gives us the p0p \rightarrow 0 case.

These are all preserved by measure-preserving automorphisms of the underlying space. Perhaps there’s some uniqueness result about these.

Posted by: Tom Ellis on July 8, 2014 3:22 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I can’t help but ask: what on earth are measure spaces for, if not forming their L 1L^1? What else would you do with them? And going from μ\mu to L 1(μ)L^1(\mu) forgets very little.

For Tom Ellis hints at a partial inversion: L L^\infty is also natural; it is furthermore an algebra, and the subset of idempotents x:L (μ)&x 2=x x : L^\infty(\mu) \& x^2 = x are an interesting family. Terry Tao was writing about similar things about a week ago.

Posted by: Jesse C. McKeown on July 8, 2014 5:57 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I can’t help but ask: what on earth are measure spaces for, if not forming their L 1L^1? What else would you do with them?

Don’t restrain yourself! Go ahead! Ask!

Indeed, Theorem B is a precise formulation of the gut feeling that you so dramatically express.

Posted by: Tom Leinster on July 8, 2014 6:18 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Mark asks, rhetorically:

I can’t help but ask: what on earth are measure spaces for, if not forming their L 1?L^1? What else would you do with them?

Form their L L^\infty?

I mention this not just to be a smart-aleck (though that’s always fun), but because my advisor Irving Segal had a concept of ‘integration algebra’ which he advocated as a better way to think about integration. L 1L^1 isn’t an algebra, but L L^\infty is. It might be fun to revisit his work with a more category-theoretic outlook.

He always hated the points in that big measure space Ω\Omega probability theorists like to have hovering over all their discussions, since everything is done ‘almost everywhere’, not at individual points.

He had an unusually florid style for a mathematician (though maybe that’s not saying much), so I’ll quote the introduction to his paper Algebraic integration theory and then state the main theorem:

Although the theory of the abstract Lebesgue integral has strong intrinsic architectural articulation, the very importance of the theory for a variety of mathematical applications has tended to cloud its basic simplicity and elegance. The large number of approaches and formalisms, each justification by its appropriateness in connection with particular applications, has given the theory as a whole an appearance of heterogeneous complexity which is in fact significantly specious and a hindrance to a deeper understanding of the theory and to its further application. While it would probably be widely granted that integration serves as a focal point for real analysis, the focus has been more virtual than real; the ultimate convergence of the multitude of generally similar but technically distinct theories has been felt rather than proved.

(That reminds me of how certain people invented the concept of ‘natural isomorphism’ to simplify the sprawling mess of different homology theories, back in the 1940’s.

On the other hand, the coherence and algebraic simplicity of the basic theory has been visible and virtually taken for granted for a long time by those working in abstract analysis. The replacement of the sigma-ring of all measurable sets by the abstract Boolean ring of measurable sets modulo null sets is natural from a fundamental statistical viewpoint, and provides probably the earliest approach displaying such features. This Boolean ring approach, which has now been elaborated by many publications, most notably those of Carathéodory and his associates, is, however, an inconvenient one for most applications, inasmuch as these deal mainly with functions, which enter into the Boolean ring approach only in a rather circumlocutory fashion. Around the later thirties there appeared, as a fruit of the spectral and representation theory originating in the well-known work of von Neumann, Stone, and Gelfand, simple abstract characterizations of measure-theoretic function spaces, as ring and/or lattices. However, no comprehensive development of integration theory along such lines took place at that time.

It was the development of a variety of new theories, rather than the desire to embellish old ones, which primarily has led to the development of a complex of results, methods, and ideas here somewhat loosely referred to as ‘algebraic integration theory.’ The introduction of a new term such as this requires some explanation and justification tion, in the light of the rapidly increasing burden which mathematicians must bear. To this end we point out that one almost universal feature of applied work is a tendency to overlook mathematical isomorphisms. In theoretical physics, for example, although analogies are frequently invoked, the concept of a rigorous isomorphism rarely occurs in a non trivial form, although it is relevant in a number of significant ways in contemporary work. The result of this is, naturally, a tendency toward a variety of babel; each special context tends to acquire a distinctive terminology and notation, and close connections or even virtual identities between superficially distinct developments, are rendered quite obscure. This is, of course, not only uneconomical, in the duplication of labor involved, but brings a substantial linguistic encumbrance to bear on the scientific commerce between different areas and the development of interdisciplinary subjects.

Even in probability theory, the most notably successful of originally applied subjects in achieving mathematical clarity and emerging in this century as a distinctive branch of mathematics, cases could be cited in which quite wrong conclusions were reached as to the relation between certain work and earlier extant theories. While the use of analogies is a partial substitute in heuristic work, it has the disadvantage of making it impossible to determine whether the results are merely plausible or actually quite correct; on occasion it even makes it difficult to determine whether the results are meaningful. The obvious corrective for this situation is a closer adherence to a formulation of integration theory which is relatively independent of particularities and revealing of features independent of the notation. This might be called invariant integration theory, but this term might well suggest a subject quite different from this one, namely that of invariant integrals. Since the setting of the theory is naturally algebraic, in its concern with features independent of isomorphisms, the term algebraic integration theory is reasonable—although the subject is distinctly more distant from conventional algebra than is algebraic topology. Such a theory is necessarily abstract, but the term ‘abstract integration theory’ has already a different meaning, signifying usually the theory in which integrals are considered not necessarily over subsets of euclidean space, but over relatively general spaces, and is a more limited and quite distinct notion from that of the theory considered here, whose distinctive description as algebraic seems therefore practical.

This build-up actually goes on for quite a bit longer, but here’s the theorem:

Theorem. Suppose AA is a real commutative associative algebra with unit, and let

:A \int : A \to \mathbb{R}

be a linear functional such that:

  1. a 20\int a^2 \ge 0, and equals zero iff a=0a = 0.

  2. For any bAb \in A there is a constant kk such that a 2bka 2\int a^2 b \le k \int a^2.

Then AA is isomorphic to a dense subalgebra of L (X)L^\infty(X) for a finite measure space XX, with the usual integral as \int.

Posted by: John Baez on July 10, 2014 8:08 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

The first question that comes to mind about this is how it deals with collections of measures that are not mutually absolutely continuous. The most obvious difficulty this raises is that they don’t have the same equivalences classes of measurable functions since their null sets differ. Is there some neat way of dealing with that?

Posted by: Tom Ellis on July 10, 2014 8:51 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

John wrote:

Mark asks, rhetorically:

That was Jesse, not Mark. (And that comment doesn’t sound like Mark!)

Sorry to make such a tiny reponse to such an informative comment, but that’s as far as I’ve got just now :-)

Posted by: Tom Leinster on July 10, 2014 12:37 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

That’s a great theorem. Thanks for telling us!

This build-up actually goes on for quite a bit longer

Indeed — 14 pages of prose in a similarly florid style! The last paragraph begins:

With this brief bird’s-eye view of algebraic integration theory…

Posted by: Tom Leinster on July 11, 2014 12:15 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I can’t help but ask: what on earth are measure spaces for, if not forming their L 1L^1? What else would you do with them?

Form their L L^\infty?

That’s a good answer, partly because of the very nice related theorem you quoted, and partly because it immediately suggests other good answers (form their L 2L^2, form their L pL^ps, form their Orlicz spaces…). But one thing I find unsatisfying about it is that L L^\infty forgets most of the information about a measure space: it only cares about which sets have measure zero.

This is related to a critique I have of the following comment:

[Segal] always hated the points in that big measure space Ω\Omega probability theorists like to have hovering over all their discussions, since everything is done ‘almost everywhere’, not at individual points.

Probability theorists also hate the points in Ω\Omega (or, more fairly, find them irrelevant to the point at hand, and hence a nuisance when they can’t be avoided). But what matters to them is the joint distribution of all the random things under consideration, which includes a lot more information than just what happens almost everywhere.

Anyway, anyone interested in this discussion would probably also be interested in this MathOverflow question.

Posted by: Mark Meckes on July 11, 2014 1:58 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Mark wrote:

Probability theorists also hate the points in Ω\Omega (or, more fairly, find them irrelevant to the point at hand, and hence a nuisance when they can’t be avoided).

Well, but Segal really hated them, so he developed algebraic integration theory as a way to never mention them.

But what matters to them is the joint distribution of all the random things under consideration, which includes a lot more information than just what happens almost everywhere.

Right; starting from one of Segal’s ‘integration algebras’ you can get all those joint distributions. An integration algebra is a real commutative algebra AA with a linear functional :A\int : A \to \mathbb{R} obeying the two conditions I mentioned a while back.

The special virtue of L L^\infty is merely that it’s dense in all the other L pL^p’s (for a finite measure space) and it’s an algebra. So, for Segal the integration algebra serves as an abstract version of L L^\infty (or a dense subalgebra thereof). Then, using the \int, he can define all the other L pL^p’s as completions of the integration algebra with respect to various norms.

To me this ‘pointless’ point of view is worth knowing, but I’m not proselytizing for it; I don’t consider points as pointless as Segal did.

Posted by: John Baez on July 12, 2014 8:18 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Right; starting from one of Segal’s ‘integration algebras’ you can get all those joint distributions. An integration algebra is a real commutative algebra AA with a linear functional :A\int:A \to \mathbb{R} obeying the two conditions I mentioned a while back.

Fair enough, although it seems to me that you’ve just admitted that when you said “Form their L L^\infty”, you really meant “Form the pair (L ,)(L^\infty, \int)”, which is not so far from L 1L^1 itself. (Although I concede that the fact that L L^\infty is an algebra is a major advantage for some purposes.)

To me this ‘pointless’ point of view is worth knowing

Absolutely, and in fact some version of it is well known to people working in noncommutative versions of probability theory, like free probability.

Posted by: Mark Meckes on July 12, 2014 10:28 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

This may have been covered in previous discussions on this blog, but one curious thing from the point of view of the “traditional” approach to the Lebesgue integral is that your approach seems not to put so much emphasis on integrating positive functions, monotone class theorem, and so on.

In the standard approach one defines the Lebesgue integral for all measurable non-negative functions, with [0,][0,\infty] being the natural range of the integration map; and then one takes as the integrable functions those whose modulus has finite integral in the sense above. So I’m curious to get a better idea for how or why the approach via initial algebras sidesteps this.

Also, relating to some other comments on this thread: there still seems something a little artificial about privileging 1/2-1/2 over 1/2-2/3. Is there any mileage in moving from “algebras” with binary operation to ones with some kind of infinitary operation? (Something like http://golem.ph.utexas.edu/category/2009/04/convex_spaces.html )

Posted by: Yemon Choi on July 9, 2014 12:27 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Ugh, typo: I meant 1/2-1/2 versus 1/3-2/3, or perhaps 1/3-1/3-1/3

Posted by: Yemon Choi on July 9, 2014 3:05 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I agree that 1/2-1/2 is a choice, though I wouldn’t necessarily call it an artificial one. If you chose 1/3-2/3, you’d simply end up with a different measure on [0,1][0, 1] (skewed to the right), though I think the two versions of [0,1][0, 1] would be isomorphic as measure spaces.

You could equally well use 1/3-1/3-1/3, or 1/4-1/4-1/4-1/4, etc., and they would also produce Lebesgue measure on [0,1][0, 1]. (Similarly, Freyd’s theorem also holds if you stick together three or more copies of the interval.)

Posted by: Tom Leinster on July 9, 2014 8:56 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Question for any passing analyst: given a finite measure space (X,μ)(X, \mu), there is a metric dd on the set Σ X\Sigma_X of measurable subsets of XX given by

d(A,B)=μ(AB) d(A, B) = \mu( A \triangle B)

where \triangle means symmetric difference. Given also a function fL 1(X)f \in L^1(X), there is a function

fdμ: Σ X A Afdμ. \begin{aligned} \int_\bullet f\,d\mu: &\Sigma_X &\to &\mathbb{R}\\ &A &\mapsto &\int_A f \,d\mu. \end{aligned}

Question: Is fdμ\int_\bullet f\,d\mu continuous?

I suppose it must be in the case X=[0,1]X = [0, 1], because 0 xf\int_0^x f is continuous in xx (as mentioned earlier).

Posted by: Tom Leinster on July 9, 2014 1:53 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I believe so, yes. The missing ingredient is

(1)fL 1 Af0 as μ(A)0 f \in L^1 \Rightarrow \integral_A f \rightarrow 0 \, \text{ as } \, \mu(A) \rightarrow 0

Here is the proof of that claim

(2) Af A|f|1 {fK}+ X|f|1 {f>K} \integral_A f \le \integral_A |f| 1_{\{f \le K\}} + \integral_X |f| 1_{\{f \gt K\}}

The first summand is bounded by Kμ(A)K\mu(A) and the second summand tends to zero as K0K \rightarrow 0 by the dominated convergence theorem. So for big enough KK the right hand side will be small and then for small enough μ(A)\mu(A) the sum will be small.

This is related to the concept of uniform integrability, in particular a singleton set containing an element of L 1L^1 is uniformly integrable.

Posted by: Tom Ellis on July 9, 2014 4:34 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Great; thanks, Tom. So now I’m optimistic that we can imitate Mark’s example in the more general setting.

Let’s give it a try.

For each (finite, as always) measure space X=(X,Σ X,μ X)X = (X, \Sigma_X, \mu_X), we have the set C(Σ X)C(\Sigma_X) of continuous functions Σ X\Sigma_X \to \mathbb{R}, where Σ X\Sigma_X is metrized as above. This is in fact a Banach space, under the sup norm. It has a closed subspace C *(Σ X)C_\ast(\Sigma_X) consisting of all those ϕC(Σ X)\phi \in C(\Sigma_X) such that ϕ()=0\phi(\emptyset) = 0; that is itself a Banach space.

Whenever we have an embedding YXY \hookrightarrow X of measure spaces, we get a map C *(Σ Y)C *(Σ X)C_\ast(\Sigma_Y) \to C_\ast(\Sigma_X) defined by ϕϕ¯\phi \mapsto \bar{\phi}, where for any measurable AXA \subseteq X, we put ϕ¯(A)=ϕ(AY)\bar{\phi}(A) = \phi(A \cap Y). This map is linear and of norm 1\leq 1 (that is, sup A|ϕ¯(A)|sup B|ϕ(B)|\sup_A |\bar{\phi}(A)| \leq \sup_B |\phi(B)|). So it’s a map of Banach spaces in the usual sense.

So, we’ve just defined a functor C *(Σ ):Meas embBanC_\ast(\Sigma_\bullet): Meas_{emb} \to Ban.

The next task is to equip C *(Σ )C_\ast(\Sigma_\bullet) with enough extra structure that it becomes an object of the category called \mathcal{B} in my slides. That means that for each measure space XX, we have to pick out a distinguished element u XC *(Σ X)u_X \in C_\ast(\Sigma_X). We do this by setting u X(A)=μ X(A)u_X(A) = \mu_X(A) for each measurable AXA \subseteq X (and checking that u Xu_X is continuous, which is easy). It has the following two properties:

  • u Xμ X(X)\|u_X\| \leq \mu_X(X) for each XX (again, easy)

  • if YXYY \rightarrow X \leftarrow Y' are embeddings with Y⨿Y=XY \amalg Y' = X then u Y¯+u Y¯=u X\bar{u_Y} + \bar{u_{Y'}} = u_X (where I’m using bar notation for the action of the functor C *C_* on morphisms, as above). That’s just a matter of unwinding the definitions.

So: we’ve defined an object (C *(Σ ),u)(C_\ast(\Sigma_\bullet), u) of the category \mathcal{B}.

By the universal property of (L 1,I)(L^1, I), there is a unique map (L 1,I)(C *(Σ ),u)(L^1, I) \to (C_\ast(\Sigma_\bullet), u) in \mathcal{B}. We can phrase this fact completely concretely: there is a unique family of linear maps

(J X:L 1(X)C *(Σ X)) measure spaces X \Bigl( J_X: L^1(X) \to C_\ast(\Sigma_X) \Bigr)_{\text{measure spaces }\,\, X}

of norm 1\leq 1 such that:

  • (J X(constant function 1))(A)=μ X(A)(J_X(\text{constant function 1}))(A) = \mu_X(A) for all measure spaces XX and measurable AXA \subseteq X

  • whenever a measure space YY is embedded into another measure space XX, and gL 1(Y)g \in L^1(Y), then (J X(g extended by 0))(A)=(J Y(g))(YA)(J_X(g \,\,\text{ extended by }\,\, 0))(A) = (J_Y(g))(Y \cap A) for all measurable AXA \subseteq X.

Since these conditions are satisfied by putting (J X(f))(A)= Afdμ X(J_X(f))(A) = \int_A f \,d\mu_X, that’s what JJ is.

In other words:

the universal property tells us the integral of any function fL 1(X)f \in L^1(X) not only on XX itself, but also on every measurable subset of XX.

(Footnote: I’ve relied here on the assumption that when one measure space YY is embedded into another measure space XX, and AA is a measurable subset of XX, then YAY \cap A is a measurable subset of YY. This isn’t actually true with the meaning of “embedding” defined in my slides: there, I only asked that an embedding is injective and that the direct [not inverse] image of a measurable set is measurable. But the theorem still holds if we strengthen the definition of embedding to include the condition that the inverse image of a measurable set is measurable, i.e. that if AA is measurable in XX then YAY \cap A is measurable in YY. Perhaps this application suggests that this version of the theorem is superior.)

Posted by: Tom Leinster on July 9, 2014 6:04 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Now that I think about it, I’m not sure it was necessary to use C *(Σ X)C_\ast(\Sigma_X) rather than C(Σ X)C(\Sigma_X). In other words, I’m not sure it was necessary to restrict from the class of all continuous functions ϕ\phi on Σ X\Sigma_X to just those satisfying ϕ()=0\phi(\emptyset) = 0.

I did it because I was imitating Mark’s construction, but unless there’s some check I’ve missed, I don’t see that it was necessary — maybe I could have used the simpler C(Σ X)C(\Sigma_X) throughout. I’ll have to check over it all again.

Posted by: Tom Leinster on July 9, 2014 6:24 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

So you’ve just proved that integration is linear, for free! Very nice.

My understanding was that the C *C_{\ast} is not needed in Mark’s proof or yours, but just gives a stronger result. In fact I think you could take “additive” functions ff such that ϕ(A)+ϕ(B)=ϕ(AB)+ϕ(AB)\phi(A) + \phi(B) = \phi(A \cup B) + \phi(A \cap B), zero on \emptyset.

That would allow you to deduce more, wouldn’t it?

Posted by: Tom Ellis on July 10, 2014 8:35 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

The next question is, is there some way of getting the monotone convergence theorem?

Posted by: Tom Ellis on July 10, 2014 8:38 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

(Well I suppose we already had linearity. But I still think it’s nice :)

Posted by: Tom Ellis on July 10, 2014 11:58 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I just went through both Mark’s example and mine in fine detail.

C *C_\ast is needed in Mark’s, I think. Using just CC, you’d have to define the structure map

ξ:C[0,1]C[0,1]C[0,1] \xi: C[0, 1] \oplus C[0, 1] \to C[0, 1]

differently (in order to make sure that it outputs functions that are continuous at 1/21/2), and then it no longer has norm 1\leq 1.

However, in the general (“Theorem B”) scenario, you can use the simpler CC instead.

Posted by: Tom Leinster on July 10, 2014 12:43 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Tom, Can you use some category theoretic argument (e.g. some sort of adjoint functor theorem) to prove the existence of Lebesgue measure? Ben
Posted by: Benjamin Steinberg on July 9, 2014 3:06 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I don’t think I know such a theorem, but I’m not entirely sure I know what you mean. Can you be any more precise about what you mean by “the existence of Lebesgue measure”?

I believe there’s a theorem (which I once worked out, but only kind of scrappily) characterizing the poset of Lebesgue-measurable subsets of [0,1][0 ,1] by some universal property. It’s very similar in spirit to the characterization of L 1[0,1]L^1[0, 1], but instead of thinking about arbitrary integrable functions, we’re thinking about characteristic functions of measurable subsets.

Posted by: Tom Leinster on July 9, 2014 3:32 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Normally it is painful to construct Lebesgue measure. One first defines it on intervals and then builds from there via approximation. It would be nice to show that an object satisfying the universal property of L 1[0,1]L^1[0,1] exists by category theoretic methods and then deduce from it the usual Lebesgue theory.
Posted by: Benjamin Steinberg on July 9, 2014 8:51 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

The “alternative proof” on slide 10 does indeed construct L 1[0,1]L^1[0, 1] by categorical methods. It’s not even an adjoint functor theorem, but more explicit. When you unwind it, it constructs L 1[0,1]L^1[0, 1] as the colimit over all nn of the spaces

{step functions on[0,1] whose breakpoints are integer multiples of 2 n}. \{\text{step functions on}\,\,[0,1]\,\,\text{ whose breakpoints are integer multiples of } \,\, 2^{-n}\}.

How much of the usual Lebesgue theory can be deduced directly from the universal property, I’m not sure yet. For instance, Fubini is a good challenge.

Posted by: Tom Leinster on July 10, 2014 1:55 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Your slides mention a program of showing that mathematical structures that are socially important are also categorically natural. Do you know something good to cite, where someone has advocated this program, explained it, and maybe listed some examples? I want to cite something about that…

Ideally this program, carried out sufficiently far, would allow for a “reworking” of mathematics from a more top-down viewpoint. Perhaps it would never be very good for a first course (as you mention), but it might let us compress a lot of long proofs. For example, it might make chunks of analysis more like algebraic topology, replacing ϵ\epsilon-δ\delta arguments with commutative diagrams and the like. Of course not everyone would want that, but something good would surely come of this alternate approach.

Posted by: John Baez on July 10, 2014 5:52 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I don’t think I can suggest anything good to cite. During the talk, I reminded the audience of the thrill they probably felt when they first discovered that various standard mathematical constructions arise as adjoints (perhaps left adjoints to some much simpler functor), or as (co)limits, etc.

One of my favourite examples of “socially important is categorically natural” is how the category Δ\Delta (hence the category of simplicial sets) arises in a canonical way from the forgetful functor CatGraphCat \to Graph. See e.g. here and here.

It’s probably only my favourite because I discovered it myself. Nevertheless, I like it because I’d never heard a convincing explanation of why simplicial sets are a natural thing to study, from any point of view. (I realize that that sentence may tempt you to have a go; please do!) Geometrically, it’s easy to see why you might want to divide a space into simplices. But why put the vertices in order? Why have the degeneracy maps? Or algebraically, why consider nonempty, finite, totally ordered sets, rather than some other collection of modifiers?

Maybe there’s some good other explanation of simplicial sets that I’m missing. But at the time, I thought the categorical story that I was able to tell was a good, clean explanation for their undoubted social importance.

(I hope it’s more or less clear what I mean by “social importance”. Obviously it doesn’t mean what a non-mathematician would think it means. It’s something like this: if I open a book on algebraic geometry then I might see that the word “divisor” comes up a lot, so I’d be able to deduce that divisors were important to algebraic geometers without even knowing what they are.)

Another example is the Freyd theorem characterizing [0,1][0, 1] (slide 6). Undoubtedly, the unit interval is socially important!

Posted by: Tom Leinster on July 10, 2014 12:58 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Why put the vertices in order? Why have the degeneracy maps? Here is one possible answer: so that the cartesian product is geometrically correct. See here for more details. There’s also this question on MO.

Posted by: Zhen Lin on July 10, 2014 2:37 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I’d never heard a convincing explanation of why simplicial sets are a natural thing to study, from any point of view.

How about the fact that they are the classifying topos for strict intervals?

Posted by: Mike Shulman on July 10, 2014 6:14 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I’d like to know why simplicial sets are natural for what we tend to use them for: namely, as models of homotopy types. It seems a bit odd that the classifying topos for strict intervals would be so good for that.

Tom’s favored explanation seems to be roughly “simplicial sets show up as nerves of categories, and nerves of categories are a natural thing”, together with some theorems to back up the second part.

Maybe simplicial sets are no better than cubical sets, etc. when it comes to modeling homotopy types, but they win thanks to this extra feature.

Maybe your remark about the classifying topos for strict intervals is connected to the technical details of Tom’s favored explanation. He states a theorem about ‘generalized nerves’ and the topos of ‘TT-simplicial sets’ for a sufficiently nice monad TT. What is this topos the classifying topos of, in general?

Posted by: John Baez on July 11, 2014 2:34 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I think it’s very natural that the classifying topos for strict intervals would be good for modeling category-like things. Roughly, it’s “the topos that you when you start with SetSet and freely throw in a strict interval.” Since toposes are cocomplete, you can glue together copies of the generic strict interval, obtaining objects that contain “morphisms” (or one might say “directed sets”). Then you can impose conditions on these objects so that these “morphisms” can be composed and inverted to get models for (it turns out) (,1)(\infty,1)-categories and \infty-groupoids.

Your last question is interesting! I’d like to know the answer.

Posted by: Mike Shulman on July 11, 2014 6:12 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

The description of the category of simplicial sets as the classifying topos of the theory of strict intervals is nice, but I don’t find it very much more persuasive than its description as the category of presheaves on nonempty finite totally ordered sets. For instance, why is it important to say “strict”? And what’s so special about intervals (totally ordered sets with a least and a greatest element)?

Zhen’s answer is also important, but it’s sort of historical. I mean, I can imagine a historical process by which people realized that it was important to put a total order on the vertices of each simplex and incorporate the degeneracy maps, and that’s a valuable thing to understand. However, it doesn’t seem to me to be a reason to think of simplicial sets as categorically natural.

I’d also like an answer to John’s question:

I’d like to know why simplicial sets are natural for what we tend to use them for: namely, as models of homotopy types.

Freyd’s theorem tells us why [0,1][0, 1] is natural for what we often use it for: namely, to parametrize time in elementary homotopy theory. I spent a while trying to find a related description of the category Δ\Delta and the functor ΔTop\Delta \to Top that sends [n][n] to the topological nn-simplex.

I didn’t succeed, but I got somewhere: in a sense made precise in Example 10.12 here, the restricted functor Δ injTop\Delta_{inj} \to Top is universal admitting barycentric subdivision. Here Δ inj\Delta_{inj} is the subcategory of Δ\Delta containing just the face maps.

Posted by: Tom Leinster on July 11, 2014 12:29 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I agree that Zhen’s answer doesn’t answer the question (right now I’m trying to get a similar sort of question answered on MO). But if you’re happy with Freyd’s result explaining [0,1][0,1], then you can see a strict interval is just an abstraction of the structure of [0,1][0,1], so that you get a classifying topos containing the “generic homotopy theory”. You need a strict interval (distinct endpoints) in order to have homotopies relating distinct points.

For what it’s worth, I don’t find your favored explanation completely convincing either, because it requires specifying not only the category CatCat, but also its monadic forgetful functor to directed graphs. Is that functor in any way canonically associated to the category CatCat? A priori, CatCat might be pra-monadic over other presheaf categories as well, and maybe you would get different nerves from those.

Posted by: Mike Shulman on July 11, 2014 3:44 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Assuming classical logic, you can extract the forgetful functor CatGrphCat \to Grph. It suffices to characterise the free arrow 𝟚\mathbb{2}: but this is none other than the minimal (= weakly initial) connected category with exactly two objects. (The functor ob:CatSetob : Cat \to Set is represented by the terminal object, and connectedness can be detected by the left adjoint of the left adjoint of ob:CatSetob : Cat \to Set.) Of course, this is very special to CatCat.

Less evilly, one might consider the usual presentation of categories as models for a three-sorted essentially algebraic theory where composition is coded as an operation. As is well-known, there is a pullback diagram relating one of those sorts to the other two. If we delete that sort and the associated operations and axioms, we are left with the (purely) algebraic theory of (reflexive, directed, multi-)graphs.

Or we could even consider the two-sorted cartesian theory where composition is coded as a three-place relation. Then the theory of graphs is obtained by deleting that relation and its associated axioms.

Of course, choosing a particular axiomatisation of the theory of categories is essentially as bad as choosing a particular monadic forgetful functor. I’m personally not convinced that the nerve functor is such a canonical thing.

Posted by: Zhen Lin on July 11, 2014 4:53 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

It seems to me that the whole point of Tom’s characterization is that it isn’t special to CatCat. I agree that choosing a particular axiomatization of the theory is not really an improvement.

Posted by: Mike Shulman on July 11, 2014 7:36 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Another unsatisfying thing about your explanation to me is that it depends on having the 1-category CatCat. So, for instance, it doesn’t work in homotopy type theory, where there is no such 1-category, only a 2-category. Is there a higher-categorical version of the nerve theorem?

Posted by: Mike Shulman on July 11, 2014 4:33 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Whilst I would not quarrel with a foundations in which the category of large categories is a 2-category, it seems to me that it is typically correct to view Cat\mathsf{Cat}, the category of small categories, as an ordinary category when taking nerves. Certainly when viewing categories as models of homotopy types via their nerves, we are thinking of them just as ordinary algebraic gadgets (eg, algebras for an ordinary monad), akin to groups, etc.

Thus I would find it very strange if it were not possible, in a natural way, to view Cat\mathsf{Cat} as an ordinary category in homotopy type theory. Certainly it is possible in ordinary intensional Martin-Löf type theory.

On a different note, with regard to the following comment of John…

Maybe simplicial sets are no better than cubical sets, etc. when it comes to modeling homotopy types, but they win thanks to this extra feature [that we can take nerves, and can prove theorems which make use of them].

…it is of course perfectly possible to take a nerve of a category landing in cubical sets! For working with nerves of higher categories (or nn-fold categories, etc), I have in fact found the cubical setting to be more natural than the simplicial one.

My feeling is that it is a historical accident that simplicial sets have been the preferred presheaf models of homotopy types. Simplicial sets have some features which are convenient for some purposes, or which can appear so until one thinks a little more deeply. A significant one is that simplicial homotopy can be defined with respect to the simplicial interval and the cartesian product. There is however no conceptual reason that it is necessary to work with a cartesian product here: a monoidal structure, as with cubical sets, is all that is needed.

I would go so far as to conjecture that all the purposes to which simplicial nerves of categories are put have perfectly good cubical analogues. Sometimes one may need to add further structure to one’s cubical sets: connections are the most well known example of such structures, but there are others. Sometimes one may also need to reformulate things a little, but this can often, in my experience, in fact lead to deeper insight into whatever it is one is looking at.

The possibility for adding further structure to cubical sets in a conceptual way is, I feel, a significant advantage of cubical sets over simplicial sets. Another is that the category of cubes (in any flavour) has a 2-universal property which is very useful in practise. It typically allows one to make rigorous and formal the passage from geometric intuition in low dimensions to a generalisation to all dimensions, which is at heart of working with presheaf models of homotopy types.

As a final remark, on a slightly different note once again, I feel that looking for an explanation of why Δ\Delta or the category of cubes is ‘categorically natural’ is something of a red herring, at least from the point of view of homotopy theory. It is perhaps a little easier to explain what I am getting at for the category of cubes, or, better, the category of semi-cubes (no degeneracies), than for Δ\Delta. This category precisely abstracts the structure of the topological nn-cubes that is significant for setting up the homotopy theory of topological spaces. One can add further structure (degeneracies, connections, …) which reflect further structure of the topological nn-cubes. I feel that this is perfectly conceptual in and of itself, and that there is no more and no less to it.

One can define the category of cubes in a categorically nice way, for example as an algebra for a 2-monad, but the significance of this category is exactly what I have expressed in the previous paragraph, I feel. The fact that categories can model homotopy types via nerves, etc, is a beautiful observation that builds upon this story, but is, for me at least, not something which helps to explain the definition of the category of cubes itself. This is all the more the case because all the content, from a homotopical point of view at least, of the definition of the nerve of a category can be captured by 2-truncated simplicial or cubical sets: we do not need the entire category.

Posted by: Richard Williamson on July 13, 2014 12:36 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

There is a 1-category of “categories” in homotopy type theory, but its objects are what we call strict categories: categories equipped with a notion of “equality of objects”. Those kinds of categories can be viewed as ordinary set-level algebraic gadgets. But they are different from the “categories” that category theory is usually concerned with. The difference is not fundamentally one of size, although strict categories tend to be small.

The nerve theorem might be true in HoTT if formulated about the 1-category of strict categories. But I would find it much less convincing, because I don’t think strict categories are a very natural thing. (For what it’s worth, it’s also not true in HoTT that all homotopy types can be presented as the nerve of a 1-category, strict or not.)

There is however no conceptual reason that it is necessary to work with a cartesian product here: a monoidal structure, as with cubical sets, is all that is needed.

No conceptual reason, perhaps, but for technical purposes, a cartesian product can be a lot more convenient than a monoidal one. Note, for instance, that the product in question is supposed to represent the cartesian product in the (,1)(\infty,1)-category of \infty-groupoids, so it’s convenient if it is also the cartesian product on the point-set level. (One might even view this as a “conceptual” reason to work with a point-set-level cartesian product.)

(Which is not necessarily an argument against cubical sets. For instance, the cartesian product of cubical sets is perfectly good when applied to fibrant ones. It’s only when you bring non-fibrant ones into the picture that it gets wonky.)

Posted by: Mike Shulman on July 14, 2014 5:22 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

With regard to strict categories: I see, yes, that is what I would have expected. Thanks! I agree that the distinction is not fundamentally one of size, I used this just for ease of making the point.

But I would find it much less convincing, because I don’t think strict categories are a very natural thing.

I think one should be careful about taking this point of view too far: do you consider a group to be an unnatural mathematical object?!

I do think that strict categories are natural and important gadgets, and that the study of them is as much a part of category theory as the ‘objects only up to isomorphism’ perspective. That is one of the wonderful things about category theory: not only does it lead to insights on a ‘higher level of thought’ about mathematics, but categories are interesting ‘ordinary mathematical objects’ in their own right. Of course this philosophy goes back at least to Lawvere’s writings in the early days of category theory (viewing metric spaces as enriched categories, etc).

Nevertheless, I agree with the principal point that it is very desirable in category theory to have a foundations in which there is a distinction between the category of categories and the category of strict categories (to use the terminology that you suggest). This allows one to cleanly separate the ‘two sides of category theory’ of my previous paragraph.

(For what it’s worth, it’s also not true in HoTT that all homotopy types can be presented as the nerve of a 1-category, strict or not.)

Whilst it is not important for the rest of the discussion, I again think that this statement could be misleading without further clarification. By a ‘homotopy type’ here, do you mean a homotopy type as defined within homotopy type theory, or is it a synonym for an (arbitrary) type?

In the first case, I would be surprised by the strength of your assertion. I can certainly believe that considerable work would be needed to prove constructively that nerves of categories model all homotopy types. This is of course not the same as saying that it is not true!

In the second case, which I would guess is what you meant, what you claim is not surprising to me, because it appears to me that there is a kind of meta-type-mismatch: ‘nerve of a 1-category’ has been translated into homotopy type theory in one way, whilst ‘homotopy type’ has been translated in a completely different one!

Note, for instance, that the product in question is supposed to represent the cartesian product in the (∞,1)-category of ∞-groupoids, so it’s convenient if it is also the cartesian product on the point-set level. (One might even view this as a “conceptual” reason to work with a point-set-level cartesian product.)

Yes, it can be convenient, or can appear so at first. I wouldn’t regard it as conceptual: it depends, for instance, upon how one interprets (,1)(\infty,1)-categories and \infty-groupoids. What you ask for could still hold for a cubical notion of \infty-groupoid, even though a cubical homotopy is defined with respect to the monoidal structure.

Posted by: Richard Williamson on July 15, 2014 9:02 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

do you consider a group to be an unnatural mathematical object?!

Of course not.

I’m not sure what your object was in bringing up groups, but in case it was something along the lines of “groups are one-object groupoids”, let me point out that it is still true in HoTT that groups are equivalent to pointed connected groupoids. It is also true that groups are equivalent to pointed connected strict groupoids; but I see no reason not to think that the former fact is sufficient, without needing to discuss strict categories. Admittedly, the distance between groups and pointed connected groupoids is a bit larger than that between groups and pointed connected strict groupoids, but I think a bit of distance there is a good thing; much confusion has been created by the unthinking identification of groups with “one-object groupoids”. (-:

That is one of the wonderful things about category theory: not only does it lead to insights on a ‘higher level of thought’ about mathematics, but categories are interesting ‘ordinary mathematical objects’ in their own right.

I agree entirely with this, but it has nothing to do with the strict/non-strict distinction. Nothing prevents us from treating non-strict categories as “ordinary mathematical objects”; not all mathematical objects have to be set-based!

In my experience, in most of the places in traditional category theory where strict categories are useful, it is only because in set-theoretic foundations, every category is strictifiable. Since this is no longer true in HoTT, I think strict categories become much less useful. I’d be interested to hear if you have particular examples in mind?

In the second case, which I would guess is what you meant… ‘nerve of a 1-category’ has been translated into homotopy type theory in one way, whilst ‘homotopy type’ has been translated in a completely different one!

Yes that’s what I meant. I would argue that that is the correct translation of “homotopy type” into HoTT.

Posted by: Mike Shulman on July 15, 2014 5:58 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I agree entirely with this, but it has nothing to do with the strict/non-strict distinction. Nothing prevents us from treating non-strict categories as “ordinary mathematical objects”; not all mathematical objects have to be set-based!

I completely agree that there is no reason to consider ‘structured sets’ to be ‘ordinary mathematical objects’. The latter was perhaps an unfortunate choice of phrase, but it was intended to contrast with category theory as a ‘higher level of thought’: my point is that I consider strict categories to live on the ‘lower level’ at which groups, etc, live.

In this way, for me, what I wrote about the two sides of category theory has everything to do with the strict/non-strict distinction: that strict categories live at the level of groups, whilst non-strict ones live at the next level up, is something that I feel is inherent to the fact that category theory has these two sides.

I’m not sure what your object was in bringing up groups, but in case it was something along the lines of “groups are one-object groupoids”

No, my point is that can both groups and strict categories can be seen as arising in exactly the same algebraic way. For instance, they are both algebras for a monad on a presheaf category: the category of sets in the case of groups, and the category of directed graphs (say) in the case of strict categories. It seems entirely artificial to me to regard the one as natural, and the other as not. It is very doubtful to me that there could be any general principle for deciding upon whether the algebras for a given monad are ‘natural’ gadgets!

Rather, it is an insight that the notion of a category leads to a whole new world of mathematics that we know and love, and that in this new world we might wish not to work with equalities on objects. I don’t see any reason that this should mean that ‘old world’ categories viewed as living in this new world are unnatural.

In my experience, in most of the places in traditional category theory where strict categories are useful, it is only because in set-theoretic foundations, every category is strictifiable. Since this is no longer true in HoTT, I think strict categories become much less useful. I’d be interested to hear if you have particular examples in mind?

I agree that the ability to strictify categories would not be a conceptual reason to consider strict categories to be important.

I think that one example is exactly what prompted me to make my first comment, namely when it comes to working with nerves. The fact that simplicial/cubical sets are presheaf categories is rather significant. If we do not work with strict categories, how does the nerve naturally land in a presheaf category? Now, if we change the meaning of everything in sight considerably, there may be some way to do it. But I would be very doubtful that it can be done without losing some important aspect of the original story.

For a second example, suppose that we look at 2-categories instead. From the point of view that you are advocating, it would seem that one should argue that strict 2-categories (even with just a type of objects, without equality) are unnatural: that there is only a 3-category of 2-categories in homotopy type theory, and we should not be able to speak about arrows up to equality.

However, I would argue that in fact the theory of strict 2-categories is extremely important, and that one should work strictly wherever possible. A good example is the theory of 2-monads. I was happy to discover recently that this philosophy appears to have been propounded by Max Kelly (as mentioned in the introduction to the paper ‘Codescent objects and coherence’ of Lack).

I would argue that that is the correct translation of “homotopy type” into HoTT.

Yes, it of course often will be. But if homotopy type theory is intended to be a foundations for mathematics, we should be able to speak about ordinary homotopy theory inside it in a way which retains the original meaning. My point about the nerves of categories not modelling homotopy types is precisely that the original meaning is different from the translation into homotopy type theory that you suggested.

Posted by: Richard Williamson on July 16, 2014 10:38 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

that strict categories live at the level of groups, whilst non-strict ones live at the next level up, is something that I feel is inherent to the fact that category theory has these two sides.

I’m saying that I think that’s wrong. There’s no reason not to consider non-strict categories to also live at the level of groups.

It is very doubtful to me that there could be any general principle for deciding upon whether the algebras for a given monad are ‘natural’ gadgets!

Sure, but I don’t see why the lack of a general principle should prevent us from making such judgments in particular cases, any more than the unsolvability of the halting problem prevents us from observing that some programs terminate and others don’t. For instance, there is a monad whose algebras are sets equipped with a ternary relation aa and a 5-ary relation bb such that a(x,b(y,x,z,z,y),x)=b(a(x,x,x),y,z,z,a(z,y,y))a(x,b(y,x,z,z,y),x) = b(a(x,x,x),y,z,z,a(z,y,y)) for all x,y,zx,y,z, but I hope you would agree with me that such gadgets do not seem very natural.

Rather, it is an insight that the notion of a category leads to a whole new world of mathematics that we know and love, and that in this new world we might wish not to work with equalities on objects. I don’t see any reason that this should mean that ‘old world’ categories viewed as living in this new world are unnatural.

It’s not the existence of non-strict categories that makes strict ones seem unnatural; it’s the paucity of examples of strict ones. For instance, even the most basic category SetSet is not strict, and it’s not even strictifiable unless you do something unnatural like assume the axiom of choice.

I agree that the ability to strictify categories would not be a conceptual reason to consider strict categories to be important.

No, what I’m saying is that the inability to strictify categories is a conceptual reason to consider strict categories not to be important.

Strict 2-categories are an excellent case in point. Kelly’s philosophy is an excellent one: one should work strictly wherever possible. Why is it possible to use strict 2-categories? Because many naturally occurring 2-categories are strict, and all of them can be strictified. People don’t use strict 3-categories much because the analogous facts are false: naturally occuring 3-categories are not strict, and not all 3-categories can be strictified. So although it is “possible” to work with strict 3-categories in the sense that they have a formal theory, people don’t do it a whole lot because it doesn’t have many applications.

In HoTT, the same thing happens one level down: naturally occurring 2-categories, such as CatCat, are not strict and cannot be strictified. So strict 2-categories (and similarly strict 1-categories) are in the same situation that strict 3-categories are in set-based mathematics: one can develop their theory, but it’s not very useful because it doesn’t apply to the important examples.

Posted by: Mike Shulman on July 16, 2014 5:29 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I’m saying that I think that’s wrong. There’s no reason not to consider non-strict categories to also live at the level of groups.

The examples that you have mentioned so far are all large categories, important for the ‘higher level of thinking’ side of category theory, and I am very surprised that you advocate considering these categories on the same level as groups in any sense. Certainly I feel that this is not a natural thing to do! I am in addition surprised if this is a widely held view in homotopy type theory. I read Voevodsky’s early writings on this, especially ‘A very short note on the homotopy λ\lambda-calculus’, in exactly the opposite way.

Anyhow, I think we have now put forward our respective views, and can agree to disagree!

I hope you would agree with me that such gadgets do not seem very natural.

I feel that this is playing with words! I do not know any reason to consider these gadgets to be significant, but that does not mean that they would not be perfectly reasonable mathematical gadgets to consider (on the same level as groups and strict categories!) if this were found to be a useful thing to do.

It’s not the existence of non-strict categories that makes strict ones seem unnatural; it’s the paucity of examples of strict ones. For instance, even the most basic category Set is not strict, and it’s not even strictifiable unless you do something unnatural like assume the axiom of choice.

Again, I think the discussion has run its course, but I do feel that you have not really given any evidence to support your claim that there is a paucity of examples of strict categories. The example you cite is an instance of what I wrote above: Set\mathsf{Set} is a large category, used in the ‘higher level of thinking’ side of category theory. That it cannot be naturally strictified seems to me to fit precisely with the philosophy I am putting forward, that we should distinguish it from those categories in which we do wish to consider equalities on objects.

It is perfectly possible to construct small categories that are used, for instance, when working with nerves, as strict categories in a natural way. There is hardly a paucity of small categories!

One thing I would like to add is that my point of view is that equality should always be thought of as intensional, namely have constructive content. There are lots of interesting ways to think of strict categories in a way which fits with this. I would not wish it to be thought that I was advocating that it is essential to consider strict categories with a set of objects in the traditional sense.

No, what I’m saying is that the inability to strictify categories is a conceptual reason to consider strict categories not to be important.

Ah, then I entirely disagree! I wasn’t sure whether to interpet your comment in this way or the other, so I chose the one that I could agree with! As above, it is perfectly possible to construct typical small categories strictly.

naturally occurring 2-categories, such as Cat, are not strict and cannot be strictified. So strict 2-categories (and similarly strict 1-categories) are in the same situation that strict 3-categories are in set-based mathematics: one can develop their theory, but it’s not very useful because it doesn’t apply to the important examples.

That makes sense. My preferred foundational approach, though, would be one in which the 2-category of large/non-strict categories is strict. I do think that such an approach is possible in intensional Martin-Löf type theory, or an extension of it.

Posted by: Richard Williamson on July 17, 2014 12:24 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I do feel that you said some new things in your last post for me to respond to; at least, you clarified aspects of your position that I did not understand before.

Firstly, I would be very wary of concluding anything about the homotopy type theory community by reading only Vladimir’s writings. (-:

Secondly, I view it as exactly one of the strengths of category theory not only that the same definition of “category” includes both large and small examples, but that the large categories are no different in essence from the small ones and can be studied as mathematical objects in the same way, using the same techniques. (Someone pointed out to me once that this is an example of “reification”.) If we use 2-monadic techniques, for instance, to prove a coherence theorem for monoidal categories, it would be silly if we couldn’t apply that theorem to large monoidal categories as well! I think insisting on drawing a sharp boundary between “categories we study as objects” and “categories as mathematical universes” defeats the purpose of noting that they are both part of category theory.

I do not know any reason to consider these gadgets to be significant, but that does not mean that they would not be perfectly reasonable mathematical gadgets to consider… if this were found to be a useful thing to do. [emphasis added]

I agree entirely. What I’m saying is that strict categories are not a (very) useful thing to consider.

The example you cite is an instance of what I wrote above: SetSet is a large category, used in the ‘higher level of thinking’ side of category theory.

Sorry, I thought this would be clear. Any category built out of sets is also not strict, and that includes plenty of small ones as well as large ones. The category of finite sets is also not strict. Nor is the category of finite-dimensional vector spaces, or the category of finite-dimensional representations of a group. Or the category of finitely-presented models of a theory. Or the category of finite-dimensional manifolds. At least some of them can be strictified, but none of them occur strictly naturally.

What exactly is it that you want to do with nerves for which strict categories are useful? Note that a non-strict category also has a nerve; it’s just a simplicial 1-type rather than a simplicial set (0-type).

One positive advantage of non-strict categories, which applies also to small categories, is that you automatically get all the correct functors between them. With strict categories you have to use anafunctors.

Additionally, at the risk of sounding like a broken record, let me once again make the point about higher topos models. There, the correct notion of category (small or large) is undoubtedly a stack, and it’s just a fact that not every stack is strictifiable (even small ones). So even if certain small stacks happen to be strictifiable, the theory of categories that we want should not exclude the others.

My preferred foundational approach, though, would be one in which the 2-category of large/non-strict categories is strict.

That would require a very different setup from anything that I can imagine, and if I saw such a thing I’d probably question in what sense the categories were “non-strict”. The notion of strict 2-category requires a set-like equality on its morphisms, and it seems to me that for the 2-category CatCat that would require a set-like equality on the objects of the categories appearing in it; so in what sense could they be non-strict?

Posted by: Mike Shulman on July 17, 2014 3:04 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Ah, I realise from your examples that my use of ‘small’ was not very helpful: perhaps I should have used ‘very small’ instead (this is not meant seriously)! All of the examples that you list are of course still of the ‘higher level’ side of things. The kind of categories I have in mind are the free standing object, the free standing isomorphism, the free standing commutative square, and so on, built by hand for particular purposes. Also for instance the path groupoid of a simplicial/cubical set.

This brings me to your question…

What exactly is it that you want to do with nerves for which strict categories are useful? Note that a non-strict category also has a nerve; it’s just a simplicial 1-type rather than a simplicial set (0-type).

I am particularly interested in the homotopy hypothesis. In my opinion, the essence of this is that we can model homotopy types by up-to-isomorphism algebraic gadgets (eg, algebras for an ordinary monad). Thus I consider it the essence of the homotopy hypothesis that we model 1-types by strict groupoids.

But I have an instinct that there is more to it. My feeling is that we cannot just bypass, in the way that you suggest, presheaf categories in the ordinary sense, with their usual universal property, without losing things of importance.

I agree entirely with the paragraph beginning ‘Secondly’, and most of the rest of your comment. I do not wish to draw a sharp boundary between the two kinds of categories, just to say that if a mathematician finds it appropriate/useful to work with strict categories as algebraic objects (so having a 1-category of them), then I don’t think that there is anything a priori unnatural about that.

It may be that whether or not we consider strict categories to be useful is more a matter of taste or philosophy. Obviously I do, and I have tried to give some reasons, but it may be that they can be explained away: but not necessarily in a manner that is to my taste. In general, I see a tendency in homotopy type theory (arguably), and (definitely) in the fashionable approaches to higher category theory which take the homotopy hypothesis for granted, to brush vast swathes of mathematics under the carpet: this is not something that I am keen on, and I work mostly on the other side of the fence.

That would require a very different setup from anything that I can imagine, and if I saw such a thing I’d probably question in what sense the categories were “non-strict”.

Yes, indeed. I am currently writing in Coq work which uses the kind of foundations that I have in mind. I’m still tweaking aspects of it, so I’ll defer a discussion. One idea that I am keen on, though, is a kind of ‘synthetic category theory’, in which one extends ordinary intensional Martin-Löf type theory by introduction, elimination, and computation rules (as usual) which implement fundamental notions of category theory ‘directly into the type theory’. The only place in the literature where I am aware that this has been suggested is a paper of Dyckhoff. What I have in mind goes much further, though.

Posted by: Richard Williamson on July 17, 2014 6:53 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

In general, I see a tendency in homotopy type theory (arguably), and (definitely) in the fashionable approaches to higher category theory which take the homotopy hypothesis for granted, to brush vast swathes of mathematics under the carpet: this is not something that I am keen on, and I work mostly on the other side of the fence.

Perhaps we’ve been talking past each other. I’ve been talking about how I think category theory ought to be done in homotopy type theory, by which I mean more specifically constructive homotopy type theory.

Of course, not all mathematics is constructive! I like to think about it in terms of constructive mathematics being the math that’s true in “all worlds” (more precisely, all (higher) toposes) — while classical mathematics (with axioms like AC) is true only in a restricted subset of worlds, but has more powerful tools to decide questions that are open in general. Obviously, if your system has fewer models, then there’s more you can say about them. In general, I think constructive proofs are to be preferred when possible, because they say more: they tell you that a theorem is true in all toposes rather than just the classical ones.

Sometimes a theorem has traditional proofs that are not constructive, but it also has other proofs that are constructive (perhaps requiring more effort). In HoTT, being constructive in this sense doesn’t mean just avoiding LEM and AC; it also means avoiding strictifications that don’t exist in general. So, for instance, while strict 2-categories are a convenient crutch, if we can do without them (and I have little doubt that we can), we’ll get a version of 2-category theory that works in all higher toposes. Similarly, whatever homotopy-theoretic calculations we can do in constructive HoTT will also be true in all higher toposes.

On the other hand, sometimes a theorem is just not provable constructively, but requires classical axioms. This doesn’t make it wrong; it just means that rather than a general statement about mathematics in toposes, it’s a more specific statement about classical toposes. It’s certainly true that there are some homotopy-theoretic calculations that are of this sort; a major open problem in HoTT is to better understand the boundary between the two situations (e.g. how many of the higher homotopy groups of spheres are constructively determined?). And once we’ve decided that we’re okay with restricting our results to be about only classical toposes, then we are of course free to use LEM, AC, strictifications, and so on.

Your version of the homotopy hypothesis, that homotopy types can be modeled by up-to-isomorphism algebraic gadgets, is, I’m pretty sure, false in constructive homotopy type theory (or more precisely, provably not provable): there are topos models in which the universe of types does not admit any surjection from a 1-type. It may nevertheless be true classically, and it may be useful when true; but if we can avoid using it, then our results will be more generally applicable. Similarly, strict categories and simplicial-set nerves do have a few uses in classical mathematics, and those will probably also be valid in “classical HoTT”.

I think all the evidence is that we can do all of what I would call category theory using non-strict categories without any classical axioms, and I think the point about higher topos models argues strongly that this is the right way to do it. But one might argue this is more of a definition of “category theory” than a substantive claim about it. There are other uses of categories in mathematics, such as to present homotopy types via simplicial set nerves, that I would not classify as “category theory”, and those may require strict categories. I suspect that they will also not be very useful constructively, but in classical mathematics they may retain their value.

Posted by: Mike Shulman on July 19, 2014 8:08 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Perhaps we’ve been talking past each other.

I don’t think so: at least, the point of view that I understood you to be taking is the one that you have elaborated upon here.

A constructive approach to category theory is fundamental to my work. For example, I have worked a lot on the homotopy hypothesis, the construction of model structures, and so on, and, contrary to what appears to be popular belief, all of this is perfectly possible constructively, in a very strong sense. It is often not by any means immediate how to rework things, but I find that the methods actually give more insight than in the classical approaches.

One of the reasons for the feeling I expressed in the paragraph that you quoted is in fact evident in your comment. Whilst I certainly find the homotopy type theory programme most interesting, and believe that it will lead to much fascinating mathematics, I think it is important to keep things in perspective. A passing reader might easily infer from your comment that since the homotopy hypothesis as you interpreted it does not hold in homotopy type theory, it is not possible to prove constructively. However, as above, this is by no means necessarily the case.

Indeed, it seems to me that homotopy type theory more or less takes the homotopy hypothesis implicitly for granted. I feel that the ramifications of this are likely to be quite significant: I am not convinced, for instance, that taking homotopy type theory as a foundations will make it easier to obtain genuine insight into the ‘internal nature’ of higher categories, as opposed to ‘moving the difficulties elsewhere’. I realise that this view is probably against the tide.

There are other uses of categories in mathematics, such as to present homotopy types via simplicial set nerves, that I would not classify as “category theory”, and those may require strict categories. I suspect that they will also not be very useful constructively, but in classical mathematics they may retain their value

My concern is strengthened by remarks such as this. Firstly, one can of course work category theoretically with a category of strict categories, as with any other category. That this category may not be interpretable in homotopy type theory in the way that category theory is formulated there does not change this! I consider my work on the homotopy hypothesis to be entirely category theoretical, for instance. I think that it is hardly tenable at this stage in homotopy type theory’s development to take the extreme formalist position that category theory is defined by the particular formulation of it in these foundations! This of course does not preclude exploring this viewpoint.

Secondly, whether or not strict categories are useful is a point on which we differ, as we have discussed, but this usefulness has nothing to do with working constructively (as opposed to working in the formulation of category theory in constructive homotopy type theory that you have discussed), at least for the uses to which I have put strict categories.

while strict 2-categories are a convenient crutch

From one point of view. Another point of view might prefer, as I might, for instance, to take them, and other strict structures, as fundamental, and regard weaker structures as secondary. It might be possible to find an appropriate foundations for such a point of view that could equally well be interpreted in higher toposes.

Posted by: Richard Williamson on July 19, 2014 11:40 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I didn’t realize you were taking issue with the more general claim that category theory is fundamentally about isomorphism-invariant structures. Lots of ink has been spilled over that, on this blog and elsewhere, and if none of it convinces you then there’s no point in going further. I would like to point out, though, that this point of view was advocated by many people long before homotopy type theory came around; I’m certainly not saying that category theory is defined by a particular formulation of it in HoTT!

I’m sorry that I used “constructive” in a nonstandard way; I said specifically that I was talking about “constructive homotopy type theory”, and later I said that this “doesn’t mean just avoiding LEM and AC; it also means avoiding strictifications that don’t exist in general”. So your work may be constructive in a set-based sense, but not in the homotopical sense; the latter being (apparently) necessary for interpretation into higher toposes. I’m dubious that there is any way to make “strict structures as fundamental” interpretable in higher toposes, but of course something like that is hard to prove impossible, so feel free to have a go!

Finally, the “homotopy hypothesis” can also mean lots of different things. Tom made a nice graphic (scroll down to “What is the Homotopy Hypothesis?”) showing a continuum from Algebra/Logic to Topology. His point was exactly what I think you are saying: that to make the homotopy hypothesis trivial by defining “\infty-groupoid” to mean “space” (or Kan complex, or whatever) misses the point. That is, the homotopy hypothesis is about relating “algebraic” and “topological” objects.

Now in homotopy type theory, we have a new kind of thing in addition to everything on Tom’s continuum. We call them “types”. This essentially creates a whole new set of meanings of the homotopy hypothesis, since we can ask whether “types” are equivalent to globular-set \infty-groupoids and/or to topological spaces. This is the statement which I’m saying probably fails in some higher toposes.

The main point I want to make is that “types” are actually way over on the algebraic side of Tom’s graphic! We sometimes call them “homotopy types” or “spaces” because we work with them the way algebraic topologists do with their so-named objects, but if you actually look at the structure that they have, it’s nothing like a topological space and everything like an algebraic \infty-groupoid. We really ought to call them “synthetic \infty-groupoids”. So homotopy type theory is absolutely not “defining away” the homotopy hypothesis in the way that nonalgebraic approaches to higher categories do.

In fact, I feel that homotopy type theory is actually in the process of realizing Grothendieck’s original dream of doing homotopy theory with \infty-groupoids. Its methods, while sometimes inspired by classical algebraic topology, also use directly the algebraic and globular structure of types. I tried to make this point in my CT13 talk. What’s required is a shift in perspective on the homotopy hypothesis: rather than asking the theory of globular-set \infty-groupoids to be equivalent to that of spaces, we should ask the theory of synthetic \infty-groupoids to be modeled by spaces. This form of the homotopy hypothesis is a theorem, which is far from trivial: it’s the basic theorem of the semantics of HoTT, due to Voevodsky and others.

Posted by: Mike Shulman on July 21, 2014 7:59 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I didn’t realize you were taking issue with the more general claim that category theory is fundamentally about isomorphism-invariant structures.

I don’t feel that I am taking issue with this! I feel as though I am repeating myself, but the point I was making was simply that if we have a category of strict categories in whichever foundations we are working in, then we can still work perfectly category theoretically, in an isomorphism invariant way, with this category.

Whether or not we have, or wish to work with, a category of strict categories in our foundations is a separate question. As long as we do not take a formalist position which restricts us to particular foundations, we could be working category theoretically in any foundations, including those which permit reasoning in non isomorphism invariant ways (even though it is permitted, we might not make use of it).

When I wrote that one might wish to consider strict structures to be fundamental, I also do not consider this to be contrary to the spirit of category theory as about isomorphism invariant structures. I would say that the crucial shift is rather from viewing equality as extensional to intensional. If one works with propositional equality throughout, I think that it is perfectly possible in intensional Martin-Löf type theory to develop category theory in such a way that strict (intepreted intensionally rather than extensionally) structures are fundamental, but in which we can ensure that we only work categorically theoretically with objects up to isomorphism, etc. An important point is that once we shift to intensional equality, we have the freedom to specify ways to construct a term of a given identity type.

Many category theoretic constructions, whilst ordinarily thought of as weak (the passage from a category to the category of presheaves upon it, for instance), can be thought of as strict, and I do in fact consider that from a constructive point of view, this may be philosophically ‘correct’ (as long as equality is intensional). But this is a different story!

I’m sorry that I used “constructive” in a nonstandard way;

No need to apologise!

So your work may be constructive in a set-based sense, but not in the homotopical sense

As above, I would not say that the constructive point of view that I am putting forward is tied to sets, unless we consider a type in a type theory in which we have identity types to be a set. To find a model in extensional mathematics of the kind of foundations that I discussed above, one would need to work with homotopy types/higher groupoids.

His point was exactly what I think you are saying

Yes, indeed.

This is the statement which I’m saying probably fails in some higher toposes.

Yes. As I mentioned earlier, I would not consider the failure of the homotopy hypothesis under this interpretation to be surprising.

if you actually look at the structure that they have, it’s nothing like a topological space and everything like an algebraic ∞-groupoid

I agree with this.

So homotopy type theory is absolutely not “defining away” the homotopy hypothesis in the way that nonalgebraic approaches to higher categories do.

I’m not sure that I agree. I’ll explain what I mean by responding to the following…

What’s required is a shift in perspective on the homotopy hypothesis: rather than asking the theory of globular-set ∞-groupoids to be equivalent to that of spaces, we should ask the theory of synthetic ∞-groupoids to be modeled by spaces. This form of the homotopy hypothesis is a theorem, which is far from trivial: it’s the basic theorem of the semantics of HoTT, due to Voevodsky and others.

It’s a fascinating and beautiful fact that intensional Martin-Löf type theory has a homotopical semantics, and I of course agree (with or without univalence, etc) that this is not trivial. Nor is it, in my opinion, anything remotely approaching the strength of the original homotopy hypothesis, though!

It may help to think of Grothendieck \infty-groupoids, as studied by Maltsiniotis and Ara. We can observe that types can be thought of as Grothendieck \infty-groupoids (syntactically) or as homotopy types (semantically), but the homotopy hypothesis is the much stronger statement that these two points of view are equivalent, which is of course completely open.

Posted by: Richard Williamson on July 21, 2014 12:14 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

What do you mean by “fundamental”? It seems to me that if you’re treating the objects of strict categories isomorphism-invariantly, then you aren’t using the fact that they have a strict equality. So in what sense is that strict equality “fundamental”?

Posted by: Mike Shulman on July 21, 2014 7:16 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

It is the strict (but propositional) equality that is used in the definition of a category, of a 2-category, in defining category theoretic notions, and so on, which definitions are exactly as they usually are in a set theoretic foundations. Both the objects and the arrows are just types.

However, for any particular category (such as a category of categories) with type of objects AA, we a priori have no way to construct a term of type a:A,b:AId A(a,b)a:A, b:A \vdash \mathsf{Id}_{A}(a,b), and thus have the freedom to specify ways to do so if we so wish.

It is in this sense that the strict point of view is fundamental: it is the one built into the foundations of our category theory. We can choose to ensure that we can only work with objects of categories up to isomorphism, or we can choose to allow categories whose type of objects is a setoid, or even is a type with extensional equality: we can think of these as ‘modules’ that we may or may not choose to add to our foundations for a given purpose (as you know, this is not only a metaphor: the module formalism in Coq can be used to implement this kind of thing).

A nice feature of such a foundations is that the distance between the way that we think of categories and the implementation would seem to me to be quite small: with a little ‘syntactic sugar’, I think it would be possible to work with categories in such a foundations just as things with objects and arrows (sets of these, if one likes to think that way), etc, as usual (with or without considering equalities of objects as preferred), and somebody not interested in foundations need never know that what they are doing has constructive content!

Posted by: Richard Williamson on July 22, 2014 10:36 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

So it sounds like you’re saying, strict equality is fundamental because it’s there in the definitions, even though we never use it. I’m saying, what’s the point of insisting that it be there in the definitions if we’re never going to use it?

We can choose to ensure that we can only work with objects of categories up to isomorphism, or we can choose to allow categories whose type of objects is a setoid, or even is a type with extensional equality

This sounds to me like you are more or less describing what in HoTT we call a “precategory”. But those are not strict at all — strictness is one of the modules you can add, like univalence/saturation that makes them a (non-strict) category. Perhaps you are using the word “strict” differently from me? By “strict” I essentially mean “satisfying UIP”.

Posted by: Mike Shulman on July 22, 2014 10:50 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Perhaps you are using the word “strict” differently from me? By “strict” I essentially mean “satisfying UIP”

Yes, I think using ‘strict’ for the kind of foundations that I am describing is not particularly helpful. I am using only propositional equality, namely the weakest possible notion, not the notion of equality that you describe.

Whilst I would not do so otherwise, I kept using the term ‘strict category’ in this discussion because I wished to emphasise that the development of category theory in this kind of foundations is entirely alike usual (set based, say) category theory. In particular, we have a 1-category and a strict 2-category of categories, etc.

So it sounds like you’re saying, strict equality is fundamental because it’s there in the definitions, even though we never use it. I’m saying, what’s the point of insisting that it be there in the definitions if we’re never going to use it?

I hope things are a bit clearer now from what I have written above: strict equality in the sense that you had in mind is not used at all, but the notion of a ‘strict category’, interpreted intensionally, is fundamental. Rather than never using strict categories in this sense, we use them for everything, ‘in the abstract’: in this way, we have a kind of ‘synthetic category theory’, to use the term I mentioned a few comments ago.

However, we of course also need to construct particular examples of categories, not only prove results ‘in the abstract’. The main point that I wish to make is that once we move from extensional to intensional equality, we have the freedom to proceed, if we so wish, in such a way that when we make these constructions of particular categories, we can ensure that we cannot work with objects of them up to equality (strict in the sense you have in mind), only up to isomorphism (or equivalence if we are working with 2-categories, etc).

I do feel that there is a significant difference between this and the HoTT approach. I appreciate, though, that rather than describe it in words, it would be better for me to point you to, for instance, some Coq code in which you can see how what I am getting at works in practise. As I mentioned before, I am working on this at the moment, and can let you (or anybody else interested) know when I am happy enough with the formalism to make the repository publically available.

This sounds to me like you are more or less describing what in HoTT we call a “precategory”.

Possibly, yes. The arrows are also just a type in what I have in mind, though. I’m not sure whether this is the case for a precategory?

Indeed this is the one of the main reasons that I kept using the ‘strict category’ terminology: both the objects and arrows are treated in exactly the same way, which seems to me to be fundamentally different from the HoTT approach.

Posted by: Richard Williamson on July 23, 2014 8:40 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

To avoid confusion, perhaps I should also add that the ‘strict categories’ in the foundations that I have been describing are implemented as an extension of intensional Martin-Löf type theory, with introduction, elimination, and computation rules, as I mentioned before, and this is a very important aspect.

This is obviously very different from the way that a precategory would be implemented in HoTT.

Posted by: Richard Williamson on July 23, 2014 8:48 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Okay; I think only now do I fully understand that you’re talking only about a proposed totally new kind of foundations for category theory, rather than making any point about existing ones. But I still don’t have much of an idea what your proposed foundation is supposed to look like, or how you are using “intensional”, or what it means to have a “strict category” without strict equality. I would appreciating having a look as soon as you have something precise written out (although my preference would be for English over Coq).

Posted by: Mike Shulman on July 23, 2014 7:47 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

No problem, I’ll do that.

Okay; I think only now do I fully understand that you’re talking only about a proposed totally new kind of foundations for category theory, rather than making any point about existing ones.

The foundations are indeed new, although there is the paper of Dyckhoff from over 20 years ago that I cited above that points in the same kind of direction.

I wouldn’t quite say that I wasn’t making any point about existing foundations, though! Looking back over the discussion, I think that we have in fact touched upon quite a few significant aspects of the foundations of category theory in homotopy type theory which I am not myself convinced about.

I mentioned the foundations that I have outlined just as an attempt to give some evidence that an approach to the foundations of category theory in which a ‘strict’ point of view is fundamental but which is not contrary to the spirit of category theory as about ‘objects up to isomorphism’ is possible.

But I still don’t have much of an idea what your proposed foundation is supposed to look like, or how you are using “intensional”, or what it means to have a “strict category” without strict equality.

I entirely appreciate that. As above, I began discussing these foundations just as an example of an approach that might be taken which follows the point of view I have been putting forward, not as an attempt to convince anybody to adopt them in their own work.

Thanks for the discussion!

Posted by: Richard Williamson on July 24, 2014 10:43 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

In the interest of preventing any possible misunderstanding, perhaps I should emphasize that the 2-category CatCat of (non-strict) categories in HoTT does satisfy laws like F(GH)=(FG)HF(G H) = (F G) H as equalities, not just isomorphisms. It’s just that these are not equalities in an hset (i.e. a type satisfying UIP), but in a 1-type, so that they carry the same data as an isomorphism (by function extensionality and univalence). And thus one also needs to know that they satisfy the same sort of pentagon identities etc. that the corresponding isomorphisms do in a bicategory.

Posted by: Mike Shulman on July 23, 2014 4:39 AM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Richard wrote:

Anyhow, I think we have now put forward our respective views, and can agree to disagree!

Again, I think the discussion has run its course, but I do feel that you have not really given any evidence to support your claim that…

Hmm, I’m not sure that saying “let’s wrap this up, but here are some further points disagreeing with you” is an effective way to bring a discussion to an end…

Posted by: Tom Leinster on July 17, 2014 12:48 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

My apologies if it came across that way. I intended my further comments just as an elaboration upon aspects of my previous ones that seemed not to have been understood (with regard to which I did not feel that I was saying anything new)/as a summing up of aspects of Mike’s position that I personally don’t feel hold water, but upon which I don’t expect to be able to persuade Mike to any change of mind through further discussion!

Posted by: Richard Williamson on July 17, 2014 2:08 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

No problem at all. I’m glad to have your input here, and I’m sure Mike feels free to reply to anything he wants to reply to. It’s often hard, in conversations like this, to know which points of difference arise from misunderstanding and which reflect genuine differences of opinion. Maybe there’s no clean line between the two.

Posted by: Tom Leinster on July 17, 2014 2:16 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Thanks!

I’m sure Mike feels free to reply to anything he wants to reply to.

Yes, absolutely.

It’s often hard, in conversations like this, to know which points of difference arise from misunderstanding and which reflect genuine differences of opinion. Maybe there’s no clean line between the two.

Indeed!

Posted by: Richard Williamson on July 17, 2014 6:56 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

much confusion has been created by the unthinking identification of groups with “one-object groupoids”.

If you were to have some time, I think there would be worse uses of it than to write a post explaining just what is wrong with this identification — preferably without assuming any background in anything much.

I did some work on this kind of thing myself, e.g. on why one has to be careful about identifying one-object bicategories with monoidal categories, or (for somewhat different reasons) one-object monoidal categories with commutative monoids. But what you’re talking about seems more subtle, or else, I just don’t understand what you mean.

Since this has caused so much confusion, putting the explanation into a post of its own seems like a much better idea than burying it deep in a comments thread on Lebesgue integration…

Posted by: Tom Leinster on July 15, 2014 6:08 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

You’re right, that would be a nice idea. Maybe one day I’ll have some time. (-:

In brief, my opinion is that all the trouble is caused by leaving out the adjective “pointed”. When you include it, all the problems go away.

Posted by: Mike Shulman on July 15, 2014 7:44 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

I wonder how this relates to Tao’s remark that “probability theory is only “allowed” to study concepts and perform operations which are preserved with respect to extension of the underlying sample space.”

Freyd’s algebraic analysis also seems relevant. Especially in connection with the Haar measure on the circle, which is equivalent to the Lebesgue measure on [0,1].

Long ago I tried to construct the L 0L^0, the measurable functions, algebraically, in the spirit of Segal. Maybe there is a nicer way along the lines you suggest.

Posted by: Bas Spitters on July 11, 2014 2:37 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

Freyd’s algebraic analysis also seems relevant.

Yes. The keystone of that paper, Freyd’s startlingly simple characterization of the set [0,1][0, 1], appears on slide 6 of my talk and was also the starting point of all my work on this. (His paper didn’t appear until nearly a decade after he first posted the result on the categories mailing list.)

Posted by: Tom Leinster on July 11, 2014 2:49 PM | Permalink | Reply to this

Re: The Categorical Origins of Lebesgue Integration

This is somewhat changing the subject. Apologies if it sounds too off-the-wall. When I was a student in the 70s, I was mainly interested in mathematics, but I also took a number of film courses. I read various “structuralist” studies which identified a director’s style by taking isolated shots or thematic tropes out of context in a given film, but in many different films, one after the other.

I made the analogy, two-thirds of my life ago, that small details in a movie are analogous to the values taken by a function, and that the analysis of a film was analogous to the integral of the function. I assure you that no drugs were involved!

In this way, the newer film analysis was like the difference between the Lebesgue integral and the Riemann integral. In a Riemann integral, the order in which a function takes its values is paramount, and context is essential. This would be “old-style” film analysis. In a Lebesgue integral, we focus on the sizes of the sets where the function takes its values, and not whether these sets are connected, and the order in which a function takes its values is irrelevant. This would be the structuralist or semiotic analysis.

It cannot be an accident (can it?) that both sets of new ideas came from France.

Posted by: Bruce Reznick on July 15, 2014 9:06 PM | Permalink | Reply to this

Post a New Comment