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.

September 12, 2011

Who’s Your Friend?

Posted by David Corfield

Strange. No sooner had I set down ‘my friend Colin McLarty’ in the previous post, than I find him repaying the compliment here. Being an erudite man, however, he prefers to do so in Latin:

There is no category theory today without equality. And I don’t think there ever will be. Amicus <David> Corfield sed magis amica veritas. (p. 39)

This is a variant of Amicus Plato sed magis amica veritas (Plato is my friend, but truth is a better friend).

No detail is given there of the need for equality, but in his paper ‘There is no ontology here’, Chap 14 of The Philosophy of Mathematical Practice (preprint), Colin writes

Gelfand and Manin overstate an important insight when they call isomorphism ‘useless’ compared to equivalence:

“Contrary to expectations [isomorphism of categories] appears to be more or less useless, the main reason being that neither of the requirements GF=1 CG F = 1_C and FG=1 DF G = 1_D is realistic. When we apply two natural constructions to an object, the most we can ask for is to get a new object which is canonically isomorphic to the old one; it would be too much to hope for the new object to be identical to the old one.” (Gelfand and Manin, 1996, p. 71)

This is actually not true even in Gelfand and Manin’s book. Their central construction is the derived category D(A)D(A) of any Abelian category AA. Given AA, they define D(A)D(A) up to a unique isomorphism (1996, §III.2). They use the uniqueness up to isomorphism repeatedly. The notion of isomorphic categories remains central. Yet for many purposes equivalence is enough.

Gelfand and Manin’s book is Methods of Homological Algebra.

Can it really be that the derived category construction is usefully defined up to isomorphism?

Posted at September 12, 2011 5:06 PM UTC

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



25 Comments & 0 Trackbacks

Re: Who’s Your Friend?

Can it really be that the derived category construction is usefully defined up to isomorphism?

I like to make a distinction between “technical usefulness” and “moral usefulness”. I doubt that any “truly meaningful” mathematical theorems depend on defining the derived category up to isomorphism, rather than equivalence. But it could easily be that some “truly meaningful” theorems become easier to prove if one works with a version of the derived category which is defined up to isomorphism.

We see this phenomenon a lot in 2-category theory. Strict Cat-enriched limits and colimits (of which a derived category is, of course, one – a coinverter) are often much easier to work with than “fully weak” 2-dimensional limits, and in good situations can be used in place of the latter. This is not so different from using model categories or other strict models for (∞,1)(\infty,1)-categories.

Posted by: Mike Shulman on September 12, 2011 9:00 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Is there any difference in spirit between your claim

I doubt that any “truly meaningful” mathematical theorems depend on defining the derived category up to isomorphism, rather than equivalence. But it could easily be that some “truly meaningful” theorems become easier to prove if one works with a version of the derived category which is defined up to isomorphism.

and a variant one step down the ladder

I doubt that any “truly meaningful” mathematical theorems depend on defining the algebraic completion of a field up to equality, rather than isomorphism. But it could easily be that some “truly meaningful” theorems become easier to prove if one works with a version of the algebraic completion which is defined up to equality?

Posted by: David Corfield on September 13, 2011 8:21 AM | Permalink | Reply to this

Re: Who’s Your Friend?

I think those claims are different. In the first case, there’s no obstacle to performing the relevant construction (inverting some morphisms) functorially up to isomorphism, even though the universal property only guarantees uniqueness up to equivalence. But there is no functorial way to algebraically complete a field.
Talking about “the” algebraic closure of a field is analogous to talking about the homotopy groups of a space without first choosing a base point. It’s often convenient but a good way to make mistakes if you’re not careful.

Posted by: Jacob Lurie on September 13, 2011 12:29 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Ah, thanks. Base points and completions have been discussed before.

So was it that I didn’t choose my example well, or has some new phenomenon emerged at the level of categories, where it’s useful to tighten up the ‘sameness’ relation from equivalence to isomorphism in a way that’s not already present in tightening from isomorphism to equality of structured sets? What if I choose a situation with some kind of structured set, and a fixed operation:

I doubt that any “truly meaningful” mathematical theorems depend on defining the tangent bundle of a manifold up to equality, rather than isomorphism. But it could easily be that some “truly meaningful” theorems become easier to prove if one works with a version of the tangent bundle which is defined up to equality

where the tangent space construction is given via specified means, e.g., via derivations?

Posted by: David Corfield on September 13, 2011 1:41 PM | Permalink | Reply to this

Re: Who’s Your Friend?

In that case, I’d say the analogy is good: there doesn’t seem to be any qualitative difference between the two situations. But there may be a “quantitative” difference, in that the issue comes up more often as the category number increases. For example, categories have three notions of “sameness”: equality, isomorphism, and equivalence. Should each of these have its own notation? Would that make things more confusing or less? (I suspect the answer depends on the audience.)

Posted by: Jacob Lurie on September 13, 2011 2:23 PM | Permalink | Reply to this

Re: Who’s Your Friend?

There’s an argument that it’s better to write, say,

(X×Y)×Z=X×(Y×Z) (X \times Y) \times Z = X \times (Y \times Z)

than

(X×Y)×Z≅X×(Y×Z). (X \times Y) \times Z \cong X \times (Y \times Z).

(I have in mind here that X,Y,ZX, Y, Z are arbitrary objects of an arbitrary category with products.) Both are misleading to some extent. The first is misleading because it’s false. The second is misleading because it drastically understates the case: the point (usually) isn’t that there simply exists an isomorphism between the two sides, but that there is a canonical system of isomorphisms, one for each XX, YY and ZZ, obeying the usual coherence laws. Writing this as equality has its advantages, I think.

Posted by: Tom Leinster on September 13, 2011 4:42 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Is this because it’s ‘really’ about relating 1-morphisms by a 2-morphism? Or even 2-morphisms by a 3-morphism if you worked with X,Y,ZX, Y, Z in a monoidal category seen as a one-object bicategory?

Posted by: David Corfield on September 13, 2011 5:40 PM | Permalink | Reply to this

Re: Who’s Your Friend?

The first is misleading because it’s false.

Unless you redefine “==”.

Something like this comes up in homotopy type theory, where we have to decide on a notation for the “equality/identity/path/equivalence type”. Martin-Löf wrote it as Id X(x,y)Id_X(x,y); in my blog posts I wrote it as Paths X(x,y)Paths_X(x,y). Many type theorists write it as x=yx=y or x≡yx\equiv y, since they are used to thinking of it as a proposition of equality. Andrej Bauer suggested x⇝yx \rightsquigarrow y (in Coq, x ~~> y) and Peter Lumsdaine suggested x∼yx \sim y (in Coq, x ~ y).

For a while, I was adamant that the symbol should not be “==” (since in homotopy type theory, the identity-type represents equivalence rather than equality), and that it should moreover be a directed symbol (since even though all paths are invertible, inverting them is a nontrivial operation, unlike inverting an equality). Recently, though, I’ve been starting to come around to a view like the one you mentioned, and want to use just “==”.

Posted by: Mike Shulman on September 13, 2011 6:40 PM | Permalink | PGP Sig | Reply to this

Re: Who’s Your Friend?

there doesn’t seem to be any qualitative difference between the two situations. But there may be a “quantitative” difference, in that the issue comes up more often as the category number increases.

I agree.

For example, categories have three notions of “sameness”: equality, isomorphism, and equivalence.

That’s certainly one reason for the quantitative difference: there just are more gradations of meaning. Another possible reason is that as category number increases, the “fully weak” statements become more complicated, motivating us to look for stricter versions.

More controversially, one might point out that the traditional basis of mathematics (set theory) is essentially 1-categorical. Sets are 0-categories, and SetSet is a 1-category, and all higher categories are defined in terms of sets. In particular, the extra strictness is always there to be used if we want it, and the language we use is best adapted to talk about 1-categorically strict things.

One might, therefore, expect that with a truly higher-categorical foundation, there would be less strictness around that we could use, but the language would be better-adapted to doing without it. And I would say that this is what we do see, to a certain extent, with homotopy type theory—though it is still in its infancy as a foundation for mathematics.

Posted by: Mike Shulman on September 13, 2011 6:25 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Hence, FOLDS. But compared with HoTT, it seems less ‘popular’. Not that I’m aware that anyone has tried, but it is amenable to becoming automated? HoTT clearly was “easy” to do, as Coq, Agda etc are actually based on type theory.

Posted by: David Roberts on September 13, 2011 10:16 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Ah cool, thanks. I guessed that the ‘DS’ in FOLDS linked it with some sort of dependent-type-like theory.

Posted by: David Roberts on September 14, 2011 6:28 AM | Permalink | Reply to this

Re: Who’s Your Friend?

FOLDS is actually just a fragment of the dependent type theory that HoTT uses. FOLDS stands for First-Order Logic with Dependent Sorts — “dependent sorts” is another way of saying “dependent types”, and “first-order” identifies the fragment under consideration. So FOLDS already is automated in Coq and Agda; just don’t use any higher-order constructions.

I suppose one caveat to that is that often FOLDS is applied to infinitary schemes, such as globular sets or opetopic sets, whereas Coq and Agda are essentially finitary: you can’t write down infinitely many types (except as a type dependent over some “infinite” type like the natural numbers). This is a serious issue that people (including me) are actively thinking about.

Posted by: Mike Shulman on September 14, 2011 2:21 AM | Permalink | Reply to this

Re: Who’s Your Friend?

Jacob wrote:

But there may be a “quantitative” difference, in that the issue comes up more often as the category number increases.

One interesting “quantitative” phenomenon is the structure formed by different levels of strictness and different strictification results.

For example, for 3-categories, I don’t think it’s fully understood what that structure looks like. I’m thinking particularly of the fact that on the one hand, every tricategory is equivalent to a Gray-category, but on the other, every tricategory is equivalent to one in which everything apart from the identities is strict. These two types of strictification go in different directions: neither result immediately implies the other. And maybe there are further similar results about 3-categories that we don’t yet know.

The most naive conception is that there’s a poset of different levels of strictness (for 3-categories, say), and some of the edges in the Hasse diagram are marked red to show that you can turn a weaker thing into a stricter one. (For example, there’d be a red edge between “tricategory” and “Gray-category”.) That’s almost certainly too crude a way to think about it, but I don’t think we know even this crude picture in dimension 3.

Posted by: Tom Leinster on September 13, 2011 7:26 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Jacob Lurie wrote:

But there is no functorial way to algebraically complete a field.

That’s true. But for ordered fields, I think there is a functorial way: first form the real closure, and then adjoin a square root of −1-1. The key is that given an order-preserving homomorphism between ordered fields, there is a unique order-preserving homomorphism between their real closures that extends it. There is some discussion on this at the nLab.

Posted by: Todd Trimble on September 13, 2011 2:19 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Is the following related?
Constructively, the algebraic closure lives in a new topos.

Posted by: Bas Spitters on September 13, 2011 8:41 PM | Permalink | Reply to this

Re: Who’s Your Friend?

We discussed that idea back here, but I think without coming to any clear conclusion.

Posted by: David Corfield on September 14, 2011 8:53 AM | Permalink | Reply to this

Re: Who’s Your Friend?

About your

distinction between “technical usefulness” and “moral usefulness”,

do you distinguish further between “moral usefulness” and “moral rightness”, or are you some kind of utilitarian pragmatist who might equate the two?

Posted by: David Corfield on September 13, 2011 10:35 AM | Permalink | Reply to this

Re: Who’s Your Friend?

do you distinguish further between “moral usefulness” and “moral rightness”?

In case anyone listening in is confused, let me remind everyone that the meaning of “moral” here has nothing to do with ethics.

Probably what I meant to say was “moral rightness” – I’m not exactly sure what “moral usefulness” would mean.

Posted by: Mike Shulman on September 13, 2011 6:32 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Thanks for the link to Eugenia Cheng’s paper, which I am enjoying, greatly.

I don’t agree with her “This is not the same dichotomy as the \problem solver/theory builder” dichotomy as
highlighted by Tim Gowers [Gow00].” because morally they ought to be. I suspect Theory Building is strategically moral (even when pragmatic tactics are used) while Problem Solving is strategically pragmatic even when moral tactics are applied.

Posted by: Roger Witte on September 14, 2011 9:56 AM | Permalink | Reply to this

Re: Who’s Your Friend?

I agree that they *ought* to be the same dichotomy, but don’t think in reality they *are*.

Posted by: Eugenia Cheng on September 5, 2012 9:18 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Congrats, Eugenia, you get the n-Cafe necromancer badge!

Posted by: Mike Shulman on September 5, 2012 9:51 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Yes, it’s a great honor, the necromancer badge. Part of what I love about it on MathOverflow is that I can never figure out what acts of necromancy I was involved in. As if I regularly have spells of amnesia about my nefarious activities, like in the movie Angel Heart.

Posted by: Todd Trimble on September 6, 2012 7:07 AM | Permalink | Reply to this

Re: Who’s Your Friend?

Here is a comment from an amateur who started mathematics in homotopy theory in the 60’s:

I think in the early 90’s it was especially useful , it seemed to Manin et al, to emphasize the distinction between… and the relative importance of… the two notions isomorphism and equivalence. The former being accepted and familiar everywhere and latter only in certain provinces. Actually the nuance has still not yet arrived in certain parts of mathematics. In these cases like hard PDE the lack is probably not important in many problems…. some of which are local and non invariant coordinates can be chosen once and for all. However, it helps any problem to know more about its setting and meaning and the categorical viewpoint, we learned in the 60’s from Grothendieck, provides unexpected insight into such diverse areas as arithmetic and topological vector spaces.

Dennis Sullivan

Posted by: dennis sullivan on October 13, 2018 8:30 PM | Permalink | Reply to this

Re: Who’s Your Friend?

A name often encountered by those following Urs Schreiber’s research on M-theory, e.g., here, for your formulation of rational homotopy theory.

Regarding PDEs, I posed the question once of why we don’t hear about differential equivalences, to which Urs replied:

A differential equation is an equalizer of two maps out of a jet bundle in the Cahier topos sliced over some base Σ\Sigma, and it is formally integrable precisely if this inherits the structure of a coalgebra over the jet comonad. Now the homotopified version of this statement verbatim applies to the ∞\infty-Cahiers topos. The resulting “differential equivalence” or maybe “differential homotopy” is then the homotopy equalizer between two morphisms out of a jet ∞\infty-bundle of an ∞\infty-bundle, and this is formally integrable precisely if it is an ∞\infty-coalgebra over the jet ∞\infty-comonad.

This is written up in Synthetic geometry of differential equations: I. Jets and comonad structure.

Posted by: David Corfield on October 14, 2018 11:08 PM | Permalink | Reply to this

Re: Who’s Your Friend?

Interesting to come back to this thread 7 years later. I was talking with Colin again about these issues this summer in Beijing. Again he raised the issue of what is taught in graduate textbooks on homology theory as an indication of the continuing importance of the notion of isomorphism of categories.

Regarding textbooks, on whether Jacob Lurie’s ‘Higher Algebra’ could be used as the basis for a grad course, someone on MathOverflow writes:

One could argue this is the next logical step of a progression. Older books in homological algebra refused to use spectral sequences. Then Weibel’s highly praised book does the opposite and introduces them early on, but relegates derived categories to a final chapter. Then Gelfand-Manin take it one step further and start with derived categories. They discuss dg-algebras and model categories at the very end and stop short of discussing non-abelian derived functors. Lurie’s higher algebra is the next step but it’s also quite big and not meant to be used for lectures…

Lurie explains why we should go beyond Gelfand-Manin in Weil’s Conjecture for Function Fields I 2.1.1 Motivation: Deficiencies of the Derived Category

The theory of derived categories is a very useful tool in homological algebra, but has a number of limitations. Many of these stem from the fact that D(Λ)D(\Lambda) is not very well-behaved from a categorical point of view. The category D(Λ)D(\Lambda) does not generally have limits or colimits, even of very simple types…

…categorical issues with the derived category stem from the fact that we are identifying chain-homotopic morphisms in D′(Λ)D&#8242;(\Lambda) without remembering how they are chain-homotopic…

It is possible to correct many of the deficiencies of the derived category by keeping track of more information. To do so, it is useful to work with mathematical structures which are a bit more elaborate than categories, where the primitive notions include not only “object” and “morphism” but also a notion of “homotopy between morphisms.

So this next step from Gelfand-Manin to Lurie is to take ‘homotopical algebra’ as primary, and ‘homological algebra’ as a ‘linear approximation’ (as the nLab suggests).

Lecture notes for graduates (online, but delivered) adopting this approach are here.

Posted by: David Corfield on October 14, 2018 11:24 PM | Permalink | Reply to this

Post a New Comment