Zulip Chat Archive

Stream: condensed mathematics

Topic: controlled exactness


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 18 2021 at 17:16):

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

view this post on Zulip Johan Commelin (Mar 18 2021 at 17:32):

Dinner is just over (-;

view this post on Zulip Johan Commelin (Mar 18 2021 at 17:33):

I have to disappoint you: locally_constant/Vhat.lean

view this post on Zulip Johan Commelin (Mar 18 2021 at 17:33):

It's done directly in the functor

view this post on Zulip Johan Commelin (Mar 18 2021 at 17:33):

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

view this post on Zulip Patrick Massot (Mar 18 2021 at 17:35):

This is what I feared.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 18 2021 at 17:40):

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

view this post on Zulip 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?).

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

I certainly can believe that (-;

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 18 2021 at 17:45):

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

view this post on Zulip 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.

view this post on Zulip 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:GHf : G \to H, consider its completion f^:G^H^\hat f : \hat G \to \hat H. Is it always true that kerf\ker f is dense in kerf^\ker \hat f?

view this post on Zulip David Michael Roberts (Mar 18 2021 at 21:17):

Universal property of completion?

view this post on Zulip Patrick Massot (Mar 18 2021 at 21:18):

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

view this post on Zulip Adam Topaz (Mar 18 2021 at 21:21):

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

view this post on Zulip Patrick Massot (Mar 18 2021 at 21:21):

Let's say normed groups for now.

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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 G^=H\hat G = H.

view this post on Zulip Adam Topaz (Mar 18 2021 at 21:37):

I was thinking of the map

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

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 18 2021 at 21:37):

I was also getting worried.

view this post on Zulip Patrick Massot (Mar 18 2021 at 21:37):

I meant bounded.

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 18 2021 at 21:57):

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

view this post on Zulip Peter Scholze (Mar 18 2021 at 21:58):

Or did I? ...

view this post on Zulip Patrick Massot (Mar 18 2021 at 21:58):

This is why I wrote "interpreting".

view this post on Zulip Peter Scholze (Mar 18 2021 at 21:58):

Let me check :-)

view this post on Zulip Patrick Massot (Mar 18 2021 at 21:58):

I'm looking at Proposition 8.17 of Analytic.pdf

view this post on Zulip Peter Scholze (Mar 18 2021 at 21:59):

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

view this post on Zulip Patrick Massot (Mar 18 2021 at 21:59):

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

view this post on Zulip Peter Scholze (Mar 18 2021 at 21:59):

This seems like the only reasonable interpretation

view this post on Zulip Patrick Massot (Mar 18 2021 at 22:00):

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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 18 2021 at 22:01):

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

view this post on Zulip 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.

view this post on Zulip 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: )

view this post on Zulip Peter Scholze (Mar 18 2021 at 22:06):

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

view this post on Zulip Peter Scholze (Mar 18 2021 at 22:07):

Good night!

view this post on Zulip Patrick Massot (Mar 18 2021 at 22:10):

Good night!

view this post on Zulip Peter Scholze (Mar 18 2021 at 22:46):

OK, the corrected version is on my webpage

view this post on Zulip Peter Scholze (Mar 18 2021 at 22:46):

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

view this post on Zulip Patrick Massot (Mar 20 2021 at 21:03):

This fix is now lean approved.

view this post on Zulip 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.

view this post on Zulip 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 y^=0\hat y = 0, because you want a sequence of positive numbers εi\varepsilon_i in the sentence

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

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

Great! Thanks for doing this.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Bhavik Mehta (Mar 22 2021 at 16:18):

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

view this post on Zulip 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