Zulip Chat Archive

Stream: Is there code for X?

Topic: category of pro-objects

Kevin Buzzard (Mar 30 2023 at 14:43):

I just searched for this and there are several instances of people saying "we need the category of pro-objects" but I never found any evidence that anyone had actually made it, either in mathlib or LTE. Is it there and I missed it, or is it still not there? I need it :-) (for a student)

Adam Topaz (Mar 30 2023 at 14:48):

It’s not there

Kevin Buzzard (Mar 30 2023 at 14:48):

Thanks for putting me out of my misery :-)

Adam Topaz (Mar 30 2023 at 14:50):

@Bhavik Mehta was working on it at one point (by viewing it as a subcategory of the category of presheaves) but I don’t think it was ever completed. It’s definitely something we should have. In LTE we had a special case that roughly worked for Profinite sets as if it was Pro(Finite), but we only developed the minimal API that was needed

Kevin Buzzard (Mar 30 2023 at 16:49):

I want Pro(Artin local O-algebras with residue field k), for O some Noetherian local ring with residue field k.

Adam Topaz (Mar 30 2023 at 16:56):

Schlessinger's criterion eh?

Yaël Dillies (Mar 30 2023 at 16:57):

@Paul Lezeau? :eyes:

Paul Lezeau (Mar 30 2023 at 17:02):

@Yaël Dillies Hm I haven't written that yet but I am hoping to formalize it as soon as I'm done with exams

Kevin Buzzard (Mar 30 2023 at 17:13):

You're going to be at Imperial next year, right? That'll be interesting.

Paul Lezeau (Mar 30 2023 at 19:29):

That's the plan!

Paul Lezeau (Mar 30 2023 at 19:32):

I'm hoping to take the number theory/ geometry formalisation course if it runs next year;)

Markus Himmel (Mar 31 2023 at 05:50):

I wrote down the definition (or more precisely its dual) at branch#ind_object last year, but I felt that there are quite a few things missing about limits and Yoneda before it really makes sense to talk about the categories of ind-objects and pro-objects. I was working with the book "Categories and Sheaves" by Kashiwara and Schapira.

Reid Barton (Mar 31 2023 at 06:35):

There are several ways to construct the ind- (or pro-) completion. Kevin what do you need specifically about it? You might just write down the API you need as constant/axioms and leave it to others (or yourself) to construct later

Kevin Buzzard (Mar 31 2023 at 06:54):

I wanted (by which I mean a student of mine wanted) to state various criteria for functors coming from deformation theory of Galois representations to be representable