## Stream: condensed mathematics

### Topic: controlled exactness

#### Patrick Massot (Mar 14 2021 at 21:47):

In case anyone else is tempted to work on this: tonight I started working on https://leanprover-community.github.io/liquid/index.html#prop:completeexact. There is no issue, I simply need to find a bit more time to finish it.

#### Patrick Massot (Mar 18 2021 at 17:16):

I'm returning to this today. I have a question about code that should be somewhere. I start with f : normed_group_hom G H. Where is f.completion : normed_group_hom (completion G) (completion H)? It has to be somewhere, right?

#### Patrick Massot (Mar 18 2021 at 17:16):

Let me ping @Johan Commelin, although it's probably dinner time on his planet.

#### Johan Commelin (Mar 18 2021 at 17:32):

Dinner is just over (-;

#### Johan Commelin (Mar 18 2021 at 17:33):

I have to disappoint you: locally_constant/Vhat.lean

#### Johan Commelin (Mar 18 2021 at 17:33):

It's done directly in the functor

#### Johan Commelin (Mar 18 2021 at 17:33):

But it would be good to factor that out of the definition of Completion

#### Patrick Massot (Mar 18 2021 at 17:35):

This is what I feared.

#### Patrick Massot (Mar 18 2021 at 17:36):

What about the intended use of this exactness lemma? Will you want this for homs in this category or normed_group_hom G H?

#### Johan Commelin (Mar 18 2021 at 17:39):

My expectation is that we will be firmly in the category world by then. We're talking about 8.17, right?

#### Patrick Massot (Mar 18 2021 at 17:40):

We are talking about https://leanprover-community.github.io/liquid/sect0005.html#prop:completeexact

#### Patrick Massot (Mar 18 2021 at 17:41):

Actually even if the application are in category world, the proof still discusses elements of normed groups (can you believe that?).

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

I certainly can believe that (-;

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

Note that even if you use the category lib, it's still quite convenient to work with elements

#### Johan Commelin (Mar 18 2021 at 17:45):

But feel free to work unbundled. I guess it makes sense to do that

#### Adam Topaz (Mar 18 2021 at 17:54):

@Patrick Massot while you're unbundling, it might be worthwhile to unbundle Completion.lift and the associated lemmas as well.

#### Patrick Massot (Mar 18 2021 at 21:15):

I actually need something I don't know how to prove on paper. Given a morphism of normed groups $f : G \to H$, consider its completion $\hat f : \hat G \to \hat H$. Is it always true that $\ker f$ is dense in $\ker \hat f$?

#### David Michael Roberts (Mar 18 2021 at 21:17):

Universal property of completion?

#### Patrick Massot (Mar 18 2021 at 21:18):

The only thing that looks formal to me is the inclusion $\overline{\ker f} \subset \ker \hat f$

#### Adam Topaz (Mar 18 2021 at 21:21):

Are these normed groups or one of these new pseudonormed groups?

#### Patrick Massot (Mar 18 2021 at 21:21):

Let's say normed groups for now.

#### Adam Topaz (Mar 18 2021 at 21:23):

Hmm... yeah it's tricky even in this case. I guess we can reduce to the case where f is injective, and then the goal is to show that the completion is injective as well (maybe it's not true?)

#### Patrick Massot (Mar 18 2021 at 21:27):

If it's not true then I don't know how to prove the lemma from this thread.

#### Sebastien Gouezel (Mar 18 2021 at 21:35):

I don't think it can be true. Take H an infinite-dimensional Hilbert space, G a dense subspace, x a vector not in G, and f the orthogonal projection on the orthogonal of x. Then f is injective on G, but it is not injective on its completion $\hat G = H$.

#### Adam Topaz (Mar 18 2021 at 21:37):

I was thinking of the map

$\bigoplus_{i = 1}^\infty \mathbb{R} \to \bigoplus_{i = 1}^\infty \mathbb{R}$

which on the $i$-th component acts by $x \mapsto x/2^i$.

#### Sebastien Gouezel (Mar 18 2021 at 21:37):

Just to be sure: when you say morphism of normed groups, should it preserve the norm (then my counterexample is not a counterexample), or just bounded?

#### Patrick Massot (Mar 18 2021 at 21:37):

I was also getting worried.

I meant bounded.

#### Patrick Massot (Mar 18 2021 at 21:39):

I was probably too optimistic when interpreting what Peter wrote. I'll need to reconsider my interpretation.

#### Peter Scholze (Mar 18 2021 at 21:57):

I'm back :-). Actually, I don't think I claimed that?

Or did I? ...

#### Patrick Massot (Mar 18 2021 at 21:58):

This is why I wrote "interpreting".

Let me check :-)

#### Patrick Massot (Mar 18 2021 at 21:58):

I'm looking at Proposition 8.17 of Analytic.pdf

#### Peter Scholze (Mar 18 2021 at 21:59):

OK, I think that argument is nonsense, you are right... :see_no_evil:

#### Patrick Massot (Mar 18 2021 at 21:59):

You start with $m \in \hat M$, presumably in $\ker \hat g$, and write it as an infinite sum of $m_i$. I thought the $m_i$ were meant to be in $\ker g$.

#### Peter Scholze (Mar 18 2021 at 21:59):

This seems like the only reasonable interpretation

#### Patrick Massot (Mar 18 2021 at 22:00):

That's what I thought until I tried to formalize it...

#### Peter Scholze (Mar 18 2021 at 22:00):

OK, I'll fix this. If one has a long exact sequence with such bounds, the claim is definitely correct

#### Peter Scholze (Mar 18 2021 at 22:01):

I tried to write a better "local" version, but it seems I screwed this up

#### Patrick Massot (Mar 18 2021 at 22:03):

Ok, I'll wait for the fix then. This is good timing actually, I should go to bed.

#### Patrick Massot (Mar 18 2021 at 22:04):

(I don't mean I'm expecting you to fix while I sleep, I have many other things to do tomorrow :smile: )

#### Peter Scholze (Mar 18 2021 at 22:06):

No worries, I will sleep better when it's fixed :-)

Good night!

Good night!

#### Peter Scholze (Mar 18 2021 at 22:46):

OK, the corrected version is on my webpage

#### Peter Scholze (Mar 18 2021 at 22:46):

Sorry! And thanks of course for catching the mistake :-)

#### Patrick Massot (Mar 20 2021 at 21:03):

This fix is now lean approved.

#### Patrick Massot (Mar 20 2021 at 21:04):

The statement doesn't use a four terms exact sequence, I'm simply stating the extra assumption as something about the range of the relevant map, not the kernel of the next one.

#### Patrick Massot (Mar 20 2021 at 21:10):

No new surprise in the proof, only the usual stuff when formalizing. For instance the proof that is written doesn't work when $\hat y = 0$, because you want a sequence of positive numbers $\varepsilon_i$ in the sentence

Taking the sequence of $\epsilon_i$'s sufficiently small so that $\sum_{i>0} \epsilon_i\leq \tfrac {‖\widehat{y}‖}{2C} \epsilon$

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

Great! Thanks for doing this.

#### Patrick Massot (Mar 20 2021 at 21:17):

I'll now split this into different files in preparation for mathlib PRs and merge to master. The whole thing is currently 600 lines long but a lot of preparation should go to mathlib.

#### Johan Commelin (Mar 20 2021 at 21:33):

@Patrick Massot Once you are done: please tick off your issue on https://github.com/leanprover-community/lean-liquid/projects/1

#### Adam Topaz (Mar 22 2021 at 14:09):

I now have a working definition of right and left Kan extensions in the following file:
https://github.com/leanprover-community/mathlib/blob/AT_kan_ext/src/category_theory/limits/kan_extension.lean

I'm a little annoyed that I couldn't just write out the term on line 278. Looks like @Bhavik Mehta had a similar issue in his code (which this builds on).

#### Bhavik Mehta (Mar 22 2021 at 16:18):

NIce! Is this good enough to get the restriction you wanted for finite limits?

#### Patrick Massot (Mar 22 2021 at 22:15):

I ticked it off. Now I have 10 mathlib PRs to write, but at least I mostly decided where I was going to put stuff.

Last updated: May 09 2021 at 15:11 UTC