Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: joyal's topos talk, softness, and coherence spaces

Jonas Frey (Feb 15 2024 at 18:37):

I have some questions on Joyal's fascinating talk that is just wrapping up.

1. J said that coherence spaces are related to bicompletions. What precisely is that relationship? Are they a bicompletion? To me it sounds like the Sum-product-bicompletion is much bigger than coherence spaces?
2. What's the reference for the statement that bicompletions of *-autonomous categories are *-autonomous?

Nathanael Arkor (Feb 15 2024 at 18:40):

The nLab page [[free bicompletion]] includes the relevant references.

Jonas Frey (Feb 15 2024 at 18:41):

Yes, I saw that you recently added material on this to the nlab!

Kevin Arlin (Feb 15 2024 at 20:03):

Jonas Frey said:

2. What's the reference for the statement that bicompletions of *-autonomous categories are *-autonomous?

What, "Todd says André said this in 1995" isn't good enough for you? :rolling_on_the_floor_laughing:

Jonas Frey (Feb 15 2024 at 20:14):

Ahhh it's that kind of reference :smiley::smiley:

Nathanael Arkor (Feb 15 2024 at 20:16):

It's not that kind of reference (the statement is asserted in Joyal's papers); however it is the kind of reference that contains no proofs, and we just learnt from Joyal's talk that he didn't even prove for himself everything he asserted in that paper.

Nathanael Arkor (Feb 15 2024 at 20:17):

(I find it quite shocking that someone would submit a paper, even to a venue that does not require proofs, without proving all the statements on paper, but that's a different discussion.)

Jonas Frey (Feb 15 2024 at 20:20):

Hmm, maybe that's the kind of thing where it would be better for the community to state the claimed results as conjectures I guess.

Nathanael Arkor (Feb 15 2024 at 20:22):

It would be, but one certainly doesn't get that impression when reading the paper.

Jonas Frey (Feb 15 2024 at 20:22):

Or maybe he did have a proof at the time, and now he doesn't remember anymore

David Michael Roberts (Feb 15 2024 at 20:29):

Like the arithmetic universes proof of Gödel's incompleteness theorem... we didn't even get the definition pinned down

Jonas Frey (Feb 15 2024 at 20:35):

Anyway, this reminds me of Barwick's the future of homotopy theory where he writes

We do not have a good culture of problems and conjectures. The people at the top of our field do not, as a rule, issue problems or programs of conjectures that shape our subject for years to come. In fact, in many cases, they simply announce results with only an outline of proof – and never generate a complete proof. Then, when others work to develop proofs, they are not said to have solved a problem of So-and-So; rather, they have completed the write-up of So-and-So’s proof or given a new proof of So-and-So’s theorem. The ossification of a caste system – in which one group has the general ideas and vision while another toils to realize that vision – is no way for the subject to flourish. Other subjects have high-status visionaries who are no sketchier in details than those in homotopy theory, but whose unproved insights are nevertheless known as conjectures, problems, and programs.

(that's what I had in the back of my mind when writing the above comment)

John Baez (Feb 15 2024 at 21:05):

I think the nLab is dealing with attrbutions correctly (now, at least) when it says:

The above references do not contain proofs. For a sketch of the existence of free bicompletions of categories, see this MathOverflow question.

If we're in the sad situation where nobody can now publish a proof of this result because everyone thinks of it as Joyal's result, it would be good if interested people take Zhen Lin's argument on MathOverflow and complete it (or bicomplete it!) to obtain a proof, and then put that on the nLab.

Kevin Arlin (Feb 15 2024 at 21:12):

Zhen’s argument also doesn’t cover the dependence of the free $\kappa$-bicompletion on $\kappa$, in particular that the canonical maps you get for increasing $\kappa$ are fully faithful, which I think is critical to proving that the free bicompletion of a locally small category is still locally small. I think that’s the main part that’s not “routine” adjoint functor theorem business. I wonder whether it’s clear to anybody here why those functors are ff?

Nathanael Arkor (Feb 15 2024 at 21:19):

I think full faithfulness should follow from Joyal's generalisation of Whitman's characterisation of the free lattice. But that does not seem like a simple statement to prove. (Indeed, in the talk today, Joyal's method seemed to be different from the one he had originally envisaged.)

Todd Trimble (Feb 15 2024 at 21:41):

Kevin Arlin said:

Jonas Frey said:

2. What's the reference for the statement that bicompletions of *-autonomous categories are *-autonomous?

What, "Todd says André said this in 1995" isn't good enough for you? :rolling_on_the_floor_laughing:

In case it wasn't clear or you didn't see my wording, it wasn't like a casual comment over dinner. It was stated in his conference talk at CT '95 in Halifax before a packed house. (I mentioned it hoping that it would jog his memory a little.)

Todd Trimble (Feb 15 2024 at 21:50):

Maybe someone here knows Hongde Hu? He might be able to help.

Ivan Di Liberti (Feb 15 2024 at 22:07):

Nathanael Arkor said:

I think full faithfulness should follow from Joyal's generalisation of Whitman's characterisation of the free lattice. But that does not seem like a simple statement to prove. (Indeed, in the talk today, Joyal's method seemed to be different from the one he had originally envisaged.)

For Set monads, there is some remote chance that the coproduct of monads whose unit is a mono will have monomorphic unit "by construction". Here I have in mind the paper "Coproducts of Monads on Set" by Adamek et al. If this is any true, I am quite sure it would be using the following facts: coprojections are monos in Set, and that colimits of chains of monos are monos, the monads map monos to monos.

Nathanael Arkor (Feb 15 2024 at 22:09):

I was wondering whether full faithfulness of the unit could be deduced from full faithfulness of the embedding into the completion and cocompletion. It would certainly be satisfying if many of the formal properties of the bicompletion could be deduced from the fact it is a coproduct of pseudomonads.

Kevin Arlin (Feb 16 2024 at 00:03):

I guess it seems like I know that an object of the $\alpha$-bicompletion of $C$ is either an object of $C$ or a limit or colimit of an $\alpha$-sized diagram of objects of the $\alpha$-bicompletion of $C$; could I induct on this description using softness to see that I know exactly what the homs in such a bicompletion are, deduing the full faithfulness of the map into the $\beta>\alpha$-bicompletion from there?

Patrick Nicodemus (Feb 16 2024 at 00:45):

Jonas Frey said:

Anyway, this reminds me of Barwick's the future of homotopy theory where he writes

I am sure he means it in earnest when he says it is not meant to be arrogant. In spite of this good faith I have a hard time taking seriously the idea that homotopy theory is not a part of algebraic topology. To me this seems like trying to jettison the old-fashioned and historical - algebraic topology, ho-hum, how ancient and boring - in favor of the modern and exciting, higher categorical concepts. Algebraic topology is ancient stuff like Kan complexes (1958 - dinosaurs!) Homotopy theory is about modern concepts like infinity groupoids (Lurie, 2009 - cutting edge!) These two are obviously completely unrelated.

fosco (Feb 16 2024 at 11:05):

I mean, it takes even a bigger leap of faith to accept that algebraic topology is a branch of "these two points are close together" kind of math...

James Deikun (Feb 16 2024 at 12:59):

I think it's somewhat reasonable to consider homotopy theory as having branched off from algebraic topology as such, much the way that homological algebra has. After all, the $(\infty,1)$-category of $\infty$-groupoids has been discovered to have a level of mathematical universality that belies its historical origins--indeed so much so that it seems almost unnatural except in univalent foundations--and the practice has drifted pretty far too.

John Baez (Feb 16 2024 at 17:44):

I'd say a certain chunk of traditional algebraic topology is the study of what homotopy types and maps between them are like: we study invariants of them, try to classify them, etc. The new work is more about what we can do with homotopy types and maps between them: how we can set up math using these rather than sets as the fundamental structures, and what are the interesting features of this new kind of math.

John Baez (Feb 16 2024 at 17:47):

But I believe it's inevitable that the old work will inform the new work. When you start serious work using any sort of mathematical material - be it sets, groups, homotopy types or whatever - you eventually start wanting to know detailed facts about what those things are like.

John Baez (Feb 16 2024 at 17:50):

Nonetheless we are right now experiencing an immense growth phase in doing new math with homotopy types. This field is so immature that - right now - one can do a lot of interesting new things with homotopy types without relying much on the detailed wisdom algebraic topologists have about what homotopy types and maps between them are like.

Mike Shulman (Feb 16 2024 at 17:51):

If I were going to draw a line between "algebraic topology" and "homotopy theory" I might be inclined to say that algebraic topology is the study of algebraic invariants of topological spaces, while homotopy theory is the study of $\infty$-groupoids, and the relation between the two is that nearly all algebraic invariants of topological spaces factor through the fundamental $\infty$-groupoid functor.

Mike Shulman (Feb 16 2024 at 17:52):

But I'm not sure whether the antecedent of that conditional is true or not.