Zulip Chat Archive

Stream: condensed mathematics

Topic: possible targets for this week


view this post on Zulip Johan Commelin (Mar 08 2021 at 08:30):

It seems that I finally have an empty calendar after the semester finished in Feb. This week I want to bash on 9.6 and 9.8. I think we can finish them this week. That would leave us with 9.7 and the monster proof of 9.5.

  • For 9.8, there are some sorrys left in combinatorial_lemma.lean. They shouldn't be hard conceptually. A bit of wrestling with tsum.
  • For 9.6, we've made very good progress last week, I think. We need to unsorry soft_truncation.lean. We also need the obvious lemmas about how bounded_exact interacts with shifting complexes left and right.
    • After that, the induction step of 9.6 should be easy
    • The base case of the induction is half done. It shouldn't be hard to finish it.

view this post on Zulip Johan Commelin (Mar 08 2021 at 08:31):

  • There is also the unfinished implication 9.5 ==> 9.4. This amounts to constructing an isomorphism between Hom(Z, M) and M. Shouldn't be hard either. (An isom of profinitely filtered pseudo normed groups with action of T1T^{-1}. But it still shouldn't be hard.)

view this post on Zulip Peter Scholze (Mar 08 2021 at 09:01):

As I said before, I'm excited about the progress you're making! Regarding possible targets, just a reminder that the proof of 9.5 also needs some amount of simplicial stuff and Dold-Kan, and specifically 8.19.

view this post on Zulip Johan Commelin (Mar 08 2021 at 10:11):

@Peter Scholze From 8.19, do we need the first sentence? I think the part about hypercovers SSS_\bullet \to S and exactness of the complex 0M^(S)M^(S0)M^(S1)0 \to \hat M(S) \to \hat M(S_0) \to \hat M(S_1) \to \dots is the part we need, right? I guess it's also the more difficult part (-;

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:14):

Yes, that's right, we only need that hypercovers of profinite sets by profinite sets induce exact complexes.

view this post on Zulip Johan Commelin (Mar 08 2021 at 10:15):

Ok, I'll add hypercovers to my mental todo list.

view this post on Zulip Johan Commelin (Mar 08 2021 at 10:16):

Btw, the simplicial stuff was a bit quiet on this stream, but Scott created a bunch of PRs to mathlib up to the Moore complex.

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:18):

Great! What's the Moore complex? :-D

view this post on Zulip Johan Commelin (Mar 08 2021 at 10:19):

https://ncatlab.org/nlab/show/Moore+complex

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:19):

Ah, that's Dold-Kan. OK, great!

view this post on Zulip Johan Commelin (Mar 08 2021 at 10:19):

seems to be the name of one half of Dold-Kan

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:20):

And it's the only direction we need here

view this post on Zulip Johan Commelin (Mar 08 2021 at 10:20):

ooh, ok, so we don't need to go back?

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:20):

I don't think so.

view this post on Zulip Johan Commelin (Mar 08 2021 at 10:20):

you shouldn't have told us... now we won't do Dold-Kan :rofl:

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:22):

You need some good functoriality for the Moore complex to build the double complex in the proof of 9.5 (from V^\hat{V} and Λ\Lambda you build this system of complexes for 9.5, and you need that a simplicial Λ\Lambda_\bullet gives a system of double complexes)

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:22):

Probably that's not too hard

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:24):

Actually, I'm not really using the Moore complex, I'm just using what's called the "alternating face map complex" in the nLab

view this post on Zulip Peter Scholze (Mar 08 2021 at 10:24):

This is surely even easier than the Moore complex

view this post on Zulip Johan Commelin (Mar 08 2021 at 10:25):

Ok, I'll take note of that.

view this post on Zulip Riccardo Brasca (Mar 08 2021 at 17:48):

I wanted to prove

lemma abs_add_eq_add_abs_iff (a b : ) :
  abs (a + b) = abs a + abs b  (0  a  0  b  a  0  b  0) := sorry

that should be easy, but if I start with

lemma abs_add_eq_add_abs_iff (a b : ) :
  abs (a + b) = abs a + abs b  (0  a  0  b  a  0  b  0) :=
begin
  wlog hle : a  b using [a b, b a],
  { exact le_total a b },
  sorry
end

Lean becomes immediatly very slow. Is this normal or I am missing something?

view this post on Zulip Johan Commelin (Mar 08 2021 at 17:55):

Note that I'm not even sure we need that lemma. Depending on which version of 9.7 we prove.

view this post on Zulip Johan Commelin (Mar 08 2021 at 17:55):

I only needed 9.7' for the proof of 9.8

view this post on Zulip Riccardo Brasca (Mar 08 2021 at 17:56):

OK, I will wait. I thought it was trivial, but there are more cases than I expected

view this post on Zulip Johan Commelin (Mar 08 2021 at 18:04):

@Riccardo Brasca Ha, I agree, it's one of those things that should be by auto, but that are just tedious and annoying

view this post on Zulip Riccardo Brasca (Mar 08 2021 at 18:42):

I did it anyway... but still it seems very slow to me. If someone want to play with it's here
https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/combinatorial_lemma.lean

I guess that some generalization (for linear_ordered_add_comm_group maybe?) could be interesting for mathlib.

view this post on Zulip Johan Commelin (Mar 08 2021 at 18:44):

thanks

view this post on Zulip Johan Commelin (Mar 08 2021 at 18:44):

some form of this should indeed go to mathlib

view this post on Zulip Johan Commelin (Mar 09 2021 at 07:07):

@Riccardo Brasca Since you removed the sorry, I merged your branch into master.

view this post on Zulip Johan Commelin (Mar 09 2021 at 07:07):

We can speed it up later

view this post on Zulip Johan Commelin (Mar 09 2021 at 07:07):

A proof is better than no proof :grinning:

view this post on Zulip Johan Commelin (Mar 09 2021 at 07:58):

Johan Commelin said:

  • There is also the unfinished implication 9.5 ==> 9.4. This amounts to constructing an isomorphism between Hom(Z, M) and M. Shouldn't be hard either. (An isom of profinitely filtered pseudo normed groups with action of T1T^{-1}. But it still shouldn't be hard.)

I filled in all the data for the isomorphism. So now we only need to fill in some proofs.

view this post on Zulip Damiano Testa (Mar 09 2021 at 08:35):

Is this version of Riccardo's lemma faster?

lemma abs_add_eq_add_abs {α : Type*} [linear_ordered_add_comm_group α]  {a b : α} (hle : a  b) :
  abs (a + b) = abs a + abs b  (0  a  0  b  a  0  b  0) :=
begin
  by_cases a0 : 0  a; by_cases b0 : 0  b,
  { simp [a0, b0, abs_of_nonneg, add_nonneg a0 b0] },
  { exact (lt_irrefl (0 : α) (a0.trans_lt (hle.trans_lt (not_le.mp b0)))).elim },
  { obtain F := (not_le.mp a0),
    simp [a0, b0, abs_of_neg, abs_of_nonneg, F, F.le],
    refine λ h, _, λ h, _⟩,
    { by_cases ba : a + b  0,
      { rw abs_of_nonpos ba at h,
        simp [add_comm (-a)] at h,
        exact le_of_eq (eq_zero_of_neg_eq h) },
      { rw [abs_of_pos (not_le.mp ba), add_left_inj] at h,
        rw eq_zero_of_neg_eq (eq.symm h) at F,
        exact (lt_irrefl (0 : α) F).elim } },
    { simp [le_antisymm h b0, abs_of_neg F], } },
  { simp [(not_le.mp a0).le, (not_le.mp b0).le, abs_of_nonpos, add_nonpos, add_comm] }
end


lemma abs_add_eq_add_abs_iff {α : Type*} [linear_ordered_add_comm_group α]  (a b : α) :
  abs (a + b) = abs a + abs b  (0  a  0  b  a  0  b  0) :=
begin
  by_cases ab : a  b,
  { exact abs_add_eq_add_abs ab },
  { rw [add_comm a, add_comm (abs _), abs_add_eq_add_abs ((not_le.mp ab).le), and.comm,
    @and.comm (b  0 ) _] }
end

view this post on Zulip Johan Commelin (Mar 09 2021 at 08:37):

If you think it's faster, please push it

view this post on Zulip Filippo A. E. Nuccio (Mar 09 2021 at 08:44):

Johan Commelin said:

Johan Commelin said:

  • There is also the unfinished implication 9.5 ==> 9.4. This amounts to constructing an isomorphism between Hom(Z, M) and M. Shouldn't be hard either. (An isom of profinitely filtered pseudo normed groups with action of T1T^{-1}. But it still shouldn't be hard.)

I filled in all the data for the isomorphism. So now we only need to fill in some proofs.

I have not been following this thread for ten days or so, trying to (lose my) battle with Laurent series. I would be happy in trying to fill some, although others will probably be faster than me.

view this post on Zulip Johan Commelin (Mar 09 2021 at 08:44):

Ooh, there are > 30 sorrys at the moment. If you claim one, I'm sure others can work on other stuff.

view this post on Zulip Filippo A. E. Nuccio (Mar 09 2021 at 08:46):

Ok, I'll give it a try. I am having some issue with the .toml, though. I run leanproject up, yet if I try git pull I get a merging issue. Is it normal?

view this post on Zulip Filippo A. E. Nuccio (Mar 09 2021 at 08:47):

Auto-merging leanpkg.toml
CONFLICT (content): Merge conflict in leanpkg.toml
Automatic merge failed; fix conflicts and then commit the result.

view this post on Zulip Johan Commelin (Mar 09 2021 at 08:48):

hhm, sounds like you had uncommited or unpushed changes locally

view this post on Zulip Johan Commelin (Mar 09 2021 at 08:49):

@Filippo A. E. Nuccio what does your git log and git status look like?

view this post on Zulip Filippo A. E. Nuccio (Mar 09 2021 at 08:50):

right, I have something in my git log to fix. I'll try on my own and come back if I need help-->done. :octopus:

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 09:30):

I made the PR #6593, with a slightly more general version of abs_add_eq_add_abs_iff. @Damiano Testa If you have a better proof, can you comment there? Thank you!

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 12:56):

@Filippo A. E. Nuccio are you working on HomZ_iso? I just proved (and pushed to master) strict'.

view this post on Zulip Filippo A. E. Nuccio (Mar 09 2021 at 13:20):

Yes, I am going to work on this a bit today and tomorrow. Thanks for telling me this is done! As soon as I will find something I can work on, I'll claim it here.

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 15:53):

In HomZ_iso the only sorrys left are the two continuous', they seem not completely trivial to me (even mathematically), but maybe I am missing something.

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:54):

@Riccardo Brasca Great! Thanks a lot for your efforts.

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:54):

I guess those continuity arguments will have to use that the norm on Z is completely boring.

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:58):

Note that there is also a sorry left in the proof of first_target, which should hopefully follow from a general lemma saying that (BD.System _ _ _).map f is always strict.

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:58):

(Because f is strict by assumption.)

view this post on Zulip Johan Commelin (Mar 09 2021 at 16:06):

@Riccardo Brasca I just realised that homZ_iso shouldn't just work for Mbar r' S but any M

view this post on Zulip Johan Commelin (Mar 09 2021 at 16:06):

That might simplify the reasoning

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 16:06):

I was wondering the same thing!

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 16:07):

All is written at the moment works in general

view this post on Zulip Johan Commelin (Mar 09 2021 at 16:08):

yes, please refactor. I was just sleepy when I wrote the sketch this morning

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 16:10):

I will do it in a couple of hours

view this post on Zulip Johan Commelin (Mar 09 2021 at 16:42):

Some thoughts:

  • a new constructor can assume continuity in only one direction, because the spaces are compact Hausdorff
  • the topology on Hom(Lambda, M) is the subspace topology of λΛM\prod_{\lambda \in \Lambda} M, hence restricting to the factor λ=1\lambda = 1 should give continuity in one direction.

view this post on Zulip Johan Commelin (Mar 09 2021 at 16:42):

Now I need to go. Back in a couple of hrs

view this post on Zulip Johan Commelin (Mar 09 2021 at 18:16):

I'm back. Let me know if you get stuck somewhere with the topology

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 18:24):

Is there a reason to state the lemma for profinitely_filtered_pseudo_normed_group_with_Tinv and not for profinitely_filtered_pseudo_normed_group?

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 18:24):

I see that the morphisms are a little different (bounded in one case and strict in the other), but it should be true

view this post on Zulip Johan Commelin (Mar 09 2021 at 18:34):

We can maybe do it in two steps, yes

view this post on Zulip Johan Commelin (Mar 09 2021 at 18:35):

But we need the Tinv compatibility for the 9.5 => 9.4 proof.

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 20:08):

I've pushed here https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/thm95.lean the easy generalization to any M.

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 20:09):

As Johan said, the proof of the second continuous' should be easy, but I am a bit lost because of elements of subsets, rewriting under λ and similar stuff :innocent:

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:14):

@Riccardo Brasca is it ok if I merge master into your branch?

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 20:14):

Sure, the difference is very small

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:15):

no longer, I just merged another branch into master

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:16):

pushed

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:32):

@Riccardo Brasca I fixed that continuity sorry

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:32):

There was a very useful trick that I wrote for another part of the project

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:32):

I pushed it to your branch

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:33):

For the final sorry, I suggest that we build the alternative constructor for isoms of profinitely_filtered_pseudo_normed_group_with_Tinvs

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 20:36):

Ahah, I see that you already wrote section pfpng_ctu exactly to deal with this kind if problems!

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:40):

yes, it is a somewhat ugly hack

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:40):

I guess this is the price we pay for working with topological_spaces instead of actual profinite sets (-;

view this post on Zulip Johan Commelin (Mar 09 2021 at 20:42):

Maybe we should also move Hom and HomZ_iso to a different file, at some point

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 21:12):

I will stop for today. If someone wants to play with my branch no problem

view this post on Zulip Riccardo Brasca (Mar 09 2021 at 21:13):

And I agree we should move Hom and HomZ_iso somewhere else

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 22:35):

You know that @Calle Sönne has a ton of stuff for profinite sets formalised?

view this post on Zulip Johan Commelin (Mar 10 2021 at 03:52):

This will be extremely useful when we start building the category of condensed sets, and gluing our first_target into the condensed setting

view this post on Zulip Johan Commelin (Mar 10 2021 at 03:52):

If there are any PRs that I should review, @Calle Sönne please just ping me. I sometimes loose track of PRs because the queue is now moving so fast.

view this post on Zulip Johan Commelin (Mar 10 2021 at 07:05):

Riccardo Brasca said:

And I agree we should move Hom and HomZ_iso somewhere else

I moved it to polyhedral_lattice/Hom.lean

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:29):

From the targets listed at the top of this thread, the status is now:

:check: 9.8 done
:white_large_square: 9.6 making good progress with usable complexes, but both the base case and the induction step are still open
:white_large_square: 9.5 => 9.4, Riccardo made some nice progress yesterday

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 12:56):

I have some time now to end the proof HomZ_iso, defining a new constructor

view this post on Zulip Calle Sönne (Mar 10 2021 at 13:17):

Johan Commelin said:

If there are any PRs that I should review, Calle Sönne please just ping me. I sometimes loose track of PRs because the queue is now moving so fast.

I realised that there was a missing piece for me to PR the rest of "profinite sets are limit of finite discrete sets" to mathlib. It relies on some old implementation of Profinite having limits and I have not yet had the time to resolve that. So for now there are no PRs of mine that needs reviewing

view this post on Zulip Calle Sönne (Mar 10 2021 at 13:18):

Kevin Buzzard said:

You know that Calle Sönne has a ton of stuff for profinite sets formalised?

I think most of my work has been doing a bunch of lemmas for topological spaces. The only stuff for profinite sets I have actually proven are that they are reflective in CompHaus and that they are limits of finite discrete sets (this one is not yet in mathlib though)

view this post on Zulip Calle Sönne (Mar 10 2021 at 13:19):

Is there anything specific that is missing?

view this post on Zulip Johan Commelin (Mar 10 2021 at 13:19):

@Calle Sönne For the first part of the project, we don't yet need much about profinite sets. It will become useful in the second stage.

view this post on Zulip Johan Commelin (Mar 10 2021 at 13:19):

So currently we don't have any pressing needs.

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:20):

Riccardo Brasca said:

I have some time now to end the proof HomZ_iso, defining a new constructor

How are things going? I fixed the other sorry in liquid.lean. So once we have this new constructor, the proof 9.5 => 9.4 is complete.

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:26):

I'm quite happy that liquid.lean and combinatorial_lemma.lean no longer show up in the list of files that contain sorry.
We are making progress!

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 19:20):

I've pushed to https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/polyhedral_lattice/Hom.lean the sorry free proof of HomZ_iso

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 19:21):

Some remarks: in https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/pseudo_normed_group/with_Tinv.lean I proved that a bijective profinitely_filtered_pseudo_normed_group_with_Tinv_hom with strict inverse is an isomorphism

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 19:22):

The proof of continuous' in inv_of_bijective can probably be golfed quite a lot.

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 19:23):

Also Hom.lean is probably a little mess, I am not that familiar with the category theory part of the library, so it's very possible that I wrote something in not the optimal way

view this post on Zulip Johan Commelin (Mar 10 2021 at 19:24):

@Riccardo Brasca great!! thanks so much for doing this

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 19:55):

I'll wait for someone to have a look at it before merging to master :)

view this post on Zulip Johan Commelin (Mar 10 2021 at 21:25):

@Riccardo Brasca I'll now take a look at this. Is it ok if I merge master into your branch again?

view this post on Zulip Johan Commelin (Mar 10 2021 at 21:58):

@Riccardo Brasca I need to go to bed now. But I pushed some wip to jmc-Hom

view this post on Zulip Johan Commelin (Mar 10 2021 at 21:59):

it doesn't compile, but you might get the idea of where I was going

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 21:59):

I will have a look, good night!

view this post on Zulip Riccardo Brasca (Mar 10 2021 at 23:51):

I merged your work in my branch and it now compiles. I also made some variables implicit (for example r): this seems more reasonable to me, but maybe it's a bad idea for the rest of the work.

view this post on Zulip Johan Commelin (Mar 11 2021 at 04:20):

Great! I will pull your branch again.

view this post on Zulip Johan Commelin (Mar 11 2021 at 04:47):

@Riccardo Brasca thanks again! I merged your branch into master.

view this post on Zulip Johan Commelin (Mar 11 2021 at 04:47):

The proof of 9.5 => 9.4 is now sorry-free. Kudos to Riccardo. :octopus:


Last updated: May 09 2021 at 15:11 UTC