# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: cech_stuff

#### Adam Topaz (Mar 31 2021 at 21:32):

In case anyone wants to play with the cech nerve, I've pushed a (somewhat preliminary) definition here:

https://github.com/leanprover-community/lean-liquid/blob/cb3b771d3f4ceb22a0ea0c8b4e3556ad8540f5a8/src/for_mathlib/cech.lean#L60

(If you check out this branch, make sure to fetch oleans since it uses an updated version of mathlib)

#### Johan Commelin (Apr 01 2021 at 09:12):

Great, thanks for working on this.

#### Johan Commelin (Apr 01 2021 at 09:12):

I'll update mathlib on master now. So that it doesn't get too far out of sync.

#### Johan Commelin (Apr 01 2021 at 10:14):

bumped mathlib

#### Adam Topaz (Apr 01 2021 at 13:40):

I'll be keeping mathlib pretty fresh in this branch, at least for a little while, since I'm doing a lot of stuff with mathlib PRs.

#### Johan Commelin (Apr 01 2021 at 13:40):

Yes, I think it's great that you're PRing things straight to mathlib.

#### Johan Commelin (Apr 01 2021 at 13:41):

On the other hand, if you feel like things are more experimental, and they should be stress-tested before going to mathlib, then it might make sense to keep them in LTE for a while

#### Adam Topaz (Apr 06 2021 at 22:11):

Profinite sets will soon have limits #7070

Hopefully next week they will also be Pro(finite) sets.

#### Johan Commelin (Apr 07 2021 at 04:30):

That's great!

#### Adam Topaz (Apr 08 2021 at 15:21):

Quick update: profinite sets are limits of finite sets:

https://github.com/leanprover-community/lean-liquid/blob/be9b2c67610095d1a8d03f07459a2ea93e3fad4c/src/for_mathlib/Profinite_canon_limit.lean#L442

Proving that this presentation is actually functorial shouldn't be too hard using the lemma `map_refined_comm`

in the same file.

#### Adam Topaz (Apr 08 2021 at 17:57):

And now here's some form of functoriality:

https://github.com/leanprover-community/lean-liquid/blob/87c511dc50365f51916e1cb441c4cf8a929d4546/src/for_mathlib/Profinite_canon_limit.lean#L467

#### Adam Topaz (Apr 08 2021 at 23:12):

Alright, there is now a more-or-less complete API which provides functoriality of these limit presentations of profinite sets.

See `change_cone_id`

, `change_cone_comp`

, and `change_cone_lift`

in the file https://github.com/leanprover-community/lean-liquid/blob/cech_stuff/src/for_mathlib/Profinite_canon_limit.lean

#### Johan Commelin (Apr 09 2021 at 05:23):

Thanks a lot for doing this!

#### Adam Topaz (Apr 09 2021 at 13:40):

What I'd like to do next is write does the fact that any cover of a profinite set by a profinite set can be expressed as a limit of covers of finite sets by finite sets (I'll think about hypercovers later, as needed, although this might suffice if we really only need the cech complex).

I'm not sure about the best way to proceed. Any ideas?

My current thought is to use work in `arrow Profinite`

and try to write down some limit cone there. If

$f : \lim_{d \in D} X_d \to \lim_{e \in E} Y_e$

is a morphism of profinite sets which are written as limits of finite sets, I think the correct indexing category which exhibits the arrow as a limit is something like $D^{op} \times E$? But even writing down this diagram is not so easy since for every choice of $e \in E$ one has to refine the corresponding object of $d$ (and I guess this needs to be done in a functorial way).

#### Adam Topaz (Apr 09 2021 at 13:44):

Do we have the Grothendieck construction? (yes: :docs#category_theory.grothendieck )

#### Johan Commelin (Apr 09 2021 at 13:52):

@Adam Topaz Cool! Seems like you're now getting to the heart of things

#### Kevin Buzzard (Apr 09 2021 at 14:24):

There is a "canonical" collection of covers of finite sets by finite sets for which it's the limit, right? If $X\to Y$ then just take all the finite quotients of $X$ (this is some subset of the equivalence relations on $X$) and the finite quotients of $Y$ such that there's a map between the finite quotients making the diagram commute.

#### Adam Topaz (Apr 09 2021 at 14:29):

Yes, that works, but I was thinking of taking a finite quotient of Y, whose fibres are then a decomposition of Y into a finite union of clopen disjoint sets, pull those back to get a clopen disjoint cover of X, and consider all refinements of this pullback

#### Adam Topaz (Apr 09 2021 at 14:31):

So for every finite quotient of Y you get a cofinal system of the finite quotients of X, and this process of choosing the cofinal system is functorial. Applying something like a grothendieck construction then gives a "correct" diagram

#### Adam Topaz (Apr 11 2021 at 19:57):

Well, the case of arrows is now done here:

https://github.com/leanprover-community/lean-liquid/blob/94be0d767ba802ade4c6f99e6fa2e622da43219c/src/for_mathlib/Profinite_functorial_limit.lean#L785

But that turned out to be much harder than I originally thought!

I'm hoping the case of arrows is actually sufficient for what we need (I think it is, if we only need cech complexes).

In what level of generality is the category $J \Rightarrow Profinite$ equivalentt to $Pro(J \Rightarrow Finset)$?

The most general case I could find in the literature is where $J$ is "loopless". (I started on some sketchy code for the general case in `for_mathlib/scratch.lean`

and eventually got stuck, but I think something can be done in the general case. One issue for now is that `arrow C`

is not defined as a functor category in mathlib.)

#### Johan Commelin (Apr 12 2021 at 06:04):

In what generality would you want to apply it?

#### Adam Topaz (Apr 12 2021 at 12:44):

Well, for example, what conditions on an augmented simplicial profinite set ensure that it's a limit of an augmented simplicial finite set?

#### Peter Scholze (Apr 12 2021 at 12:45):

That should always be true, right? (I assume you mean the limit of a pro-(augmented simplicial finite set).)

#### Peter Scholze (Apr 12 2021 at 12:45):

Adding in "hypercover" both times should be a little more tricky

#### Adam Topaz (Apr 12 2021 at 12:52):

Yeah that's what I mean. There is certainly a functor from pro(aug-simpl-finset) to aug-simpl-profnite, but I don't immediately see why every object is in the image.

#### Adam Topaz (Apr 12 2021 at 12:52):

Do you know of a reference for this?

#### Peter Scholze (Apr 12 2021 at 13:01):

Every simplicial $X$ is the limit of the coskeletons of its skeletons; so one can reduce to the similar assertion for truncated simplicial $X$'s; then argue by induction, writing $n$-truncated $X$'s as $n-1$-truncated ones plus a latching map

#### Adam Topaz (Apr 12 2021 at 13:04):

Ah ok. Yes, so when the source category J is finite you get an equiv between pro(J -> Finset) and J -> Profinite.

#### Peter Scholze (Apr 12 2021 at 13:05):

Hmm, that's not right, is it? Or it depends on your definition of "finite category". Profinite sets with an automorphism don't have that property

#### Adam Topaz (Apr 12 2021 at 13:05):

Finite means finite objects and finite Homs.

#### Peter Scholze (Apr 12 2021 at 13:08):

OK

#### Peter Scholze (Apr 12 2021 at 13:09):

How does one prove the claim for general finite categories, actually?

#### Adam Topaz (Apr 12 2021 at 13:14):

Ah maybe one really does need the category to be loopless?

#### Peter Scholze (Apr 12 2021 at 13:14):

I'm not sure! For profinite sets with an action by a finite group, it is true, so I'm inclined to believe it's true for finite categories

#### Peter Scholze (Apr 12 2021 at 13:17):

I also just realized that my argument above, as written, applies only to semisimplicial objects

#### Adam Topaz (Apr 12 2021 at 13:33):

The idea I had in mind in the finite case is this (I think it works?): If $J$ is the finite category and $j \in J$, write $X_j$ for the associated profinite set. Now given a finite quotient $X_e \to S$, it can be refined (I think?) in some canonical way so that for every endomorphism of $e$, the associated endomorphism $X_e \to X_e$ descends to $S$. For every other object $e'$ with a morphism from $e$, endow $X_{e'}$ with the trivial finite quotient, and for every object $e''$ mapping to $e$ endow $X_{e''}$ with the quotient obtained by pulling back this $X_e \to S$. If everything works, then this endowed every object $X_j$ with a finite quotient $S_j$ which are all compatible w.r.t. the morphisms arising from the finite category $J$, and furthermore as the original $e$ and $S$ vary, this gives cofinal systems among all finite quotients of the $X_e$.

#### Adam Topaz (Apr 12 2021 at 13:34):

That's sketchy, but this is what works in the case of the finite catgory $\bullet \to \bullet$ which I used in the `arrow Profinite`

case.

#### Adam Topaz (Apr 12 2021 at 13:35):

(although that category is loopless, so it's easier as one does not have to go through the original step of refining $S$)

#### Adam Topaz (Apr 12 2021 at 13:40):

err.... actually that argument doesn't work.

#### Peter Scholze (Apr 12 2021 at 13:42):

Hmm yeah it seems to assume looplessness

#### Adam Topaz (Apr 12 2021 at 13:42):

The point is to take a functor $j \mapsto X_j$ and construct some functor $j \mapsto S_j$ of finite sets with a functorial quotient $X_j \to S_j$ in such a way so that the $S_j$ are cofinal among the finite quotients.

#### Adam Topaz (Apr 12 2021 at 13:43):

So the argument works for profinite sets with a finite group action. Is it true for profinite sets with a finite *monoid* action?

#### Peter Scholze (Apr 12 2021 at 13:44):

Ah; good question...

#### Peter Scholze (Apr 12 2021 at 13:44):

What's a good example of a finite monoid? {0,1} under multiplication?

#### Adam Topaz (Apr 12 2021 at 13:44):

Sure.

#### Johan Commelin (Apr 12 2021 at 13:45):

`{0,1,..,n}`

with saturating addition

#### Peter Scholze (Apr 12 2021 at 13:46):

In the first case, I guess that would be profinite sets with an idempotent endomorphism? I think that case is OK

#### Adam Topaz (Apr 12 2021 at 13:51):

In any case, this discussion makes me think that this is a complicated enough question that we should try to make the argument in question work with arrows as opposed to simplicial objects

#### Peter Scholze (Apr 12 2021 at 13:54):

I think so

#### Adam Topaz (Apr 12 2021 at 13:54):

How important is it to pass from arrows to the chech nerve then to the cech complex in 8.4?

#### Adam Topaz (Apr 12 2021 at 13:55):

(well, even though 8.4 in the blueprint is stated with hypercovers)

#### Peter Scholze (Apr 12 2021 at 13:56):

8.4=8.19 in Analytic.pdf?

#### Peter Scholze (Apr 12 2021 at 13:57):

OK yes

#### Adam Topaz (Apr 12 2021 at 13:57):

Yeah

#### Peter Scholze (Apr 12 2021 at 13:57):

You mean whether one really needs the intermediary of (co)simplicial objects?

#### Adam Topaz (Apr 12 2021 at 13:59):

right. If we have an arrow $f : X \to Y$ we can construct the Cech complex directly. So the second half of 8.19 in analytic could be stated as: For every cover $f : T \to S$ of profinite sets, the associated Cech complex $0 \to \widehat{M}(S) \to \widehat{M}(T) \to \cdots$ is exact and etc.

#### Peter Scholze (Apr 12 2021 at 14:00):

It's probably worth formalizing that first; I'm sure some glue will be necessary later anyways. But @Johan Commelin would know much better

#### Peter Scholze (Apr 12 2021 at 14:01):

Mathematically, it seems completely fine

#### Johan Commelin (Apr 12 2021 at 14:02):

Well, what's rolling out of the construction of the double complex is Lean-wise quite far from the construction of the Cech complex.

#### Johan Commelin (Apr 12 2021 at 14:02):

So I was expecting that in the end 8.19 would be stated in terms of some `is_Cech_nerve`

#### Johan Commelin (Apr 12 2021 at 14:02):

And if that is the case, I don't think it matters anymore how 8.19 is proven.

#### Adam Topaz (Apr 12 2021 at 14:02):

What I'm proposing is to make it in terms of some `is_Cech_complex`

#### Johan Commelin (Apr 12 2021 at 14:03):

Aha. What would the definition look like?

#### Adam Topaz (Apr 12 2021 at 14:03):

Good question :)

#### Johan Commelin (Apr 12 2021 at 14:03):

What do I need to check, to verify that some complex `is_Cech_complex`

?

#### Adam Topaz (Apr 12 2021 at 14:04):

Naively we could say: "There exists some cover such that this complex is isomorphic to the Cech complex associated to the cover."

#### Peter Scholze (Apr 12 2021 at 14:04):

But there's this implicit variable $\hat{M}$ anyways

#### Adam Topaz (Apr 12 2021 at 14:04):

Where "isomorphic" probably means something stronger e.g. the norms should be strictly equal

#### Peter Scholze (Apr 12 2021 at 14:05):

So I think this only really makes sense on the level of the simplicial profinite set

#### Peter Scholze (Apr 12 2021 at 14:06):

Otherwise you force yourself to compose any nice isomorphism you may have through evaluation at $\hat{M}$ and taking alternating face maps

#### Johan Commelin (Apr 12 2021 at 14:07):

Note that the columns in the double complex will not be norm-strict isomorphic to whatever rolls out of the Cech construction, because the `i`

th object has the norm rescaled by `(i+1)!`

or something like that.

#### Johan Commelin (Apr 12 2021 at 14:07):

So we'll also need some glue there.

#### Adam Topaz (Apr 12 2021 at 14:17):

On second thought it shouldn't be too much of an issue to work with the cech nerve itself. We could say this: If `is_cech_nerve f C`

(meaning that `C`

is **a** cech nerve of a cover $f : T \to S$), then the second part of 8.19 holds true, and the proof would go by expressing `f`

as a limit.

#### Peter Scholze (Apr 12 2021 at 14:18):

That sounds good

#### Peter Scholze (Apr 12 2021 at 14:18):

Aside: Earlier on, there was a question whether anything actually needs simplicial objects as opposed to semisimplicial objects (eg, hypercovers). Actually, I think everything I write in the lecture notes works for semisimplicial objects. I'm not actually sure now why most modern discussions of hypercovers use simplicial objects. What goes wrong with hypercovers as semisimplicial objects?

#### Adam Topaz (Apr 12 2021 at 14:22):

The definition of hypercover would have to be changed right? The coskeleton functors are consstructed termwise as some limit over some diagram that includes degeneracy maps

#### Peter Scholze (Apr 12 2021 at 14:23):

Hmm, my impression was that the coskeleta are compatible, but I would have to check

#### Peter Scholze (Apr 12 2021 at 14:23):

(ie removing degeneracies from the limit gives a cofinal map, giving the same limit)

#### Adam Topaz (Apr 12 2021 at 14:23):

Oh yeah that should be okay. The coskeleta are some right Kan extension anyway.

#### Adam Topaz (Apr 13 2021 at 01:41):

I pushed a few more things to the `cech_stuff`

branch:

- The equivalence bettween
`arrow C`

and functors from`with_terminal (discrete punit)`

to`C`

. - A
`cech`

construction which now goes from`arrow C`

to`simplicial.augmented C`

, and the forgetful functor the other way called`to_arrow`

. - The adjunction
`to_arrow ⊣ cech`

, which then gives compatibility of`cech`

with limits "for free" :)

If anyone wants to play with these constructions, they're in the `for_mathlib/cech.lean`

file in the `cech_stuff`

branch, and make sure to fetch oleans as this uses an updated mathlib.

#### Johan Commelin (Apr 13 2021 at 05:07):

@Adam Topaz this is starting to look good! I'm still very busy with the homotopy stuff, and I need to do admin because semester is starting again.

#### Johan Commelin (Apr 13 2021 at 05:08):

I really want to finish the homotopy part before spending too much time on other parts of the project, and it looks like you're still full steam ahead.

#### Johan Commelin (Apr 13 2021 at 05:09):

But if there are specific struggles, please do tell me.

#### Adam Topaz (Apr 13 2021 at 15:46):

Does the following link work for anybody?

https://github.com/leanprover-community/lean-liquid/blob/cech_stuff/src/for_mathlib/Profinite_functorial_limit.lean

#### Adam Topaz (Apr 13 2021 at 15:46):

I'm getting a 500 error

#### Bhavik Mehta (Apr 13 2021 at 15:47):

Adam Topaz said:

- The equivalence bettween
`arrow C`

and functors from`with_terminal (discrete punit)`

to`C`

.

`with_terminal (discrete punit)`

is the same as `fin 2`

and `with_initial (discrete punit)`

right? Perhaps we should make a canonical name for talking about this category, or show that these three are all the same thing

#### Bryan Gin-ge Chen (Apr 13 2021 at 15:47):

Adam Topaz said:

I'm getting a 500 error

I'm getting one too. Even clicking on the link to Profinite_functorial.limit from the directory fails. Very strange!

#### Adam Topaz (Apr 13 2021 at 15:50):

@Bhavik Mehta I was actually discussing something similar with @Jakob Scholbach recently. Yes this is a good idea!

#### Adam Topaz (Apr 13 2021 at 15:50):

I mostly used `with_terminal (discrete punit)`

because I wanted to get the functor to `with_terminal simplicial_category`

for "free" by using `with_terminal.map`

#### Bhavik Mehta (Apr 13 2021 at 15:51):

Right, I think they each have their place to get universal properties nicely

#### Adam Topaz (Apr 13 2021 at 15:51):

Re the 500 error -- I just checked, and the file actually exists if you clone the repo.

#### Adam Topaz (Apr 13 2021 at 15:53):

In general I would also like to have the equivalence between `with_terminal J \func C`

and the some comma category involving constant functors from J.

#### Adam Topaz (Apr 13 2021 at 15:53):

(and the analogous thing for `with_initial`

as well)

#### Bhavik Mehta (Apr 13 2021 at 15:56):

Now that you mention it, this feels a lot like the ideas in https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/limits/constructions/over/products.lean, where `wide_pullback_shape J`

is essentially `with_terminal (discrete J)`

, and the existence of limits of shape `wide_pullback_shape J`

in `C`

is used to show the existence of limits of shape `discrete J`

in `C/X`

#### Bhavik Mehta (Apr 13 2021 at 15:57):

In fact I feel like your results on `with_terminal`

could be used to simplify some of the things about `wide_pullback_shape`

#### Adam Topaz (Apr 15 2021 at 13:36):

What's the status of Proposition 8.3 from the blueprint?

#### Adam Topaz (Apr 15 2021 at 13:36):

Has anything been done toward this?

#### Kevin Buzzard (Apr 15 2021 at 14:01):

I looked through a lot of the project recently and I don't recall seeing this, but I would wait to hear from Johan. Of course we don't really have anything at all on condensed anything, not even a definition.

#### Peter Scholze (Apr 15 2021 at 14:03):

8.3 itself would have a well-defined meaning, though: We basically defined $\hat{V}$ only as a functor from profinite sets $S$, but not via what it should actually be, namely continuous functions to $\hat{V}$ (rather, we took the completion of locally constant functions to $V$)

#### Adam Topaz (Apr 15 2021 at 14:04):

I'm not looking for anything condensed, but note that `LCC.obj M`

is a contravariant functor on `Profinite`

. That's the main thing I'm looking for -- a description of `LCC.obj M`

, as a functor on `Profinite\op`

, in terms of the completion of `M`

as a topological group

#### Adam Topaz (Apr 15 2021 at 14:06):

It seems to me that this would be the easiest way to show that $\widehat{M}(\lim_i S_i)$ is the colimit of $\widehat{M}(S_i)$?

#### Peter Scholze (Apr 15 2021 at 14:06):

Wait, that's not true, right?

#### Peter Scholze (Apr 15 2021 at 14:06):

The colimit would be the locally constant functions to $\hat{M}$

#### Adam Topaz (Apr 15 2021 at 14:08):

Oh yeah that's right. So now I'm confused about the proof of 8.4

#### Adam Topaz (Apr 15 2021 at 14:08):

Oh sorry I'm missing a completion

#### Adam Topaz (Apr 15 2021 at 14:09):

should be the completion of the colimit

#### Johan Commelin (Apr 15 2021 at 14:19):

Do we need 8.3?

#### Johan Commelin (Apr 15 2021 at 14:19):

It's not mentioned in the proof of 8.4.

#### Adam Topaz (Apr 15 2021 at 14:19):

Well, that's what I'm thinking -- we want to express the complex as a (completed) colimit of complexes associated to the finite quotients

#### Adam Topaz (Apr 15 2021 at 17:16):

I'm starting a small refactor of @Johan Commelin 's work on the alternating face map construction in the `augmented_stuff`

branch

#### Johan Commelin (Apr 15 2021 at 17:27):

Sounds good. I hope it doesn't cause to much pain to adapt the one or two places where I've used it.

#### Adam Topaz (Apr 15 2021 at 17:29):

So far it's going fine :)

#### Adam Topaz (Apr 15 2021 at 17:29):

I haven't gotten anywhere beyond where it's defined though

#### Adam Topaz (Apr 24 2021 at 16:25):

I ended up getting really bogged down with the Kan extension approach to the Cech nerve, so I redefined `cech`

in terms of wide pullbacks in the following file:

https://github.com/leanprover-community/lean-liquid/blob/cech_stuff/src/for_mathlib/cech2.lean

The part in the `category_theory.limits`

namespace is some additional API for wide pullbacks, and would be an easy mathlib PR if someone wants to take this on (it would be best to add analogues for `wide_pushworward`

as well as part of a mathlib PR)

#### Bhavik Mehta (Apr 24 2021 at 16:35):

Adam Topaz said:

I ended up getting really bogged down with the Kan extension approach to the Cech nerve, so I redefined

`cech`

in terms of wide pullbacks in the following file:

https://github.com/leanprover-community/lean-liquid/blob/cech_stuff/src/for_mathlib/cech2.lean

The part in the`category_theory.limits`

namespace is some additional API for wide pullbacks, and would be an easy mathlib PR if someone wants to take this on (it would be best to add analogues for`wide_pushworward`

as well as part of a mathlib PR)

(minor nit: `wide_pushout`

rather than `wide_pushforward`

)

#### Adam Topaz (Apr 24 2021 at 16:36):

(edited)

Last updated: May 09 2021 at 15:11 UTC