cech_stuff

Stream: condensed mathematics

[Adam Topaz]

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]

Great, thanks for working on this.

[Johan Commelin]

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

[Johan Commelin]

bumped mathlib

[Adam Topaz]

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]

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

[Johan Commelin]

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]

Profinite sets will soon have limits #7070
Hopefully next week they will also be Pro(finite) sets.

[Johan Commelin]

That's great!

[Adam Topaz]

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]

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]

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]

Thanks a lot for doing this!

[Adam Topaz]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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]

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]

In what generality would you want to apply it?

[Adam Topaz]

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]

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

[Peter Scholze]

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

[Adam Topaz]

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]

Do you know of a reference for this?

[Peter Scholze]

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]

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

[Peter Scholze]

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]

Finite means finite objects and finite Homs.

[Peter Scholze]

OK

[Peter Scholze]

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

[Adam Topaz]

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

[Peter Scholze]

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]

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

[Adam Topaz]

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]

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]

(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]

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

[Peter Scholze]

Hmm yeah it seems to assume looplessness

[Adam Topaz]

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]

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]

Ah; good question...

[Peter Scholze]

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

[Adam Topaz]

Sure.

[Johan Commelin]

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

[Peter Scholze]

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

[Adam Topaz]

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]

I think so

[Adam Topaz]

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

[Adam Topaz]

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

[Peter Scholze]

8.4=8.19 in Analytic.pdf?

[Peter Scholze]

OK yes

[Adam Topaz]

Yeah

[Peter Scholze]

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

[Adam Topaz]

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]

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]

Mathematically, it seems completely fine

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

Aha. What would the definition look like?

[Adam Topaz]

Good question :)

[Johan Commelin]

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

[Adam Topaz]

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

[Peter Scholze]

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

[Adam Topaz]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Johan Commelin]

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.

[Johan Commelin]

So we'll also need some glue there.

[Adam Topaz]

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]

That sounds good

[Peter Scholze]

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]

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]

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

[Peter Scholze]

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

[Adam Topaz]

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

[Adam Topaz]

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.

[Johan Commelin]

@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]

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]

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

[Adam Topaz]

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]

I'm getting a 500 error

[Bhavik Mehta]

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

[Bryan Gin-ge Chen]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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]

(and the analogous thing for with_initial as well)

[Bhavik Mehta]

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]

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]

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

[Adam Topaz]

Has anything been done toward this?

[Kevin Buzzard]

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]

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]

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]

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]

Wait, that's not true, right?

[Peter Scholze]

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

[Adam Topaz]

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

[Adam Topaz]

Oh sorry I'm missing a completion

[Adam Topaz]

should be the completion of the colimit

[Johan Commelin]

Do we need 8.3?

[Johan Commelin]

It's not mentioned in the proof of 8.4.

[Adam Topaz]

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]

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

[Johan Commelin]

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]

So far it's going fine :)

[Adam Topaz]

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

[Adam Topaz]

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]

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]

(edited)

[Johan Commelin]

Cech nerves are in mathlib! :octopus:

[Sebastien Gouezel]

I don't know what Cech nerves are. Do they have anything to do with Cech cohomology?

[Sebastien Gouezel]

(I'd love to have Cech cohomology in mathlib :-)

[Sebastien Gouezel]

(Because I'd love to have Alexander duality in its general form, and deduce Jordan theorem like a breeze).

[Johan Commelin]

@Sebastien Gouezel yes there's a very strong connection!

[Kevin Buzzard]

It's the combinatorics behind Cech cohomology

[Johan Commelin]

If you have an open cover $X = \bigcup_i U_i$ then also of course get a surjection $\bigsqcup_i U_i \to X$. The Cech nerve of that surjection is isomorphic to the simplicial object that is usually just constructed by hand from the intersections of the $U_i$.

[Johan Commelin]

Once you have the simplicial object, you can build the cohomology for the alternating face map complex.

[Sebastien Gouezel]

ok, it's a categorical way of expressing stuff I know how to do by hand.

[Johan Commelin]

So, I think we are very close to defining cohomology wrt a single cover.

[Johan Commelin]

And then there is of course this limiting procedure. That can probably be defined easily, but we might want to have some API around it to work with it nicely.

[Kevin Buzzard]

Modulo the fact that there has been no cohomology theory ever defined in lean for which we can prove a long exact sequence

[Johan Commelin]

I would say that the definitions of all three are well within reach now:

• singular cohomology
• Cech cohomology
• sheaf cohomology

[Johan Commelin]

Time for a bunch of comparison isos!

[Kevin Buzzard]

However there are recent grounds for optimism here

[Johan Commelin]

Sebastien Gouezel said:

(Because I'd love to have Alexander duality in its general form, and deduce Jordan theorem like a breeze).

This sounds really great!

[Sebastien Gouezel]

Alexander duality tells you that, if you have two homeomorphic subsets X and Y of $\R^n$, then the cohomologies of their complements are the same (as they can be read off the cohomology of X, resp. Y). So, the complement of anything homeomorphic to the sphere has two connected components, just like for the sphere, which is Jordan's theorem. This is really a crazy theorem (just look at what it says for two circles in the plane: they can be either one inside the other, or separated, but still there are always three connected components in the complement, and two holes).

[Sebastien Gouezel]

(Well, not so crazy once you think of it, but still amazing :-)

[Peter Scholze]

I've always thought of the part that's hidden here as the more delicate part: That any open subset of $\mathbb R^n$ decomposes as a disjoint union of path-connected open and closed subspaces. (This seems "obvious" from our mental picture of a smooth manifold, but I think the nasty part of the proof of Jordan's theorem is hidden here.)