possible targets for this week

Stream: condensed mathematics

[Johan Commelin]

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.

[Johan Commelin]

• 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 $T^{-1}$. But it still shouldn't be hard.)

[Peter Scholze]

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.

[Johan Commelin]

@Peter Scholze From 8.19, do we need the first sentence? I think the part about hypercovers $S_\bullet \to S$ and exactness of the complex $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 (-;

[Peter Scholze]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Peter Scholze]

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

[Johan Commelin]

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

[Peter Scholze]

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

[Johan Commelin]

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

[Peter Scholze]

And it's the only direction we need here

[Johan Commelin]

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

[Peter Scholze]

I don't think so.

[Johan Commelin]

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

[Peter Scholze]

You need some good functoriality for the Moore complex to build the double complex in the proof of 9.5 (from $\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)

[Peter Scholze]

Probably that's not too hard

[Peter Scholze]

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

[Peter Scholze]

This is surely even easier than the Moore complex

[Johan Commelin]

Ok, I'll take note of that.

[Riccardo Brasca]

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?

[Johan Commelin]

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

[Johan Commelin]

I only needed 9.7' for the proof of 9.8

[Riccardo Brasca]

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

[Johan Commelin]

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

[Riccardo Brasca]

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.

[Johan Commelin]

thanks

[Johan Commelin]

some form of this should indeed go to mathlib

[Johan Commelin]

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

[Johan Commelin]

We can speed it up later

[Johan Commelin]

A proof is better than no proof :grinning:

[Johan Commelin]

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 $T^{-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.

[Damiano Testa]

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

[Johan Commelin]

If you think it's faster, please push it

[Filippo A. E. Nuccio]

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 $T^{-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.

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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?

[Filippo A. E. Nuccio]

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

[Johan Commelin]

hhm, sounds like you had uncommited or unpushed changes locally

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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:

[Riccardo Brasca]

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!

[Riccardo Brasca]

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

[Filippo A. E. Nuccio]

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.

[Riccardo Brasca]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

(Because f is strict by assumption.)

[Johan Commelin]

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

[Johan Commelin]

That might simplify the reasoning

[Riccardo Brasca]

I was wondering the same thing!

[Riccardo Brasca]

All is written at the moment works in general

[Johan Commelin]

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

[Riccardo Brasca]

I will do it in a couple of hours

[Johan Commelin]

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 $\prod_{\lambda \in \Lambda} M$, hence restricting to the factor $\lambda = 1$ should give continuity in one direction.

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Johan Commelin]

We can maybe do it in two steps, yes

[Johan Commelin]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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:

[Johan Commelin]

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

[Riccardo Brasca]

Sure, the difference is very small

[Johan Commelin]

no longer, I just merged another branch into master

[Johan Commelin]

pushed

[Johan Commelin]

@Riccardo Brasca I fixed that continuity sorry

[Johan Commelin]

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

[Johan Commelin]

I pushed it to your branch

[Johan Commelin]

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

[Riccardo Brasca]

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

[Johan Commelin]

yes, it is a somewhat ugly hack

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

And I agree we should move Hom and HomZ_iso somewhere else

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

Riccardo Brasca said:

And I agree we should move Hom and HomZ_iso somewhere else

I moved it to polyhedral_lattice/Hom.lean

[Johan Commelin]

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

[Riccardo Brasca]

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

[Calle Sönne]

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

[Calle Sönne]

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)

[Calle Sönne]

Is there anything specific that is missing?

[Johan Commelin]

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

[Johan Commelin]

So currently we don't have any pressing needs.

[Johan Commelin]

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.

[Johan Commelin]

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!

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

I will have a look, good night!

[Riccardo Brasca]

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.

[Johan Commelin]

Great! I will pull your branch again.

[Johan Commelin]

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

[Johan Commelin]

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