# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: condensed abelian groups

#### 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 .

#### 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)

#### Reid Barton (Dec 08 2020 at 18:04):

More precisely, taking `Type 1`

-sized sheaves on tiny (:= `Type 0`

-sized) profinite sets

#### 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.

#### 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

#### Adam Topaz (Dec 08 2020 at 18:34):

My plan was to **define** profinite sets as `Pro(FinType)`

:rofl:

#### Adam Topaz (Dec 08 2020 at 18:34):

But I got stuck with the details, tbh.

#### Bhavik Mehta (Dec 08 2020 at 18:35):

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

#### Adam Topaz (Dec 08 2020 at 18:35):

Yes absolutely.

#### Bhavik Mehta (Dec 08 2020 at 18:36):

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

#### Adam Topaz (Dec 08 2020 at 18:36):

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

#### 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.

#### Adam Topaz (Dec 08 2020 at 18:38):

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

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

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

#### Adam Topaz (Dec 08 2020 at 18:39):

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

#### 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

#### 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.

#### 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

#### Adam Topaz (Dec 08 2020 at 19:02):

There's a nice skeleton for `FinType`

, already in mathlib :)

#### 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

#### 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
```

#### Bhavik Mehta (Dec 08 2020 at 19:27):

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

#### 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!

#### Calle Sönne (Dec 08 2020 at 21:16):

Looks great

#### 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.

#### Kevin Buzzard (Dec 08 2020 at 21:54):

Abelian categories are now in mathlib!

#### Kevin Buzzard (Dec 08 2020 at 21:55):

#### 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.

#### Adam Topaz (Dec 08 2020 at 22:37):

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

#### 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

#### 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

#### Bhavik Mehta (Dec 08 2020 at 23:29):

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

#### 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?

#### Bhavik Mehta (Dec 08 2020 at 23:34):

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

#### Adam Topaz (Dec 08 2020 at 23:35):

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

#### Bhavik Mehta (Dec 08 2020 at 23:35):

was just about to ask for that, thanks

#### 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

#### 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

#### Adam Topaz (Dec 08 2020 at 23:50):

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

#### Bhavik Mehta (Dec 08 2020 at 23:51):

I do :)

#### Bhavik Mehta (Dec 08 2020 at 23:51):

Coming soon to a mathlib near you

#### 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

#### 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

#### Bhavik Mehta (Dec 09 2020 at 00:10):

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

#### Reid Barton (Dec 09 2020 at 00:11):

It is the correct way to solve them in this context

#### 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

#### 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

#### Reid Barton (Dec 09 2020 at 00:37):

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

#### 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

#### 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

#### Reid Barton (Dec 09 2020 at 00:41):

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

#### 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

#### Reid Barton (Dec 09 2020 at 00:44):

If `C`

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

#### Reid Barton (Dec 09 2020 at 00:44):

let's see what LPAC does

#### 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

#### Bhavik Mehta (Dec 09 2020 at 00:53):

Do you know how difficult that proof is to formalise?

#### Reid Barton (Dec 09 2020 at 00:54):

it doesn't look especially hard

#### Reid Barton (Dec 09 2020 at 00:54):

Lemma 2.24

#### Adam Topaz (Dec 09 2020 at 00:55):

What's LPAC?

#### Reid Barton (Dec 09 2020 at 00:56):

Locally Presentable and Accessible Categories

#### Bhavik Mehta (Dec 09 2020 at 00:56):

Oh yeah that looks very manageable

#### Reid Barton (Dec 09 2020 at 00:57):

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

#### 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).

#### 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."

#### 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

#### 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

#### Adam Topaz (Dec 09 2020 at 17:43):

#### 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

#### 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

#### Peter Scholze (Feb 02 2021 at 16:02):

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

#### 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!

#### 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

#### 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