Zulip Chat Archive

Stream: condensed mathematics

Topic: Mbar functor

Johan Commelin (Jul 22 2021 at 06:37):

We have currently proven a mix of thm 9.4 and 9.5. To get the actual 9.4, we need to prove it for profinite sets S. So far, we only have it for finite sets S.

What do we need to do:

Make Mbar_le into a functor on finite sets.
For $S = \lim_i S_i$ $S = lim_{i} S_{i}$ a profinite set, define Mbar_le.profinite: $\overline{\mathcal M}_{r'}(S)_{\le c} = \lim_i \overline{\mathcal M}_{r'}(S_i)_{\le c}$ $\overline{M}_{r^{'}} (S)_{\leq c} = lim_{i} \overline{M}_{r^{'}} (S_{i})_{\leq c}$ . This should be a functor on profinite sets. Feel free to improve the name.
- Add instances, so that $\overline{\mathcal M}_{r'}(S)_{\le c}$ is a profinite set.
Define Mbar.profinite: $\overline{\mathcal M}_{r'}(S) = \bigcup_{c \ge 0} \overline{\mathcal M}_{r'}(S)_{\le c}$ $\overline{M}_{r^{'}} (S) = ⋃_{c \geq 0} \overline{M}_{r^{'}} (S)_{\leq c}$ . This should be a functor on profinite sets. Feel free to improve the name.
- Add instances, so that $\overline{\mathcal M}_{r'}(S)$ is a profinitely_filtered_pseudo_normed_group_with_Tinv.
State thm 9.4 for profinite S, and prove it. *

Johan Commelin (Jul 22 2021 at 06:37):

All of this can be done without needing the definition of a condensed set.

Johan Commelin (Jul 22 2021 at 07:38):

Johan Commelin said:

Make Mbar_le into a functor on finite sets.

It might be best to not touch the current definition, and instead define Mbar_le.functor as functor from FinType to Profinite. Evaluating it on a finite set can then be defeq to Mbar_le.

Adam Topaz (Jul 22 2021 at 15:34):

I've started on functorializing(?) Mbar.

Adam Topaz (Jul 22 2021 at 15:36):

I assume the following is correct (for Mbar, I'll work on Mbar_le next)?

/-- Given an element of `Mbar r' S` and a function `f : S → T`, this
  constructs an associated element of `Mbar r' T`. -/
def map : Mbar r' S → Mbar r' T := λ F,
{ to_fun := λ t n, ∑ s in finset.univ.filter (λ s', f s' = t), F s n,
  coeff_zero' := λ s, by simp,
  summable' := λ t, begin
     ...
  end }

Johan Commelin (Jul 22 2021 at 15:44):

In the end, the functor Mbar on profinite sets will be defined in terms of the functor Mbar_le on profinite sets (see the sketch above).
So I think it isn't necessary to turn Mbar (as we have it right now) into a functor on finite sets.

Johan Commelin (Jul 22 2021 at 15:44):

We will need an iso between [fintype S], (Mbar_functor r').obj S and Mbar r' S

Adam Topaz (Jul 22 2021 at 15:44):

I understand, but Mbar_le is defined as a subset of Mbar.

Johan Commelin (Jul 22 2021 at 15:45):

Fair enough.

Adam Topaz (Jul 22 2021 at 15:45):

So now that this Mbar.map is defined, we just need to show that it's compatible with the filtration.

Adam Topaz (Jul 22 2021 at 16:18):

Do we not have a topology on Mbar so that the Mbar_les are subspaces?

Adam Topaz (Jul 22 2021 at 16:18):

I remember we discussed this a while back, but I don't remember what the conclusion was :)

Johan Commelin (Jul 22 2021 at 16:24):

You run into defeq issues.

Johan Commelin (Jul 22 2021 at 16:24):

Because Mbar_le naturally gets a profinite topology. You can put the colimit topology on Mbar. But then the subspace topology on Mbar_le will only be propeq, not defeq to the topology you started with.

Adam Topaz (Jul 22 2021 at 16:26):

Man... formalizing is hard.

Adam Topaz (Jul 22 2021 at 17:26):

https://github.com/leanprover-community/lean-liquid/blob/ee3d614135c82452cd37f72383ac152b2962668a/src/Mbar/Mbar_le.lean#L497

Adam Topaz (Jul 22 2021 at 17:27):

I guess to extend this to a functor on Profinite we can take a right Kan extension, but do we actually want to do that?

Johan Commelin (Jul 22 2021 at 17:41):

I'm always feeling uneasy with Kan extensions :see_no_evil:
But if it is a Kan extension, then probably that is the best way to do it.

Adam Topaz (Jul 22 2021 at 17:45):

By the way, is there a better way to write things like ∑ s in finset.univ.filter (λ s', f s' = t), F s n?

Johan Commelin (Jul 22 2021 at 18:04):

I've also wished for a better way, but I don't think we have it yet.

Kevin Buzzard (Jul 22 2021 at 22:48):

We don't have preimage (f : X -> Y) (y : Y) : set X?

Adam Topaz (Jul 22 2021 at 22:50):

It would have to be a finset in this case, not a set

Yakov Pechersky (Jul 22 2021 at 22:53):

Why wouldn't (sum s : {t}.preimage f) work, since you have a fintype?

Yakov Pechersky (Jul 22 2021 at 22:53):

The coe sort would also be a fintype.

Adam Topaz (Jul 22 2021 at 23:09):

I'm confused. What is sum?

Yakov Pechersky (Jul 22 2021 at 23:11):

I don't have a unicode keyboard at the moment. I mean \sum, the sum sigma.

Yakov Pechersky (Jul 22 2021 at 23:11):

You'd have a sum over a coesort, and you'd have a coerced s in F s n, but they would mean the same values.

Adam Topaz (Jul 22 2021 at 23:31):

I still don't understand what sum s : {t}.preimage f is supposed to mean... This seems like it's saying that the sum of s is a term of {t}.preimage f. But what I want to do is to take a sum where the index varies over {t}.preimage f.

Adam Topaz (Jul 22 2021 at 23:35):

And sure, I can take a sum over the type associated to the preimage, but I feel like this will cause more pain when compared with a slightly less than optimal notation

Yakov Pechersky (Jul 22 2021 at 23:39):

Instead of "sigma s in filter ... ", say "sigma s : coerced ..." and rely on fintype sums. I understand the hesitancy about pain.

Adam Topaz (Jul 22 2021 at 23:40):

Ah I see what you mean now. But yes, I'm afraid the pain will be worse with this, since I rely on things like docs#finset.sum_bUnion (in the reverse direction) for a few of the proofs involved

Yakov Pechersky (Jul 22 2021 at 23:40):

What I was saying is that "take a sum where the index varies over {t}.preimage f." is precisely ∑ s : {t}.preimage f, F s n

Yakov Pechersky (Jul 22 2021 at 23:42):

Right, there are a lot of slightly incompatible forms. And it gets worse because rw isn't strong enough to rewrite around them unless you match the syntax precisely.

Adam Topaz (Jul 22 2021 at 23:43):

What I really want is notation ∑ a in S where p a, f a to mean ∑ a in S.filter p, f a.

Yakov Pechersky (Jul 22 2021 at 23:49):

How would you do it in the finset.univ case?

Adam Topaz (Jul 22 2021 at 23:51):

Without the in S, but with the where p a

Johan Commelin (Jul 23 2021 at 01:25):

I guess finsum might be useful as well. But I haven't yet tried using it in places like this.

Johan Commelin (Jul 23 2021 at 01:29):

Adding notation for the S.filter p step would make things more readable, which is good. But then we would still need a bunch of API lemmas, to make it usable.

Adam Topaz (Jul 23 2021 at 17:41):

I just pushed the extension of the functor from Fintype to Profinite here:
https://github.com/leanprover-community/lean-liquid/blob/284acf5fe6b2f78cecce80715b003226aff00dd7/src/Mbar/Mbar_le.lean#L515

(and a general version here https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/Profinite/extend.lean )

Adam Topaz (Jul 23 2021 at 17:42):

I used the presentation of a profinite set as a limit of its discrete quotients for this, but at some point we should probably relate this to the Kan extension.

Johan Commelin (Jul 24 2021 at 07:34):

@Adam Topaz Thanks!

Adam Topaz (Jul 24 2021 at 16:38):

Concerning Mbar.profinite... how should we define this? You wrote a union above, which is presumably a colimit, so a priori should involve some sheafification if we want a condensed object.

Peter Scholze (Jul 24 2021 at 21:34):

filtered colimits need not be sheafified in condensed sets!

Adam Topaz (Jul 24 2021 at 21:38):

Great!

Adam Topaz (Jul 26 2021 at 16:29):

I've defined a thing called Mbar.profinite here
https://github.com/leanprover-community/lean-liquid/blob/0cf5a881a1c416b3d71aeb0a9c0b1603e376c551/src/Mbar/Mbar_le.lean#L585
Of course there is much more to do, including proving that it's actually a sheaf ;)

Johan Commelin (Jul 26 2021 at 16:30):

@Adam Topaz Awesome. Checking that it is a sheaf would need some stuff from the beginning of Condensed.pdf.

Johan Commelin (Jul 26 2021 at 16:31):

As in, we want easier sheaf conditions, for the special setting that we're in.

Johan Commelin (Jul 26 2021 at 16:32):

I've been really busy with a tonne of other stuff. And next week I'll be on holidays. (This week I have 2 more talks to give.)
But I think we should copy the strategy of the first half: make a push for the statement first.

Adam Topaz (Jul 26 2021 at 16:32):

And if I understand Peter's comment above, the fact that it doesn't require sheafification probably boils down to the fact that filtered colimits commute with finite limits in Type*,

Johan Commelin (Jul 26 2021 at 16:32):

This Mbar.profinite is a good test case. We'll need it anyway, even though it doesn't show up in the statement.

Johan Commelin (Jul 26 2021 at 16:34):

In the end, we need something that we might call signed_radon_measure : CondMod(real). This beast is another of those sheafs, and its definition looks very similar to Mbar.profinite.

Peter Scholze (Jul 26 2021 at 20:15):

You don't need condensed $\mathbb R$ -modules for the statement! It takes place in condensed abelian groups

Adam Topaz (Jul 26 2021 at 21:04):

I realized that I misspoke above. Mbar.profinite is not even a presheaf on Profinite. I made a version called Mbar.precondensed here https://github.com/leanprover-community/lean-liquid/blob/50f0c86e29b0988cabee4911c026591f33de255f/src/Mbar/Mbar_le.lean#L605 which, to every S : Profinite actually associates the presheaf on Profinite associated to Mbar(S). The universes make it a bit of a mess.

What's happening is the following:

Mbar_le.bifunctor is the functor which to every $c : \mathbb{R}_{\geq 0}$ and S : Profinite associates the profinite set Mbar_le r' c S.
Next, compose with the functor sending a profinite set to the representable presheaf.
Finally, take the colimit of these presheaves as c varies to obtain Mbar.precondensed.

Note that Mbar_le r' c S is defined as a limit in Profinite, where, a priori, we should be taking a limit of presheaves on Profinite, but this should give the same result.
Is it actually important for us to consider Mbar_le r' c S for profinite S as a condensed set?

Adam Topaz (Jul 26 2021 at 21:08):

Concerning the universe issue, which is related to the discussion https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/condensed.20sets/near/245993721 I ended up using presheaves of the form

(as_small.{u+1} Profinite.{u})ᵒᵖ ⥤ Type (u+1)

Johan Commelin (Jul 27 2021 at 04:41):

@Adam Topaz We will need to treat $\mathcal M(S, \Z((T))_{>r})$ as a condensed abelian group, at some point. But I'm not sure that we need Mbar as condensed something. We need $\overline{\mathcal M}_{r'}(S)$ for profinite $S$ . But by the time we need it, we have left the condensed world behind us already.

Adam Topaz (Jul 27 2021 at 11:51):

I guess the question then is still about how $$\overline\mathcal{M}_{r'}(S)$$ is defined. In which category does the colimit occur?

Johan Commelin (Jul 27 2021 at 12:17):

In the category of abelian groups, I think.

Adam Topaz (Jul 27 2021 at 12:17):

Well, the mbar_le's are just sets.

Adam Topaz (Jul 27 2021 at 12:18):

(well, Profinite sets)

Johan Commelin (Jul 27 2021 at 12:21):

Ooh, right. Sorry. So it is a colimit of sets. And the result is a profinitely filtered pseudo-normed group.

Adam Topaz (Jul 27 2021 at 12:22):

I see. Is it clear that this agrees with the construction coming from the condensed world if one forgets the condensed structure?

Adam Topaz (Jul 27 2021 at 12:23):

In any case the thing I originally defined as Mbar.profinite is exactly this colimit of sets

Johan Commelin (Jul 27 2021 at 12:26):

Adam Topaz said:

I see. Is it clear that this agrees with the construction coming from the condensed world if one forgets the condensed structure?

I guess the question is to what extent taking the representable presheaf commutes with taking colimits?

Johan Commelin (Jul 27 2021 at 12:27):

I think that it should be fine, because profinite sets are compact. So any map $T \to \mathcal M(S)$ will factor via some $\mathcal M(S)_{\le c}$ .

Adam Topaz (Jul 27 2021 at 12:34):

That sounds right.

Adam Topaz (Jul 27 2021 at 12:50):

Ah, I guess the general nonsense fact is that the representable (by a profinite set) condensed sets are compact objects.

Last updated: Dec 20 2023 at 11:08 UTC