## September 12, 2011

#### 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 $G F = 1_C$ and $F 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)$ of any Abelian category $A$. Given $A$, they define $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:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2437

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 $(\infty,1)$-categories.

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

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

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

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

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

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

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

than

$(X \times Y) \times Z \cong X \times (Y \times Z).$

(I have in mind here that $X, 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 $X$, $Y$ and $Z$, 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

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, 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

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)$; in my blog posts I wrote it as $Paths_X(x,y)$. Many type theorists write it as $x=y$ or $x\equiv y$, since they are used to thinking of it as a proposition of equality. Andrej Bauer suggested $x \rightsquigarrow y$ (in Coq, x ~~> y) and Peter Lumsdaine suggested $x \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

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 $Set$ 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

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

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

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

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

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

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

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

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

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

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

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