Condensed R-modules

Stream: condensed mathematics

[Johan Commelin]

We'll need to work with Ext-groups in the category of condensed ℤ[T⁻¹]-modules. So if we start attacking the sorries that show that Condensed Ab is an abelian category with enough projectives, we should try to do it in the generality that also covers this case.

[Adam Topaz]

with the way our universes are set up right now, does Condensed Ab have enough projectives?

[Johan Commelin]

Maybe not. We really need to sort out those universes. I'll try to think about this as soon as I have gotten other urgent tasks off my todolist.

[Adam Topaz]

The universe parameters are Condensed Ab.{u+1} : Type (u+2) and it has a category.{u+1} instance. If I understand the argument from condensed.pdf correctly, we would have to take a direct sum of projectives indexed by J : Type (u+2) to obtain a projective presentation of some random object X : Condensed Ab.{u+1}.

[Kevin Buzzard]

I've not been following because I'm in teaching hell for the next three and a bit weeks. Is the issue that we actually need to do all this careful colimits over certain large(ish) cardinals nonsense or is it something else?

[Adam Topaz]

The way we have (co)limits set up is that when C : Type u is a category.{v} C, we can speak about (co)limits of functors J to C where J : Type v is a small category.

In this case, we have Condensed Ab.{u+1} : Type (u+2) is a category.{u+1}, which means we can a priori only take colimits along diagrams indexed by small categories J : Type (u+1). So if we need to take a direct sum indexed by J : Type (u+2), then we're out of luck.

The good news is that the objects we're reallly interested in turn out to be sheaves whose associated presheaf is essentially a functor from Profinite.{u} to Ab.{u}, but needs to be promoted via some ulift-like constructions to an object in Condensed Ab.{u+1}, so the direct sums we need to take to show that these particilar objects have a projective resolution are sufficiently small.

[Adam Topaz]

Of course, I could just be misunderstanding the general argument, and it's possible we don't need to take a large direct sum to show that Condensed Ab.{u+1} has enough projectives

[Peter Scholze]

My math understanding is that Condensed Ab.{u+1} ought to be functors from Profinite.{u}to Ab.{u+1}, and then the index set J that appears will be, for a presheaf $F$, the disjoint union over all isomorphism classes of objects $S$ of Profinite.{u} of $F(S)$. Now in ZFC universes, this disjoint union still lies in the u+1 universe.

But what you say above indicates that this is also true, as long as the index set of $S$'s is still in universe u. Well, it isn't quite -- it's a bit larger, but still much smaller than u+1 in terms of ZFC universes.

So maybe that it helps to take instead functors from Profinite.{u} to Ab.{u+2}? Then I'm pretty sure Profinite.{u} lies in Type.{u+1}, so that disjoint union of $F(S)$'s above should lie in Type.{u+2}, and this should be good enough.

[Johan Commelin]

Hmm, that could an interesting "hack" to solve it. (-;

[Adam Topaz]

I don't know why I thought the index set would be in u+2 (I think I had in mind to quantify over subobjects or something), but this indeed works:

import topology.category.Profinite
import algebra.category.Group

universe u
variable (F : Profinite.{u}ᵒᵖ ⥤ Ab.{u+1})

#check Σ (S : Profinite.{u}), F.obj (opposite.op S)
--Σ (S : Profinite), ↥(F.obj (opposite.op S)) : Type (u+1)

Sorry for the noise. We will have enough projectives :)