category of pro-objects

Stream: Is there code for X?

[Kevin Buzzard]

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]

It’s not there

[Kevin Buzzard]

Thanks for putting me out of my misery :-)

[Adam Topaz]

@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]

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

[Adam Topaz]

Schlessinger's criterion eh?

[Yaël Dillies]

@Paul Lezeau? :eyes:

[Paul Lezeau]

@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]

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

[Paul Lezeau]

That's the plan!

[Paul Lezeau]

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

[Markus Himmel]

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]

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]

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

[Adam Topaz]

Prorepresentability is also important for things like étale fundamental groups. We should probably develop a general API for such things

[Matthew Ballard]

I just looked at the definition of power series

[Adam Topaz]

What do you mean?

[Matthew Ballard]

Given this discussion, I was curious if/how formal power series were defined.

[Kevin Buzzard]

Bet it's just nat -> R

[Adam Topaz]

Yeah that’s essentially it

[Adam Topaz]

And I think we’re missing the connection with the adic completion of a polynomial ring

[Matthew Ballard]

It laments this in the doc string

[Adam Topaz]

docs#power_series

[Matthew Ballard]

Once I-adic completion (topological or algebraic) is available it should not be hard to fill in the details.

[Kevin Buzzard]

I think I-adic (that's $I$-adic, not $\ell$-adic I guess) completion is now available? Or am I being over-optimistic?

[Adam Topaz]

docs#adic_completion

[Adam Topaz]

@Coleton Kotch you might be interested in this discussion

[Christian Merten]

@Markus Himmel: Do you have further plans with ind objects?

In particular (that's why I am reopening this old thread), have you thought about the best way to dualise docs#CategoryTheory.Limits.IndObjectPresentation to pro objects? I would like it to look like this:

import Mathlib.CategoryTheory.Limits.Indization.IndObject

universe v u

open CategoryTheory Limits

variable {C : Type u} [Category.{v} C]

structure ProObjectPresentation (A : C ⥤ Type v) where
  I : Type v
  [ℐ : SmallCategory I]
  [hI : IsFiltered I]
  F : I ⥤ Cᵒᵖ
  ι : F ⋙ coyoneda ⟶ (Functor.const I).obj A
  isColimit : IsColimit (Cocone.mk A ι)

This should be the FGA definition. In particular it is about covariant functors, while in Kashiwara-Shapira pro-objects are defined as a subcategory of contravariant functors (i.e. presheaves). Are you okay with this?

Second question: I need a pro-yoneda lemma, i.e. given an inverse system $\tilde X = (X_i)_{i \in I}$ of objects in a category $\mathcal{C}$, denote by $h_{\tilde X}$ the induced functor $\mathcal{C} \to (Sets)$ sending $Y$ to $\varinjlim_{i} \mathrm{Hom}_{\mathcal{C}}(X_i, Y)$. Then $\mathrm{Hom}(h_{\tilde X}, F) \cong \varprojlim_{i} F(X_i)$. Are you working on something related? If no, I'll start doing it.

[Kevin Buzzard]

If you want a test case, then I'm very interested in deforming a representation $G\to GL_2(k)$ ($k$ a perfect field of characteristic $p$) to the category of Artin local $W(k)$-algebras with residue field $k$...

[Christian Merten]

Kevin Buzzard said:

If you want a test case, then I'm very interested in deforming a representation $G\to GL_2(k)$ ($k$ a perfect field of characteristic $p$) to the category of Artin local $W(k)$-algebras with residue field $k$...

If I knew what that means, I would be happy to try ;-)

[Kevin Buzzard]

Mazur introduced, and Wiles used to great effect, this idea. If $k$ is a finite field then one can consider the category of commutative rings $R$ which are finite (as sets), local (i.e. have a unique maximal ideal $m$) and have a fixed identification $R/m=k$. Given a group homomorphism $\rho:G\to GL_n(k)$ we could define a lift of $\rho$ to $R$ to be a homomorphism $\tilde\rho:G\to GL_n(R)$ which reduces mod $m$ to $\rho$. Mazur observed that under some mild hypotheses on $G$, this functor was prorepresentable, and raised the question that if $G$ was a Galois group and $\rho$ came from some arithmetical situation (e.g. the $p$-torsion in an elliptic curve) then perhaps the prorepresenting object was arithmetically significant. Wiles showed that it was isomorphic to a Hecke algebra, and FLT followed. I'm going to need all of this machinery at some point in the near future, so I'm particularly interested in being able to state that this functor is prorepresentable.

[Christian Merten]

By "this functor" you mean the functor sending a representation over $k$ to the set of lifts to $R$?

[Kevin Buzzard]

Yes that's right, sorry for being unclear!

[Kevin Buzzard]

In fact the Mazur/Wiles situation has G a topological group and all representations continuous (i.e. with open kernel).

[Kevin Buzzard]

The idea is that there is a universal representation to $GL_n(R^{univ})$ explaining all lifts but now $R^{univ}$ is a pro-object in the category of these finite rings, so it can be thought of as a profinite ring.

[Christian Merten]

Kevin Buzzard said:

Yes that's right, sorry for being unclear!

So everything covariant here, I take that as a vote for the FGA definition.

[Christian Merten]

Kevin Buzzard said:

In fact the Mazur/Wiles situation has G a topological group and all representations continuous (i.e. with open kernel).

This reminds me that I also need a proper definition of continuous representations for Galois categories (currently its very ad hoc).

[Markus Himmel]

I'm happy with any definition for the ind-category and the pro-category as long as there are equivalences IndCategory C ≌ FullSubcategory IsIndObject (where IsIndObject A might as well be defined as IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall.{v} (CostructuredArrow yoneda A)) and ProCategory C ≌ (IndCategory Cᵒᵖ)ᵒᵖ compatible with the various Yoneda embeddings and inclusions. I'm primarily interested in abstract limit-colimit properties of the categories and functors C ⥤ IndCategory C, IndCategory C ⥤ Cᵒᵖ ⥤ Type v, C ⥤ ProCategory C, ProCategory C ⥤ (C ⥤ Type v)ᵒᵖ, and everything I need follows from the two equivalences above. My only plan regarding the category of pro-objects so far was to transfer all the abstract properties from the category of ind-objects using the above equivalence. So I think that we should choose whatever definitions make working with ind-objects and pro-objects easiest in practice, and I should be able to make the formal stuff work form there.

[Markus Himmel]

Regarding the pro-yoneda lemma: I don't think something related is on my roadmap. I have a version of the Yoneda lemma involving colimits here, but it's different (the colimit is in the codomain instead of the domain).

[Markus Himmel]

To answer the more general question about my plans for ind-objects: I'm currently working on the following things:

• ind-objects are closed under filtered colimits (this is done here, I'm currently in the process of PRing the prerequisites)
• if C (is small and) has finite limits, then a presheaf is an ind-object if and only if it preserves finite limits
• hom-sets between ind-objects are small
• prerequisites about comma categories needed for the description of morphisms of ind-objects in terms of natural transformations of the functors defining them (after a suitable restriction)

There are many more things that I will definitely need:

• the universal property
• the functor C ⥤ IndCategory C preserves finite colimits
• if C has finite limits, then IndCategory C has finite limits and the functors C ⥤ IndCategory C and IndCategory C ⥤ Cᵒᵖ ⥤ Type v preserve finite limits
• if C has finite colimits, then IndCategory C has finite colimits (and hence also small colimits)

From there, my plan is to move on to the case where C is small and abelian, showing the equivalence between IndCategory C and LeftExactFunctor C AddCommGroup and working towards the statement that IndCategory C is a Grothendieck category.

[Markus Himmel]

One thing I've been wondering about is the characterization of hom-sets of pro-objects in terms of limits of colimits of hom-sets in C, see for example Lemma 2.6 on the nlab page on pro-objects. Kashiwara-Schapira only seem to need this to show that the pro-category is locally small. Is this characterization useful in applications? If so, it might be a good time to start thinking about how to make it ergonomic in Lean.

More generally, how do people work with morphisms of ind-objects and pro-objects in practice?

[Kevin Buzzard]

I am slightly nervous about the plan "prove everything for ind objects and deduce for pro objects" but only because in mathlib right now the general principle seems to be "do everything twice rather than attempting to deduce eg the theory of colimits from the theory of limits"

[Kevin Buzzard]

I think that in the FLT work people just informally pass from the pro-objects in the category of finite-as-a-type rings with residue field Z/p to an appropriate category of complete local Z_p-algebras with residue field Z/p and continuous morphisms...

[Markus Himmel]

Kevin Buzzard said:

I am slightly nervous about the plan "prove everything for ind objects and deduce for pro objects" but only because I'm mathlib right now the general principle seems to be "do everything twice rather than attempting to deduce eg the theory of colimits from the theory of limits"

My current vision for this is that everything is stated twice, but all the necessary infrastructure should be provided to transfer proofs, and longer proofs should not be duplicated. A simple example where this works is file#CategoryTheory/Filtered/Final. I think that we're in a much much better position for this than a few years ago, but there is still a lot of work to do. For example, file#CategoryTheory/Limits/Preserves/Opposites will need to grow by a factor of six to cover all necessary cases, and I'm currently thinking about how to make this happen while staying sane. Still, I think that this is a worthwhile approach that will increase productivity and usability in the long run.

[Christian Merten]

Kevin Buzzard said:

I think that in the FLT work people just informally pass from the pro-objects in the category of finite-as-a-type rings with residue field Z/p to an appropriate category of complete local Z_p-algebras with residue field Z/p and continuous morphisms...

Is the index category in the "lifts of representations" example naturally small? And maybe more importantly, if the lifts functor lands in Type v, is the indexing category naturally in Type v?
(The reason I am asking this: In my example, fibre functors of Galois categories, this does not happen, if one does not assume that the Galois category in question is itself small. This does not cause issues (yet), but prevents me from using the current ind-object (better: pro-object) setup (which is not a problem at all, since I don't need any categorical properties of ind/pro objects).

[Kevin Buzzard]

The finite rings are all in Type and the pro-objects are limits over types of finite objects (eg the p-adic integers is a limit over n in Nat of Z/p^n) so they're also in Type. Does this answer your question or is there more to it?

[Christian Merten]

If by the "pro-objects are limits over types" you mean the "pro-objects are limits indexed over elements of Type" then this answers my question and it should fit in the current setup.

[Christian Merten]

Markus Himmel said:

One thing I've been wondering about is the characterization of hom-sets of pro-objects in terms of limits of colimits of hom-sets in C, see for example Lemma 2.6 on the nlab page on pro-objects. Kashiwara-Schapira only seem to need this to show that the pro-category is locally small. Is this characterization useful in applications? If so, it might be a good time to start thinking about how to make it ergonomic in Lean.

More generally, how do people work with morphisms of ind-objects and pro-objects in practice?

I have ever only used the pro-yoneda lemmas, the one with colim on the left and the one with colim on the right, to speak about morphisms of pro objects (identifying the pro-object with the functor it represents). I think, since nlab defines pro objects to be the full subcategory of pro-representable functors, the characterisation in lemma 2.6 should follow from these.

[Kyle Miller]

In topology, one way pro-objects show up is filters. If you take the open neighborhood filter in a space $X$ at a point $x$ (call it $F_x$) and you let $Y$ be a space standing for itself using the trivial filter, then $\hom(F_x,Y)$ of topological/smooth/etc. pro-manifolds is the same thing as the set of germs of functions $X\to Y$ centered at $x$, which you can see from the lim/colim characterization. This is a special situation though, since (at least for smooth manifolds) you can use extension theorems to get a surjective map $\hom(X,Y)\to\hom(F_x,Y)$ to represent every germ using some smooth map $X\to Y$.

For any open filters $F$ on $X$ and $G$ on $Y$, then the lim/colim characterization tells you how to make sense of $\hom(F,G)$. For every open neighborhood $V$ in $G$ there is an open neighborhood $U$ in $F$ and a morphism $U\to V$, and these all need to be compatible with respect to restrictions. (Interesting how that looks suspiciously like some sort of continuity condition when written this way.)

If you have a smooth map $X\to Y$ that sends a closed subspace $A$ to a closed subspace $B$, then you can "restrict" this be a smooth map "$A\to B$" in the pro-object sense, by replacing $A$ and $B$ with the filters of all open sets containing $A$ and $B$. Such a pro-morphism contains the map $A\to B$ itself, but it also contains the infinitesimal information about the map.

[Adam Topaz]

@Jack McKoen