Zulip Chat Archive

Stream: condensed mathematics

Topic: condensed abelian groups


view this post on Zulip Kevin Buzzard (Dec 08 2020 at 18:01):

@Calle Sönne and @Kenny Lau and @Bhavik Mehta have been working on defining condensed sets. A natural goal here would be to prove that the category of condensed abelian groups is an abelian category with all the extra stuff too (e.g. arbitrary products). This is Theorem 1.10 of http://www.math.uni-bonn.de/people/scholze/Condensed.pdf .

view this post on Zulip Kevin Buzzard (Dec 08 2020 at 18:01):

Reid has suggested that we initially ignore the cardinal bounds; we can come back to them later (they are in some sense not the point of the challenge)

view this post on Zulip Reid Barton (Dec 08 2020 at 18:04):

More precisely, taking Type 1-sized sheaves on tiny (:= Type 0-sized) profinite sets

view this post on Zulip Kevin Buzzard (Dec 08 2020 at 18:07):

This will be a nice test of the abelian category machinery, so this has great value independent of the application to the challenge.

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 18:33):

@Adam Topaz's effort towards ind-objects seem relevant as well, if we need to show that the category Pro-Fintype is the same as Profinite

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:34):

My plan was to define profinite sets as Pro(FinType) :rofl:

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:34):

But I got stuck with the details, tbh.

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 18:35):

I think regardless of the definition, the equivalence between the two categories ought to be there

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:35):

Yes absolutely.

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 18:36):

Do you have a branch where you're working on this out of interest?

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:36):

I haven't started anything seriously, just playing around.

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:37):

For example, I tried making some crazy inductive-quotient style definition, which works out fine, except for universe problems.

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:38):

And I tried the "direct" way where you define hom sets as

limjcolimiHom(F(i),G(j))\operatorname{lim}_j \operatorname{colim}_i \operatorname{Hom}(F(i),G(j))

but even defining the identity morphisms seems to be a major pain...

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:39):

I'm still not sure what definition would be best here...

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 18:56):

import category_theory.limits.functor_category
import category_theory.full_subcategory
import category_theory.limits.types

namespace category_theory
namespace limits

universes v u
variables {C : Type u} [small_category C]

structure as_inductive (P : Cᵒᵖ  Type u) :=
(D : Type u)
[𝒟 : small_category D]
[hD : is_filtered D]
(α : D  C)
(i : P  colimit (α  (yoneda : C  Cᵒᵖ  Type u)))

structure is_inductive (P : Cᵒᵖ  Type u) : Prop :=
(mk' : nonempty (as_inductive P))

@[derive category]
def ind := {P : Cᵒᵖ  Type u // is_inductive P}

end limits
end category_theory

this works but I don't know if making C a small category is too restrictive

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:58):

Right, so this is the presentation of filtered colimits of representables in presheves. That's the right category.

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 19:01):

Yeah, but Fintype isn't a small category, so with this definition we don't get Ind(Fintype) \iso Type

view this post on Zulip Adam Topaz (Dec 08 2020 at 19:02):

There's a nice skeleton for FinType, already in mathlib :)

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 19:02):

Sure but I don't see any maths reason why Ind is only defined for small categories

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 19:03):

Ah this looks better:

import category_theory.limits.functor_category
import category_theory.full_subcategory
import category_theory.limits.types
import category_theory.Fintype

namespace category_theory
namespace limits

universes v u
variables {C : Type u} [category.{v} C]

structure as_inductive (P : Cᵒᵖ  Type v) :=
(D : Type*)
[𝒟 : small_category D]
[hD : is_filtered D]
(α : D  C)
(c : cocone (α  yoneda))
(hc : is_colimit c)
(i : P  c.X)

structure is_inductive (P : Cᵒᵖ  Type v) : Prop :=
(mk' : nonempty (as_inductive P))

variable (C)

@[derive category]
def ind := {P : Cᵒᵖ  Type v // is_inductive P}

def thing : ind Fintype.{u}  Type u :=
sorry

end limits
end category_theory

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 19:27):

some stuff building on that here: https://github.com/leanprover-community/mathlib/tree/ind-object

view this post on Zulip Calle Sönne (Dec 08 2020 at 21:16):

Kevin Buzzard said:

This will be a nice test of the abelian category machinery, so this has great value independent of the application to the challenge.

I didnt know this existed!

view this post on Zulip Calle Sönne (Dec 08 2020 at 21:16):

Looks great

view this post on Zulip Calle Sönne (Dec 08 2020 at 21:26):

So where have people been working on this? I have just been (slowly) trying to build upon @Kevin Buzzard s definition of Profinite sets on the branch Profinite2. So far I proved they have limits, so now I guess that the pretopology can be defined.

view this post on Zulip Kevin Buzzard (Dec 08 2020 at 21:54):

Abelian categories are now in mathlib!

view this post on Zulip Kevin Buzzard (Dec 08 2020 at 21:55):

docs#category_theory.abelian

view this post on Zulip Kevin Buzzard (Dec 08 2020 at 21:56):

The first goal is to show that the category of sheaves of abelian groups on Profinite is an abelian category.

view this post on Zulip Adam Topaz (Dec 08 2020 at 22:37):

It may be worthwhile to prove that this is true for abelian sheaves on any site.

view this post on Zulip Adam Topaz (Dec 08 2020 at 22:41):

But this requires sheafification, which I don't think we have yet in mathlib for a general grothendieck topology

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 23:28):

Adam Topaz said:

It may be worthwhile to prove that this is true for abelian sheaves on any site.

@Kevin Buzzard tells me this isn't true in general

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 23:29):

(unless I'm misunderstanding something which is more than likely)

view this post on Zulip Adam Topaz (Dec 08 2020 at 23:32):

Condensed abelian groups satisfy stronger axioms than just an abelian category that do not hold true in for general abelian sheaves. Maybe this is what he means?

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 23:34):

Probably, assume that I understood something wrong rather than that he said something wrong though :)

view this post on Zulip Adam Topaz (Dec 08 2020 at 23:35):

https://stacks.math.columbia.edu/tag/03CN

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 23:35):

was just about to ask for that, thanks

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 23:44):

Looking through that it seems like it splits up quite nicely: https://stacks.math.columbia.edu/tag/03A3 is just a statement on abelian categories, it requires that the category of abelian presheaves is abelian: https://stacks.math.columbia.edu/tag/03A6, and what's left then is that the abelian sheaves are a reflective subcategory where the reflector is left exact

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 23:44):

To get here of course we need to define abelian presheaves and sheaves, which I talked a bit about here: https://github.com/leanprover-community/mathlib/pull/5255#issuecomment-740065209

view this post on Zulip Adam Topaz (Dec 08 2020 at 23:50):

We also need the sheafification functor, but I'm sure you already have plans for that :)

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 23:51):

I do :)

view this post on Zulip Bhavik Mehta (Dec 08 2020 at 23:51):

Coming soon to a mathlib near you

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 00:07):

Is Profinite as in mathlib a small category? The results in stacks are stated only for small categories, as is the result I put in the link above

view this post on Zulip Reid Barton (Dec 09 2020 at 00:09):

It might be necessary to ulift the morphisms of Profinite to make it small in the next universe

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 00:10):

Do you think just doing that will solve the universe issues?

view this post on Zulip Reid Barton (Dec 09 2020 at 00:11):

It is the correct way to solve them in this context

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 00:12):

By the way do you have any suggestions for making the category of ind-objects? I had a go here: https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/condensed.20abelian.20groups/near/219247857 but it doesn't seem like the best way to me

view this post on Zulip Reid Barton (Dec 09 2020 at 00:37):

If I recall correctly, it's not that easy to prove that objects of this form are closed under filtered colimits

view this post on Zulip Reid Barton (Dec 09 2020 at 00:37):

which is the one property you'd hope would be obvious from this definition

view this post on Zulip Reid Barton (Dec 09 2020 at 00:39):

also the definition seems to indicate we lack a version of a colimit cocone indexed on the vertex

view this post on Zulip Reid Barton (Dec 09 2020 at 00:39):

I have a construction of the closure under a certain class of colimits somewhere, but I'm not sure it is very useful either

view this post on Zulip Reid Barton (Dec 09 2020 at 00:41):

oh but that was mostly to avoid enlarging the universe, which isn't an issue here

view this post on Zulip Reid Barton (Dec 09 2020 at 00:43):

Typically I'd assume that C is small and has finite colimits and take the full subcategory on the guys that send those to limits

view this post on Zulip Reid Barton (Dec 09 2020 at 00:44):

If C doesn't have finite colimits then I guess you can take flat functors?

view this post on Zulip Reid Barton (Dec 09 2020 at 00:44):

let's see what LPAC does

view this post on Zulip Reid Barton (Dec 09 2020 at 00:52):

it proves that being a filtered colimit of representables is equivalent to the corresponding colimit-preserving functor preserving finite limits

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 00:53):

Do you know how difficult that proof is to formalise?

view this post on Zulip Reid Barton (Dec 09 2020 at 00:54):

it doesn't look especially hard

view this post on Zulip Reid Barton (Dec 09 2020 at 00:54):

Lemma 2.24

view this post on Zulip Adam Topaz (Dec 09 2020 at 00:55):

What's LPAC?

view this post on Zulip Reid Barton (Dec 09 2020 at 00:56):

Locally Presentable and Accessible Categories

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 00:56):

Oh yeah that looks very manageable

view this post on Zulip Reid Barton (Dec 09 2020 at 00:57):

at least if you replace "directed" in the statement by "filtered"

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 01:00):

Bhavik Mehta said:

Probably, assume that I understood something wrong rather than that he said something wrong though :)

Apologies for the confusion -- this was a conversation we had on the discord and I'm pretty sure it was me who got it wrong -- I'd misremembered something. Arbitrary products are exact for condensed abelian groups (a product of epis is epi), and this is not true for sheaves of abelian groups on a general site, but all the axioms for an abelian category hold for sheaves of abelian groups on a general site (Bhavik I think I told you that arbitrary products might not exist in general).

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 01:02):

Yup, as you mentioned Scholze says something along these lines:
"This makes Cond(Ab) exceptionally well-behaved, even more well-behaved than the category of abelian sheaves on a usual topos: Usually, infinite products fail to be exact."

view this post on Zulip Reid Barton (Dec 09 2020 at 01:09):

Your thing is an interesting test case, I feel like it will probably be pretty hard to prove directly

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 01:21):

I'm not sure if it'll make that easier but I do suspect the definition would be nicer as saying the corresponding colimit-preserving functor preserving finite limits

view this post on Zulip Adam Topaz (Dec 09 2020 at 17:43):

@Calle Sönne https://github.com/leanprover-community/mathlib/blob/1f1ba587f272d203a40801c6b21af453f7de6ee3/src/topology/subset_properties.lean#L1305

view this post on Zulip Bhavik Mehta (Feb 02 2021 at 16:00):

Getting back to the ind-objects stuff, I've got a workable definition of flat functor on an arbitrary category (ie, not necessarily small and with no assumptions on limits/colimits), together with a proof that it's the same notion as preserving finite limits if they exist in the category, and almost got that the category of flat functors (ie ind-objects) is closed under filtered colimits (if the category is small), so I'm not far off from formally showing they're the ind-completion

view this post on Zulip Bhavik Mehta (Feb 02 2021 at 16:01):

The real tests here though are showing that ind Fintype = Type, and ind Fintype^op = Profinite^op

view this post on Zulip Peter Scholze (Feb 02 2021 at 16:02):

@Bhavik Mehta Those would be great to have, yes.

view this post on Zulip Bhavik Mehta (Feb 10 2021 at 16:40):

If anyone's interested in joining, I'm having a go at showing ind Fintype = Type in Kevin's discord!

view this post on Zulip Bhavik Mehta (Feb 18 2021 at 18:36):

Does anyone know if this result will explicitly be helpful? Specifically Calle has shown the topology version without an explicit equivalence of categories, is that good enough for the liquid project or is the actual category theory helpful too

view this post on Zulip Adam Topaz (Feb 18 2021 at 18:39):

I think the equivalence Pro (FinType) \equiv Profinite is actually useful because there are a lot of arguments that work with some functor on Profinite where you reduce to the finite case using this equivalence.


Last updated: May 09 2021 at 16:20 UTC