## Stream: condensed mathematics

### Topic: possible targets for this week

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

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

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

#### 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 $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 (Mar 08 2021 at 10:14):

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

#### Johan Commelin (Mar 08 2021 at 10:15):

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

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

#### Peter Scholze (Mar 08 2021 at 10:18):

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

#### Johan Commelin (Mar 08 2021 at 10:19):

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

#### Peter Scholze (Mar 08 2021 at 10:19):

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

#### Johan Commelin (Mar 08 2021 at 10:19):

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

#### Peter Scholze (Mar 08 2021 at 10:20):

And it's the only direction we need here

#### Johan Commelin (Mar 08 2021 at 10:20):

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

#### Peter Scholze (Mar 08 2021 at 10:20):

I don't think so.

#### Johan Commelin (Mar 08 2021 at 10:20):

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

#### 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 $\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 (Mar 08 2021 at 10:22):

Probably that's not too hard

#### 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

#### Peter Scholze (Mar 08 2021 at 10:24):

This is surely even easier than the Moore complex

#### Johan Commelin (Mar 08 2021 at 10:25):

Ok, I'll take note of that.

#### 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


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

#### Johan Commelin (Mar 08 2021 at 17:55):

I only needed 9.7' for the proof of 9.8

#### 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

#### 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

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

thanks

#### Johan Commelin (Mar 08 2021 at 18:44):

some form of this should indeed go to mathlib

#### Johan Commelin (Mar 09 2021 at 07:07):

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

#### Johan Commelin (Mar 09 2021 at 07:07):

We can speed it up later

#### Johan Commelin (Mar 09 2021 at 07:07):

A proof is better than no proof :grinning:

#### 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 $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 (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,
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], } },
end

abs (a + b) = abs a + abs b ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
begin
by_cases ab : a ≤ b,
@and.comm (b ≤ 0 ) _] }
end


#### Johan Commelin (Mar 09 2021 at 08:37):

If you think it's faster, please push it

#### 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 $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 (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.

#### 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?

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


#### Johan Commelin (Mar 09 2021 at 08:48):

hhm, sounds like you had uncommited or unpushed changes locally

#### Johan Commelin (Mar 09 2021 at 08:49):

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

#### 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:

#### 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!

#### 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'.

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

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

#### Johan Commelin (Mar 09 2021 at 15:54):

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

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

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

#### Johan Commelin (Mar 09 2021 at 15:58):

(Because f is strict by assumption.)

#### 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

#### Johan Commelin (Mar 09 2021 at 16:06):

That might simplify the reasoning

#### Riccardo Brasca (Mar 09 2021 at 16:06):

I was wondering the same thing!

#### Riccardo Brasca (Mar 09 2021 at 16:07):

All is written at the moment works in general

#### Johan Commelin (Mar 09 2021 at 16:08):

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

#### Riccardo Brasca (Mar 09 2021 at 16:10):

I will do it in a couple of hours

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

#### Johan Commelin (Mar 09 2021 at 16:42):

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

#### Johan Commelin (Mar 09 2021 at 18:16):

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

#### 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?

#### 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

#### Johan Commelin (Mar 09 2021 at 18:34):

We can maybe do it in two steps, yes

#### Johan Commelin (Mar 09 2021 at 18:35):

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

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

#### 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:

#### Johan Commelin (Mar 09 2021 at 20:14):

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

#### Riccardo Brasca (Mar 09 2021 at 20:14):

Sure, the difference is very small

#### Johan Commelin (Mar 09 2021 at 20:15):

no longer, I just merged another branch into master

pushed

#### Johan Commelin (Mar 09 2021 at 20:32):

@Riccardo Brasca I fixed that continuity sorry

#### Johan Commelin (Mar 09 2021 at 20:32):

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

#### Johan Commelin (Mar 09 2021 at 20:32):

I pushed it to your branch

#### 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

#### 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!

#### Johan Commelin (Mar 09 2021 at 20:40):

yes, it is a somewhat ugly hack

#### 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 (-;

#### Johan Commelin (Mar 09 2021 at 20:42):

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

#### Riccardo Brasca (Mar 09 2021 at 21:12):

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

#### Riccardo Brasca (Mar 09 2021 at 21:13):

And I agree we should move Hom and HomZ_iso somewhere else

#### Kevin Buzzard (Mar 09 2021 at 22:35):

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

#### 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

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

#### 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

#### 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

#### Riccardo Brasca (Mar 10 2021 at 12:56):

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

#### 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

#### 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)

#### Calle Sönne (Mar 10 2021 at 13:19):

Is there anything specific that is missing?

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

#### Johan Commelin (Mar 10 2021 at 13:19):

So currently we don't have any pressing needs.

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

#### 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!

#### 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

#### 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

#### Riccardo Brasca (Mar 10 2021 at 19:22):

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

#### 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

#### Johan Commelin (Mar 10 2021 at 19:24):

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

#### Riccardo Brasca (Mar 10 2021 at 19:55):

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

#### 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?

#### 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

#### Johan Commelin (Mar 10 2021 at 21:59):

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

#### Riccardo Brasca (Mar 10 2021 at 21:59):

I will have a look, good night!

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

#### Johan Commelin (Mar 11 2021 at 04:20):

Great! I will pull your branch again.

#### Johan Commelin (Mar 11 2021 at 04:47):

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

#### 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