Zulip Chat Archive

Stream: condensed mathematics

Topic: Lemma 9.8

Adam Topaz (Jan 26 2022 at 18:58):

I started looking at the profinite version of lemma 9.8.

I added a few sorry's to the file https://github.com/leanprover-community/lean-liquid/blob/master/src/combinatorial_lemma/profinite.lean

Many of these sorry's should be easy, but the most serious one so far is

instance (c) : preserves_limits (
  hom_functor r Λ ⋙
  ProFiltPseuNormGrpWithTinv₁.to_PFPNG₁ r ⋙
  ProFiltPseuNormGrp₁.level.obj c ) := sorry

This says that

$Hom(\Lambda,\lim_i A_i)_{\le c} = \lim_i (Hom(\Lambda,A_i)_{\le c})$

where everything in sight is considered as objects of ProFiltPseuNormGrpWithTinv₁.
I haven't checked all the details, but I'm fairly sure this is correct (or at least some approximation should be correct).

Peter Scholze (Jan 26 2022 at 19:27):

I'm also confident that this is true

Adam Topaz (Jan 26 2022 at 19:31):

Thanks! Okay, i think I see a straightforward proof as well... once we choose generators $(a_i)_i$ for $\Lambda$ , $Hom(\Lambda,lim_i A_i)_{\le c}$ essentially becomes $(\lim_i A_i)_{c \cdot e_1} \times \cdots \times (\lim_i A_i)_{c \cdot e_n}$ for some $e_i$ 's, and the way limits are defined in this strange category gives us $(\lim_i A_{i,c \cdot e_1}) \times \cdots \times (\lim_i A_{i,c \cdot e_n})$ . Now the limits commute with the product, so we get $\lim_i (A_{i,c \cdot e_1} \times \cdots \times A_{i,c \cdot e_n})$ , which then becomes $\lim_i(Hom(\Lambda,A_i)_{\le c})$ .

Peter Scholze (Jan 26 2022 at 19:33):

Yes, essentially. Except you can't always quite take generators like that (what's true is that $\mathrm{Hom}(\Lambda,\mathrm{lim}_i A_i)_{\leq c}$ is an appropriate fibre product, and then the argument works)

Adam Topaz (Jan 26 2022 at 19:38):

Yeah I see now... the generators for the norm need not be free generators for the module.

Adam Topaz (Jan 27 2022 at 05:19):

This should simplify the proof a little bit: #11690

Adam Topaz (Jan 27 2022 at 21:35):

combinatorial_lemma/profinite.lean and pseudo_normed_group/category.lean have some new fairly simple sorry's, in case anyone is bored...

Johan Commelin (Jan 28 2022 at 04:49):

Adam Topaz said:

This should simplify the proof a little bit: #11690

This is now merged. I can do a mathlib bump, unless you already started @Adam Topaz?

Adam Topaz (Jan 28 2022 at 04:50):

I wanted to hack around a bit on lemma 9.8. I probably won't get anywhere, but do you mind waiting for about 1 hour?

Johan Commelin (Jan 28 2022 at 04:50):

Sure!

Adam Topaz (Jan 28 2022 at 05:48):

I went ahead and did the mathlib bump (and kill the associated sorry covered by #11690 ).

Adam Topaz (Feb 01 2022 at 06:28):

I have a working skeleton for lemma 9.8 here

https://github.com/leanprover-community/lean-liquid/blob/9e8611aff040e7303882df3a345e46d9f72e4d8e/src/combinatorial_lemma/profinite.lean#L253

I made a separate declaration, since it has additional universe restrictions on Lambda and S, but I don't think these will be an issue later on (I just didn't want to break the build in some other file because of universe nonsense before going to sleep). This file has various fairly reasonable sorry's, in case anyone wants to take a look! (And now I'm off to sleep.)

Johan Commelin (Feb 01 2022 at 06:32):

Sleep tight!

Johan Commelin (Feb 01 2022 at 08:52):

7 sorries left.

Johan Commelin (Feb 01 2022 at 08:53):

Now I need to do something else

Johan Commelin (Feb 01 2022 at 11:16):

5 sorries left (in profinite.lean)

Adam Topaz (Feb 01 2022 at 20:28):

Hi all... A quick update -- Lemma 9.8 is done in the profinite case
https://github.com/leanprover-community/lean-liquid/blob/03989626d8bc87e555d2c4a359f12cf80dcb27af/src/combinatorial_lemma/profinite.lean#L474

This was a bit more challenging that I had envisioned. It involved proving that various functors between our profinitely_filtered categories preserve limits, as well as the level functors to Profinite. In the process, I showed that limits in the category of profinitely filtered pseudo normed groups (with exhaustive filtration and strict morphisms) are "almost" computed by the limit of the underlying abelian groups, except one must consider at the bounded elements (w.r.t. the filtration on the projections). Also, I was happy to finally use docs#Compactum somewhere useful to get rid of some continuity proofs by reducing some arguments to limits in PseuNormGrp_1 (note that this PseuNormGrp_1 category did not exist before 4 days ago, and now we know that it has limits, etc.).

Adam Topaz (Feb 01 2022 at 20:28):

Thanks also Johan for killing off a few of the last sorry's.

David Michael Roberts (Feb 02 2022 at 11:46):

So I guess this should be updated, then: https://leanprover-community.github.io/liquid/intro.html#a0000000012

Johan Commelin (Feb 02 2022 at 11:48):

@David Michael Roberts No, I don't think so. That still seems accurate.

Johan Commelin (Feb 02 2022 at 11:49):

Until like 24 hrs ago, the status was as follows: Thm 9.4, Thm 9.5, and Lem 9.8 were all done for finite sets S.
Now the status is that they are all done for profinite sets S.

Johan Commelin (Feb 02 2022 at 11:49):

But we still need to do more work to deduce the final target.

Johan Commelin (Feb 02 2022 at 11:50):

See https://github.com/leanprover-community/lean-liquid/projects/2 for a very rough picture of what's done and what's left to do.

David Michael Roberts (Feb 02 2022 at 12:00):

@Johan Commelin ah, ok, thanks. It may be the independent numbering of Scholze's pdf(s) and the roadmap may have confused me.

Johan Commelin (Feb 02 2022 at 12:02):

Yeah, I understand how that can be confusing

Last updated: Dec 20 2023 at 11:08 UTC