Zulip Chat Archive

Stream: condensed mathematics

Topic: cech_stuff


view this post on Zulip 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)

view this post on Zulip Johan Commelin (Apr 01 2021 at 09:12):

Great, thanks for working on this.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 01 2021 at 10:14):

bumped mathlib

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 01 2021 at 13:40):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 07 2021 at 04:30):

That's great!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 09 2021 at 05:23):

Thanks a lot for doing this!

view this post on Zulip 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:limdDXdlimeEYef : \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 Dop×ED^{op} \times E? But even writing down this diagram is not so easy since for every choice of eEe \in E one has to refine the corresponding object of dd (and I guess this needs to be done in a functorial way).

view this post on Zulip Adam Topaz (Apr 09 2021 at 13:44):

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

view this post on Zulip Johan Commelin (Apr 09 2021 at 13:52):

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

view this post on Zulip 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 XYX\to Y then just take all the finite quotients of XX (this is some subset of the equivalence relations on XX) and the finite quotients of YY such that there's a map between the finite quotients making the diagram commute.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 JProfiniteJ \Rightarrow Profinite equivalentt to Pro(JFinset)Pro(J \Rightarrow Finset)?
The most general case I could find in the literature is where JJ 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.)

view this post on Zulip Johan Commelin (Apr 12 2021 at 06:04):

In what generality would you want to apply it?

view this post on Zulip 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?

view this post on Zulip 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).)

view this post on Zulip Peter Scholze (Apr 12 2021 at 12:45):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Apr 12 2021 at 12:52):

Do you know of a reference for this?

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:01):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Apr 12 2021 at 13:05):

Finite means finite objects and finite Homs.

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:08):

OK

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:09):

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

view this post on Zulip Adam Topaz (Apr 12 2021 at 13:14):

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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:17):

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

view this post on Zulip 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 JJ is the finite category and jJj \in J, write XjX_j for the associated profinite set. Now given a finite quotient XeSX_e \to S, it can be refined (I think?) in some canonical way so that for every endomorphism of ee, the associated endomorphism XeXeX_e \to X_e descends to SS. For every other object ee' with a morphism from ee, endow XeX_{e'} with the trivial finite quotient, and for every object ee'' mapping to ee endow XeX_{e''} with the quotient obtained by pulling back this XeSX_e \to S. If everything works, then this endowed every object XjX_j with a finite quotient SjS_j which are all compatible w.r.t. the morphisms arising from the finite category JJ, and furthermore as the original ee and SS vary, this gives cofinal systems among all finite quotients of the XeX_e.

view this post on Zulip 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.

view this post on Zulip 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 SS)

view this post on Zulip Adam Topaz (Apr 12 2021 at 13:40):

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

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:42):

Hmm yeah it seems to assume looplessness

view this post on Zulip Adam Topaz (Apr 12 2021 at 13:42):

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

view this post on Zulip 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?

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:44):

Ah; good question...

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:44):

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

view this post on Zulip Adam Topaz (Apr 12 2021 at 13:44):

Sure.

view this post on Zulip Johan Commelin (Apr 12 2021 at 13:45):

{0,1,..,n} with saturating addition

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:54):

I think so

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Apr 12 2021 at 13:55):

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

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:56):

8.4=8.19 in Analytic.pdf?

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:57):

OK yes

view this post on Zulip Adam Topaz (Apr 12 2021 at 13:57):

Yeah

view this post on Zulip Peter Scholze (Apr 12 2021 at 13:57):

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

view this post on Zulip Adam Topaz (Apr 12 2021 at 13:59):

right. If we have an arrow f:XYf : 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:TSf : T \to S of profinite sets, the associated Cech complex 0M^(S)M^(T)0 \to \widehat{M}(S) \to \widehat{M}(T) \to \cdots is exact and etc.

view this post on Zulip 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

view this post on Zulip Peter Scholze (Apr 12 2021 at 14:01):

Mathematically, it seems completely fine

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Apr 12 2021 at 14:02):

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

view this post on Zulip Johan Commelin (Apr 12 2021 at 14:03):

Aha. What would the definition look like?

view this post on Zulip Adam Topaz (Apr 12 2021 at 14:03):

Good question :)

view this post on Zulip Johan Commelin (Apr 12 2021 at 14:03):

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

view this post on Zulip 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."

view this post on Zulip Peter Scholze (Apr 12 2021 at 14:04):

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

view this post on Zulip Adam Topaz (Apr 12 2021 at 14:04):

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

view this post on Zulip Peter Scholze (Apr 12 2021 at 14:05):

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

view this post on Zulip Peter Scholze (Apr 12 2021 at 14:06):

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

view this post on Zulip 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 ith object has the norm rescaled by (i+1)! or something like that.

view this post on Zulip Johan Commelin (Apr 12 2021 at 14:07):

So we'll also need some glue there.

view this post on Zulip 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:TSf : T \to S), then the second part of 8.19 holds true, and the proof would go by expressing f as a limit.

view this post on Zulip Peter Scholze (Apr 12 2021 at 14:18):

That sounds good

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Peter Scholze (Apr 12 2021 at 14:23):

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

view this post on Zulip Peter Scholze (Apr 12 2021 at 14:23):

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

view this post on Zulip Adam Topaz (Apr 12 2021 at 14:23):

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

view this post on Zulip Adam Topaz (Apr 13 2021 at 01:41):

I pushed a few more things to the cech_stuff branch:

  1. The equivalence bettween arrow C and functors from with_terminal (discrete punit) to C.
  2. A cech construction which now goes from arrow C to simplicial.augmented C, and the forgetful functor the other way called to_arrow.
  3. 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 13 2021 at 05:09):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Apr 13 2021 at 15:46):

I'm getting a 500 error

view this post on Zulip Bhavik Mehta (Apr 13 2021 at 15:47):

Adam Topaz said:

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

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Apr 13 2021 at 15:51):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Apr 13 2021 at 15:53):

(and the analogous thing for with_initial as well)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Apr 15 2021 at 13:36):

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

view this post on Zulip Adam Topaz (Apr 15 2021 at 13:36):

Has anything been done toward this?

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Apr 15 2021 at 14:03):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Apr 15 2021 at 14:06):

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

view this post on Zulip Peter Scholze (Apr 15 2021 at 14:06):

Wait, that's not true, right?

view this post on Zulip Peter Scholze (Apr 15 2021 at 14:06):

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

view this post on Zulip Adam Topaz (Apr 15 2021 at 14:08):

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

view this post on Zulip Adam Topaz (Apr 15 2021 at 14:08):

Oh sorry I'm missing a completion

view this post on Zulip Adam Topaz (Apr 15 2021 at 14:09):

should be the completion of the colimit

view this post on Zulip Johan Commelin (Apr 15 2021 at 14:19):

Do we need 8.3?

view this post on Zulip Johan Commelin (Apr 15 2021 at 14:19):

It's not mentioned in the proof of 8.4.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Apr 15 2021 at 17:29):

So far it's going fine :)

view this post on Zulip Adam Topaz (Apr 15 2021 at 17:29):

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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Apr 24 2021 at 16:36):

(edited)


Last updated: May 09 2021 at 15:11 UTC