With Category Theory, Mathematics Escapes From Equality

Stream: maths

[Olli]

what do the mathematicians here think about this article: With Category Theory, Mathematics Escapes From Equality ?

[Olli]

something I found interesting having just watched The Future of Mathematics talk was finding out that topos theory is such a big deal amongst mathematicians, having only had exposure to it from studying type theory

[Olli]

in his talk @Kevin Buzzard said that the category theorists are retiring, but I would have considered topos theory to be a subfield of category theory

[Johan Commelin]

@Olli It's a well-written overview of a revolution that has been ripping through parts of mathematics in the last few years.

[Johan Commelin]

It's quite clear by now that infty-cats will play a big role in future maths. Most people are sort of warming up to them. But personally, I haven't seriously used them yet.

[Johan Commelin]

(Also, thanks for the link.)

[Johan Commelin]

One thing that I would really like to see is a good connection between HoTT and Lurie's infty-cats. Maybe @Reid Barton knows if there is a good article on this?

[Olli]

if formalization of FLT costs $100M, how much would it cost to formalize Lurie's work? it would this work be significantly different from the type of work that goes into proving FLT?

[Johan Commelin]

Yes, I think formalizing Lurie is easier. Possibly even easier when done in HoTT.

[Johan Commelin]

The amount of pages is a lot less, and the literature is quite linearly structured.

[Johan Commelin]

But then, I'm really an amateur on both these things.

[Olli]

would saying that formalising this type of work is more breadth oriented vs. depth oriented compared to proof of FLT be correct?

[Johan Commelin]

In some sense, yes, I think

[Olli]

so is there a chance that if you started with infinity categories, you'd actually finish the proof of FLT faster, because you had more flexible tools, or would that be something completely different?

[Olli]

the book I have on topos theory that I only just began reading presents it as a foundational system

[Olli]

and my impression is that most mathematicians care very little about foundational issues

[Olli]

but maybe they would care if it made their work easier? is that the promise?

[Johan Commelin]

Yes. But I think it wouldn't help very much for FLT

[Johan Commelin]

Although it would probably help if one were to really formalise parts of étale cohomology.

[Olli]

yeah I'm now really curious about the relationship between topos theory and HoTT, would love to hear more about that

[Johan Commelin]

And everything involving derived categories.

[Johan Commelin]

So yes, some parts of the FLT proof would be affected. But I wouldn't expect a major speed up. You'll lose more time by first formalising all Luries stuff, I guess.

[Johan Commelin]

Note, it's not just topos theory. It's higher topos theory.

[Johan Commelin]

Topos theory has been around for ages (-;

[Johan Commelin]

But for example, in the recent lecture notes by Scholze on condensed mathematics, he needs to glue some derived categories... this doesn't actually work. So what he does instead is climb up this infty-tower, and glue some infty-categories instead. That's a thing where these infty-categories really pay off.

[Olli]

that's cool, I wonder if there are any practical applications of infinity-CT outside of mathematics, besides perhaps in theorem proving (via HoTT)?

[Reid Barton]

The amount of pages is a lot less, and the literature is quite linearly structured.

In fact Jacob's current project https://kerodon.net/ is almost entirely self-contained.
On the other hand it hasn't quite gotten to the point where Higher Topos Theory begins yet

[Ulrik Buchholtz]

Re the connection between HoTT and (∞,1)-categories in set theoretic foundations: This is unfortunately a very sore spot for HoTT at the moment, as we don't know how to define the type of (∞,1)-categories. (We could do if we knew how to define the type of semi-simplicial types, but we don't.) Of course, we can define quasi-categories, but we then need to take the ∞-groupoid quotient by the Joyal equivalences, and we don't know how to do that. These problems all seem to require each other for their solution in HoTT, and noone knows where to start.
Note that this problem with analytically defining (∞,1)-categories etc. in HoTT occurs because we aim to represent higher mathematical objects by their correct type/∞-groupoid, and we're not content with a set-presentation thereof.
There is a work-around: work in HoTT as modeled in simplicial ∞-groupoids/spaces. Then we can work with (∞,1)-categories synthetically as complete Segal types, cf. Riehl-Shulman.
I wrote a book chapter for philosophers discussing these issues: Higher Structures in Homotopy Type Theory, and the situation is basically unchanged. (Meanwhile, there were a couple of promising attempts, but so far no luck.)

[Kevin Buzzard]

Thanks for this, Ulrik! Something that perhaps should be stressed on this thread is that Lurie's work is not just navel-gazing -- his work on these higher categories actually has applications in what I have sarcastically referred to in the past as "proper mathematics" (although this strategy is beginning to get me into trouble so perhaps I should stop doing it). So ultimately these questions will need to be solved.

[Ulrik Buchholtz]

Oh yes, and even applications to mathematical physics/foundations of physics, cf. e.g. work by Urs Schreiber and collaborators.

[Patrick Massot]

It's a well-written overview of a revolution that has been ripping through parts of mathematics in the last few years.
It's quite clear by now that infty-cats will play a big role in future maths. Most people are sort of warming up to them. But personally, I haven't seriously used them yet.

Notice for casual readers: 99.9% of mathematicians don't even know that infinity-categories exist and, most likely, they will never care. But people who love that stuff have a very strong tendency to oversell it, most probably because it's a very heavy technology that takes longer than expected to deliver applications (to abstract mathematics, not to the real world). Personally I'd love to know more about this stuff, but I really think that kind of propaganda should not exist in mathematics.

[Johan Commelin]

You are right... I should have better delimited this to e.g. arithmetic geometry and algebraic topology/homotopy theory.

[Keeley Hoek]

We had an undergraduate (infinity,1)-categories (as quasicategories) course last year!

[Kevin Buzzard]

Are you talking about ANU maths department?

[Keeley Hoek]

That's right.

[Scott Morrison]

(For the record, this had nothing to do with me. :-)

[Scott Morrison]

(And so now all the undergrads know more about (\infty,1)-categories than I do.)

[Johan Commelin]

You should make them formalise it :rolling_on_the_floor_laughing:

[Patrick Massot]

I just read the Quanta article. Unsurprisingly it loves the genius story, but I'm pretty sure many people will be very upset by how little they say about previous work.

[David Michael Roberts]

One thing that I would really like to see is a good connection between HoTT and Lurie's infty-cats.

(not really Lurie's infinity-cats, but I know what you mean)
Work of Mike Shulman is relevant here: https://arxiv.org/abs/1904.07004, the abstract reads in part

We prove the conjecture that any Grothendieck (∞,1)-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to (∞,1)-toposes, just as higher-order logic is used for 1-toposes.