controlled exactness

Stream: condensed mathematics

[Patrick Massot]

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]

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]

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

[Johan Commelin]

Dinner is just over (-;

[Johan Commelin]

I have to disappoint you: locally_constant/Vhat.lean

[Johan Commelin]

It's done directly in the functor

[Johan Commelin]

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

[Patrick Massot]

This is what I feared.

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

I certainly can believe that (-;

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Patrick Massot]

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]

Universal property of completion?

[Patrick Massot]

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

[Adam Topaz]

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

[Patrick Massot]

Let's say normed groups for now.

[Adam Topaz]

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]

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

[Sebastien Gouezel]

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]

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]

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]

I was also getting worried.

[Patrick Massot]

I meant bounded.

[Patrick Massot]

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

[Peter Scholze]

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

[Peter Scholze]

Or did I? ...

[Patrick Massot]

This is why I wrote "interpreting".

[Peter Scholze]

Let me check :-)

[Patrick Massot]

I'm looking at Proposition 8.17 of Analytic.pdf

[Peter Scholze]

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

[Patrick Massot]

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]

This seems like the only reasonable interpretation

[Patrick Massot]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Peter Scholze]

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

[Peter Scholze]

Good night!

[Patrick Massot]

Good night!

[Peter Scholze]

OK, the corrected version is on my webpage

[Peter Scholze]

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

[Patrick Massot]

This fix is now lean approved.

[Patrick Massot]

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]

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]

Great! Thanks for doing this.

[Patrick Massot]

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]

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

[Adam Topaz]

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]

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

[Patrick Massot]

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.