Zulip Chat Archive

Stream: condensed mathematics

Topic: normed snake lemma


view this post on Zulip Johan Commelin (Jan 20 2021 at 12:43):

I pushed a statement of Proposition 9.10 (the normed snake lemma) to the file normed_snake.lean.
(cc @Riccardo Brasca)

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 12:53):

Great! This looks like something not too hard

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 12:53):

You probably forgot a lemma normed_snake at the of the file

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 12:54):

I mean, you forgot to write the statement :)

view this post on Zulip Johan Commelin (Jan 20 2021 at 12:55):

ooops, forgot to save before pushing. I pushed again.

view this post on Zulip Adam Topaz (Jan 20 2021 at 15:02):

In case anyone is working on this -- I just fixed the docstring (make sure to pull :smile: )
https://github.com/leanprover-community/lean-liquid/blob/9eca62d7c442709436ef5ce2f22a9b327c486914/src/normed_snake.lean#L28

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 15:04):

I am interested in it, but still in the process of reading the "normal" math

view this post on Zulip Adam Topaz (Jan 20 2021 at 15:13):

Okay, I just killed the easy sorry in that file :)

view this post on Zulip Johan Commelin (Jan 20 2021 at 15:16):

I fixed a typo in the statement.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 16:26):

In the statement of normed_snake I think that the fact that N is the quotient M'/M is missing: there is hg : ∀ c i, function.surjective (g.apply c i), but g seems unrelated to M. Am I missing something?

view this post on Zulip Adam Topaz (Jan 20 2021 at 16:37):

I think that's implied by the assumption hg, right?

view this post on Zulip Adam Topaz (Jan 20 2021 at 16:38):

Oh, maybe the assumption that Mis the kernel of g is missing?

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 16:40):

Yes hg says that g is surjective, but not that M is its kernel

view this post on Zulip Adam Topaz (Jan 20 2021 at 16:42):

Yeah it seems like the assumption is missing, unless I'm mmissing something...

view this post on Zulip Johan Commelin (Jan 20 2021 at 16:50):

Sorry, you are right. Please add an "exactness in the middle assumption".

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 17:21):

Also the quotient norm I don't think satisfies the written property hN : ∀ c i x, ∥g.apply c i x∥ = ∥x∥: usually the norm on the quotient is the inf over all the representative of an element.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 17:22):

I have to think a little bit about it, but we probably need something like a proposition is_quotient g and assume that

view this post on Zulip Johan Commelin (Jan 20 2021 at 17:26):

Yep... I wrote a hasty statement

view this post on Zulip Johan Commelin (Jan 20 2021 at 17:27):

At least we want to describe the quotient, but not use a construction in the statement. That will make it easier to apply this lemma.

view this post on Zulip Johan Commelin (Jan 20 2021 at 17:28):

Riccardo Brasca said:

I have to think a little bit about it, but we probably need something like a proposition is_quotient g and assume that

I like this idea!

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 17:32):

At least the quotient is "pointwise" by definition if I understand where the proposition is used

view this post on Zulip Adam Topaz (Jan 20 2021 at 17:49):

Thinking out loud here: If I were planning to prove the "usual" snake lemma, I think the easiest assumption is to say that "for all x, if g x = 0 then there exists y such that f y = x" and "for all y, g (f y) = 0". Thoughts?

view this post on Zulip Johan Commelin (Jan 20 2021 at 17:50):

We will probably want both versions (pointy and pointfree). One is useful for proving, the other is good for applying in categorical settings.

view this post on Zulip Adam Topaz (Jan 20 2021 at 17:51):

Okay, sure. I guess we should just have some basic api for quotients in NormedGroup.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 17:51):

@Adam Topaz this condition is for sure necessary, but we also have to say something about the norm on the quotient

view this post on Zulip Adam Topaz (Jan 20 2021 at 17:52):

Riccardo Brasca said:

Adam Topaz this condition is for sure necessary, but we also have to say something about the norm on the quotient

Yes, I agree, but that's already there, right?

view this post on Zulip Adam Topaz (Jan 20 2021 at 17:52):

Oh right, I see your comment above now. Sorry I was away for a bit and catching up on the discussion now.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 17:53):

Maybe I am confused, but the condition already there is too strong: it implies that x=y||x|| = ||y|| if g(x)=g(y)g(x) = g(y)

view this post on Zulip Johan Commelin (Jan 20 2021 at 17:53):

sure, that condition should be removed

view this post on Zulip Adam Topaz (Jan 20 2021 at 17:54):

Yeah, this is too strong -- it implies strictness, right? Hence it implies injectivity!

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 17:54):

For usual Banach space we have π(x)x||\pi(x)|| \leq ||x||, where π\pi is the projection

view this post on Zulip Johan Commelin (Jan 20 2021 at 17:54):

Right, me stupid :oops: :rofl:

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 17:54):

But I don't think this property characterize the projection

view this post on Zulip Johan Commelin (Jan 20 2021 at 17:55):

I think your inf idea sounded good. But the best thing would be to define is_quotient and prove that it has the univ. property.

view this post on Zulip Adam Topaz (Jan 20 2021 at 18:07):

Is this the idiomatic way to construct the image of a morphism (as a subgroup)?

( : add_subgroup V₁).map f.to_add_monoid_hom

Seems a bit silly...

view this post on Zulip Johan Commelin (Jan 20 2021 at 18:11):

There should be add_monoid_hom.image but we might want to add a copy of that for normed_group_hom.

view this post on Zulip Adam Topaz (Jan 20 2021 at 18:11):

I didn't find any such thing.... I'll look harder.

view this post on Zulip Johan Commelin (Jan 20 2021 at 18:15):

Hmm, maybe we only have it for linear maps

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 18:53):

I am pretty sure this is true, but are we 100% sure that the underlying group of the quotient as normed groups is the groups quotient?

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 18:53):

I mean at the beginning I was wondering about what happens if the subgroup is not closed, but this is impossible since it is complete

view this post on Zulip Johan Commelin (Jan 20 2021 at 18:56):

normed groups aren't assumed to be complete

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 18:58):

Ah... I just checked, for R\mathbf{R}-Banach spaces the quotient exists if the subspace is closed (at least everybody seems to assume this)

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 18:58):

But maybe it is to have the quotient complete, I have to read the proof

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 19:02):

Something is happening here: if aYˉa \in \bar Y but a∉Ya \not \in Y then aX/Y=0||a||_{X/Y} = 0... and indeed the fact that the subspace is closed it used in the literature to prove that the quotient norm is a norm (a=0||a||=0 iff a=0a=0)

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:04):

aah, in [Analytic] normed groups are not assumed to be separated

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:04):

so we should change the definition in Lean

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:05):

maybe we can call those prenormed_groups or something like that. (So they aren't metric spaces, because you can have a nontrivial subgroup of elements with norm 0.)

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:07):

On the other hand... I think we only care about complete normed groups, for the applications of the normed snake lemma in the proof of 9.4.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 19:09):

So when there is "normed group" we mean "seminormed group"?

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:10):

maybe... this is roughly the first time in my life that I work with normed groups that are not DVR's/local fields.

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:10):

See the top of appendix 2 to section 8 (defn 8.16)

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 19:12):

Ah ok, it's called separated if x||x|| implies x=0x=0

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:13):

So in Lean normed_group implies separated. And for the statement of 9.4 that is not a problem, because everything is complete.

view this post on Zulip Adam Topaz (Jan 20 2021 at 19:13):

But one has to then take the completion of the quotient.

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:14):

because the subgroups might not be closed? makes sense

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:14):

So my guess is that we should introduce seminormed_group or something like that, which drops the separatedness.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 19:14):

If you require separateness then the quotient exist for closed subspace

view this post on Zulip Adam Topaz (Jan 20 2021 at 19:15):

I guess the issue is really that the image of a morphism need not be a closed subgroup?

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 19:16):

Or maybe it depends on what you call quotient. The gadget that satisfies the universal property will be the quotient by the closure I think

view this post on Zulip Adam Topaz (Jan 20 2021 at 19:16):

Right.... so the other option is to take the closure of the image, and take the quotient by that.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 19:16):

Yes, this issues exists already for "standard" Banach spaces

view this post on Zulip Adam Topaz (Jan 20 2021 at 19:16):

oh that's what you wrote :)

view this post on Zulip Adam Topaz (Jan 20 2021 at 19:20):

ugh, I guess we need an api for the closure of a subgroup... I don't think this exists in mathlib.

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:22):

there is a thorough api for separation and completion.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 19:24):

After a very quick reading of the proof of 9.10 I have the impression that the only property of the quotient (semi)norm we need there is π(x)x||\pi(x)|| \leq ||x|| where π\pi is the projection

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:26):

maybe we should just try formalizing it

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:26):

the proof looks very Leanable

view this post on Zulip Johan Commelin (Jan 20 2021 at 19:26):

does someone want to livestream their attempt?

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 19:26):

I am probably far too optimistic, but the proof seems very explicit. I will try to add "by hand" the assumption I need about the quotient to see if is doable

view this post on Zulip Heather Macbeth (Jan 20 2021 at 19:27):

In docs#inner_product_space one has this issue for the orthogonal projection, docs#orthogonal_projection. It takes a completeness hypothesis.

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 20:03):

I think this is a sensible statement

lemma normed_snake (k : 0) (m : ) (c₀ : 0) [fact (1  k)]
  (hf :  c i, normed_group_hom.is_strict (f.apply c i))
  (Hf :  (c : 0) (i : ) (hi : i  m+1) (x : M.X (k * c) i),
    (M.res x : M.X c i)  k * f.apply (k*c) i x)
  (hg :  c i, (g.apply c i).ker  (f.apply c i).range)
  (hN :  c i x, g.apply c i x = x)
  -- jmc: Is this ↑↑ the correct way of saying "`N` has the quotient norm"?
  (hM : M.is_bdd_exact_for_bdd_degree_above_idx k m c₀)
  (hM' : M'.is_bdd_exact_for_bdd_degree_above_idx k m c₀)
  (hM_adm : M.admissible)
  (hM'_adm : M'.admissible)
  (k_new : 0) [fact (1  k_new)] (hk : k_new = k^3 + k) :
  N.is_bdd_exact_for_bdd_degree_above_idx k_new (m-1) c₀

I've added

/-- The image of a bounded group homomorphism. Naturally endowed with a `normed_group` instance. -/
def range : add_subgroup V₂ := f.to_add_monoid_hom.range

In src/for_mathlib/normed_group_hom.lean (I didn't check, but all the basic properties, like for the kernel, should be immediate).

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:04):

hmmm, the hN still looks wrong, right?

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:04):

should that = be \le?

view this post on Zulip Riccardo Brasca (Jan 20 2021 at 20:05):

Ops, I thought I did it

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:05):

We should just start proving it. I think the proof will really be fun.

view this post on Zulip Adam Topaz (Jan 20 2021 at 20:07):

Johan Commelin said:

does someone want to livestream their attempt?

I would like to, but I'm busy this afternoon.

view this post on Zulip Peter Scholze (Jan 20 2021 at 20:17):

You are really making me a bit nervous about the things I've written. Exactly as it should be! :-)
In 9.10, the hypothesis imposed is ensuring that on separated completions, the map from MM to MM' is "pro-injective" (any element in the kernel gets killed by some (explicit) restriction map), but on the norm-00-part arbitrary things can happen. Fortunately, the notion of k\leq k-exactness actually only depends on the separated quotients! So I think what I wrote should be OK.

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:23):

@Peter Scholze so what would you suggest/prefer... that we work with the separated notion normed_group, or that we generalize (like in your notes) to include the non-separated case?

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:24):

I guess we could postpone this question for the time being.

view this post on Zulip Peter Scholze (Jan 20 2021 at 20:44):

good question. it's fine to always pass to separated quotients, so I guess you can just stick with the API you have

view this post on Zulip Bhavik Mehta (Jan 20 2021 at 21:44):

Johan Commelin said:

We will probably want both versions (pointy and pointfree). One is useful for proving, the other is good for applying in categorical settings.

In case it's useful, I think it's worth being aware of @Markus Himmel's work on abelian categories, and in particular his proof of the four lemma using pseudoelements

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 12:39):

In my previous version of the lemma I also forgot that g must be surjective. Here is a new statement.

lemma normed_snake (k : 0) (m : ) (c₀ : 0) [fact (1  k)]
  (hf :  c i, normed_group_hom.is_strict (f.apply c i))
  (Hf :  (c : 0) (i : ) (hi : i  m+1) (x : M.X (k * c) i),
    (M.res x : M.X c i)  k * f.apply (k*c) i x)
  (hg :  c i, (g.apply c i).ker = (f.apply c i).range)
  (hgsur :  c i, function.surjective (g.apply c i))
  (hN :  c i x, g.apply c i x  x)
  -- jmc: Is this ↑↑ the correct way of saying "`N` has the quotient norm"?
  (hM : M.is_bdd_exact_for_bdd_degree_above_idx k m c₀)
  (hM' : M'.is_bdd_exact_for_bdd_degree_above_idx k m c₀)
  (hM_adm : M.admissible)
  (hM'_adm : M'.admissible)
  (k_new : 0) [fact (1  k_new)] (hk : k_new = k^3 + k) :
  N.is_bdd_exact_for_bdd_degree_above_idx k_new (m-1) c₀

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 14:05):

Mmm, we should really have a definition of the "quotient norm".
For me, it is the following: let YXY \subseteq X be an inclusion in some category equipped with quotients and a norm and let π ⁣:XX/Y\pi \colon X \to X/Y be the projection. Then π(x)=infyY{x+y}||\pi(x)|| = \inf_{y \in Y}\{||x+y||\}, so for example trivially π(x)x||\pi(x)|| \leq ||x||.

Now, in the third line of the proof of Proposition 9.10 the authors say:

Then we can write mk3ci+1=fk3ci+1(mk3ci+1)+mk3ci+1m_{k^3c}'^{i+1} = f_{k^3c}^{i+1}(m_{k^3c}^{i+1}) + m_{k^3c}''^{i+1} with mk3ci+1Mk3ci+1nk3ci+1Nk3ci+1||m_{k^3c}''^{i+1}||_{M_{k^3c}'^{i+1}} \leq ||n_{k^3c}^{i+1}||_{N_{k^3c}^{i+1}}.

Here Nk3ci+1N_{k^3c}^{i+1} is the quotient by the image of fk3ci+1f_{k^3c}^{i+1} and the projection of mk3ci+1m_{k^3c}'^{i+1} is nk3ci+1n_{k^3c}^{i+1} by definition. In particular we also have π(mk3ci+1)=nk3ci+1\pi(m_{k^3c}''^{i+1}) = n_{k^3c}^{i+1}, so mk3ci+1Mk3ci+1=nk3ci+1Nk3ci+1||m_{k^3c}''^{i+1}||_{M_{k^3c}'^{i+1}} = ||n_{k^3c}^{i+1}||_{N_{k^3c}^{i+1}} and in practice this means that the inf\inf in the definition of the quotient norm is a min\min, attained at mk3ci+1m_{k^3c}''^{i+1}.

I know that for classical Banach spaces this is not true (even if the subspace is closed). Am I missing something trivial?

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

Hmm, so apriori it looks like the quotient norm gives the inequality in the other direction.

view this post on Zulip Adam Topaz (Jan 21 2021 at 14:17):

By quotient norm you mean you take the inf of the norms of the elements in the preimage of π(x)\pi(x), righht?

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 14:17):

Yep, by definition we get that the quotient norm is smaller than something, rather then bigger

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 14:17):

@Adam Topaz Yes, that's what I mean

view this post on Zulip Adam Topaz (Jan 21 2021 at 14:19):

And if IIRC, the "correct" category is separated normed abelian groups?

view this post on Zulip Adam Topaz (Jan 21 2021 at 14:19):

Just trying to orient myself (I just woke up)

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 14:22):

I am not sure if separateness is required, but in any case what I wrote above stays true

view this post on Zulip Peter Scholze (Jan 21 2021 at 14:23):

You are right, Riccardo, we need to slightly weaken that inequality, and allow some small increase in norm

view this post on Zulip Peter Scholze (Jan 21 2021 at 14:26):

But I think we can just take the infimum again at the end, so I think the lemma should stay true as stated

view this post on Zulip Peter Scholze (Jan 21 2021 at 14:31):

I should maybe also say that in the generality of this lemma (and conceivably in the relevant generality) it may happen that the NN's are nonseparated, in which case the infimum need not be attained.

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 14:34):

Thank you, I will replace CC by C+εC + \varepsilon, that makes this part of the proof OK, and I will take the infimum at the end.

view this post on Zulip Adam Topaz (Jan 21 2021 at 14:52):

@Riccardo Brasca Are you formalizing the proof?

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 14:55):

I just started... new version of the statement (including the quotient norm and the very beginning of the proof)

/-- The normed snake lemma. See Proposition 9.10 from Analytic.pdf -/
lemma normed_snake (k : 0) (m : ) (c₀ : 0) [fact (1  k)]
  (hf :  c i, normed_group_hom.is_strict (f.apply c i))
  (Hf :  (c : 0) (i : ) (hi : i  m+1) (x : M.X (k * c) i),
    (M.res x : M.X c i)  k * f.apply (k*c) i x)
  (hg :  c i, (g.apply c i).ker = (f.apply c i).range)
  (hgsur :  c i, function.surjective (g.apply c i))
  (hN :  c i x, g.apply c i x = Inf {r :  |  y  (f.apply c i).range, r = x + y })
  -- jmc: Is this ↑↑ the correct way of saying "`N` has the quotient norm"?
  (hM : M.is_bdd_exact_for_bdd_degree_above_idx k m c₀)
  (hM' : M'.is_bdd_exact_for_bdd_degree_above_idx k m c₀)
  (hM_adm : M.admissible)
  (hM'_adm : M'.admissible)
  (k_new : 0) [fact (1  k_new)] (hk : k_new = k^3 + k) :
  N.is_bdd_exact_for_bdd_degree_above_idx k_new (m-1) c₀ :=
begin
  intros c hc i hi n,
  let n₁ := N.d n,
  obtain m', hm' := hgsur (k_new * c) (i + 1) n,
  let m₁' := M'.d m',
  let C := n₁,
  sorry
end

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:00):

There was some talk of live streaming? ;)

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:02):

Is there a good reason to introduce k_new separately?

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:02):

I am redoing the proof on pen and paper right now, but very carefully :)

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:03):

Perhaps you should push the corrected statement of the theorem?

view this post on Zulip Johan Commelin (Jan 21 2021 at 15:04):

Adam Topaz said:

Is there a good reason to introduce k_new separately?

Maybe not. But it helps with the [fact].

view this post on Zulip Johan Commelin (Jan 21 2021 at 15:05):

I guess we should just teach lean that powers and sums of reals bigger than 1 are also bigger than 1.

view this post on Zulip Johan Commelin (Jan 21 2021 at 15:05):

But I was in a hurry when I wrote the first version of that statement.

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:05):

Sure, I guess we need

instance {k : 0} [fact (1  k)] : fact (1  k^3 + k) := sorry

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:07):

This works:

instance {k : 0} [h : fact (1  k)] : fact (1  k^3 + k) := le_trans h $ by simp

view this post on Zulip Johan Commelin (Jan 21 2021 at 15:10):

But more generally, we could provide two instances: one for k^n and one for k + k'.

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:14):

Okay, here's a quick sketch for that:

instance one_le_add {a b : 0} [ha : fact (1  a)] [hb : fact (1  b)] : fact (1  a + b) := le_trans ha $ by simp

instance one_le_pow {n : } {a : 0} [h : fact (1  a)] : fact (1  a^n) :=
begin
  induction n with n hn,
  { simp [le_refl] },
  { change 1  a * a^n,
    have : 1 * a^n  a * a^n, by exact mul_le_mul_right' h (a ^ n),
    rw [one_mul] at this,
    refine le_trans hn this }
end

example {k : 0} [h : fact (1  k)] : fact (1  k^3 + k) := by apply_instance

view this post on Zulip Johan Commelin (Jan 21 2021 at 15:15):

Is one_le_pow not yet in mathlib? :shock: Anyway, please add these to facts.lean

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:16):

will do.

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:17):

Johan Commelin said:

Is one_le_pow not yet in mathlib? :shock: Anyway, please add these to facts.lean

I didn't check.... I probably should :)

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

Ah okay, I can use this: docs#one_le_pow_iff

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:20):

Oh, but that has an annoying assumption that nis nonzero... (which is used for the implication that we don't need.)

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:21):

If you are also modifying the statement I don't if using Inf as I did is the more convenient way of stating that property (I've never used Inf)

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:21):

@Riccardo Brasca I was going to avoid modifying the file, since I didn't want to cause a merging nightmare for you.

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:22):

I am working on a copy :)

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:26):

@Riccardo Brasca My copy of the repo doesn't like (f.apply c i).range.

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:27):

I've added

/-- The image of a bounded group homomorphism. Naturally endowed with a `normed_group` instance. -/
def range : add_subgroup V₂ := f.to_add_monoid_hom.range

In src/for_mathlib/normed_group_hom.lean

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:27):

One should probably add the other properties, as for the kernel

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:27):

Sure.

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:28):

Well, let me push my changes to facts.lean. After that, I suggest changing the statement of the normed snake lemma to the following:

/-- The normed snake lemma. See Proposition 9.10 from Analytic.pdf -/
lemma normed_snake (k : 0) (m : ) (c₀ : 0) [fact (1  k)]
  (hf :  c i, normed_group_hom.is_strict (f.apply c i))
  (Hf :  (c : 0) (i : ) (hi : i  m+1) (x : M.X (k * c) i),
    (M.res x : M.X c i)  k * f.apply (k*c) i x)
  (hg :  c i, (g.apply c i).ker = (f.apply c i).range)
  (hgsur :  c i, function.surjective (g.apply c i))
  (hN :  c i x, g.apply c i x = Inf {r :  |  y  (f.apply c i).range, r = x + y })
  -- jmc: Is this ↑↑ the correct way of saying "`N` has the quotient norm"?
  (hM : M.is_bdd_exact_for_bdd_degree_above_idx k m c₀)
  (hM' : M'.is_bdd_exact_for_bdd_degree_above_idx k m c₀)
  (hM_adm : M.admissible)
  (hM'_adm : M'.admissible) :
  --(k_new : ℝ≥0) [fact (1 ≤ k_new)] (hk : k_new = k^3 + k) :
  N.is_bdd_exact_for_bdd_degree_above_idx (k^3 + k) (m-1) c₀ :=
sorry

view this post on Zulip Adam Topaz (Jan 21 2021 at 15:29):

pushed.

view this post on Zulip Johan Commelin (Jan 21 2021 at 15:29):

@Riccardo Brasca can you push what you have? If you don't want to push to master, feel free to create snake :wink: :snake:

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:33):

Let me figure out how to do it (no help needed, sooner or later I have to learn how to do such things)

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:37):

I guess I need an invitation, or something like that (I can also use my repository if you prefer)

view this post on Zulip Johan Commelin (Jan 21 2021 at 15:41):

ooh, sorry... I'll send you an invite

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:41):

I am riccardobrasca on GitHub

view this post on Zulip Johan Commelin (Jan 21 2021 at 15:42):

invitation sent

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 15:44):

Pushed to branch snake

view this post on Zulip Adam Topaz (Jan 21 2021 at 16:04):

@Riccardo Brasca FWIW, regarding using Inf, my limited experience with it is that the api for Inf is very pleasant to use.

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 16:05):

Good to know!

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 16:06):

I finished checking the proof with pen and paper and I am confident that there will be no surprises, it's a lot of clever diagram chasing, but it is completely explicit

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 16:07):

At the end we need that if ab+εa \leq b + \varepsilon for all ε<0\varepsilon < 0 then aba \leq b. I don't know if this is in mathlib, but it is unrelated to the proof

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:15):

docs#le_of_forall_le_of_dense ?

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:17):

or even closer, docs#le_of_forall_pos_le_add

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 16:18):

@Heather Macbeth perfect, thank's!

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 16:18):

I have to do other things now, but I will resume working on this in a few hours

view this post on Zulip Adam Topaz (Jan 21 2021 at 16:43):

If I understand the discussion above correctly, I think this is at least a start toward the proof (building on @Riccardo Brasca 's code):

LONG

view this post on Zulip Adam Topaz (Jan 21 2021 at 16:44):

This has a lot of duplicate code that can be moved outside the proof...

view this post on Zulip Adam Topaz (Jan 21 2021 at 16:44):

And the first sorry seems like it it should use something from mathlib (which I could'nt find). Actually, the whole proof after the "suffices" block should follow easily from some stuff that should be in mathlib.

view this post on Zulip Adam Topaz (Jan 21 2021 at 16:53):

It's possible the order of quantifiers is wrong in the suffices statement.

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 16:54):

It seems good to me

view this post on Zulip Adam Topaz (Jan 21 2021 at 16:54):

Okay great :)

view this post on Zulip Adam Topaz (Jan 21 2021 at 16:54):

I mean it was not clear to me how the proof would work with the quantifiers the other way around...

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 17:13):

The proof of the suffices statement should be an immediate consequence of le_of_forall_pos_le_add, but Lean is not happy about it:

unknown identifier 'le_of_forall_pos_le_add'

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 17:14):

le_of_forall_pos_le_add' is in algebra.ordered_group in mathlib, but not in the file algebra.ordered_group of the project

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 17:21):

If I modify that file to include le_of_forall_pos_le_add' then I get excessive memory consumption detected at 'replace' everywhere :dizzy:

view this post on Zulip Adam Topaz (Jan 21 2021 at 17:23):

Yeah I ran into the same issue with le_of_forall_pos_le_add not found. Maybe we need to bump mathlib?

view this post on Zulip Adam Topaz (Jan 21 2021 at 17:24):

Trying to update mathlib now...

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 17:24):

I see that you put mathlib in _target/... that makes clear to me you did something I don't understand :sweat_smile:

view this post on Zulip Adam Topaz (Jan 21 2021 at 17:25):

Okay, that worked. I'll finish off that first sorry

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 17:31):

How can I update mathlib?

view this post on Zulip Adam Topaz (Jan 21 2021 at 17:35):

I used leanproject upgrade-mathlib

view this post on Zulip Adam Topaz (Jan 21 2021 at 17:41):

@Riccardo Brasca This is a mess....

LONG

view this post on Zulip Adam Topaz (Jan 21 2021 at 17:42):

I pushed to the branch AT-snake in case you want access to the code.

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 17:53):

Mmm... I think that the epsilon is in the part with the norm, not in the parti with k

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 17:53):

∥ N.res n - N.d y ∥ ≤ k_new * (∥ N.d n ∥+ ε)

view this post on Zulip Adam Topaz (Jan 21 2021 at 17:55):

Ah right.

view this post on Zulip Adam Topaz (Jan 21 2021 at 17:57):

Let me fix that. one sec.

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

Okay, I fixed the statement and cleaned it up significantlyy.

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

https://github.com/leanprover-community/lean-liquid/blob/a1e2f37c01b35849b90072e09a29443ed0ae0dea/src/normed_snake.lean#L50

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 18:09):

Given ε, assuming ∥ N.res n - N.d y ∥ ≤ k_new * (∥ N.d n ∥+ ε1) for all ε1, why doesn't apply it for ε1= ε/ k_new?

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 18:09):

I mean, there are of course problems with 0≤... but mathematically that's what I would do

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 18:11):

OK, that's what you did, sorry

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 18:38):

Wait a minute... maybe you were right and the order of the quantifier should be reversed (and I agree that then the proof is not clear)

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 18:49):

I mean, all the elements constructed in the third line of the proof depend on ε\varepsilon so also all the others depend on it

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

Yeah exactly. This is what I was worried about.

view this post on Zulip Adam Topaz (Jan 21 2021 at 19:01):

I think the order of the quantifiers can probably be reversed if one assumes completeness, because then for each epsilon you would get an element and eventually have to prove that those elements converge (I don't know if the details would actually work out).

view this post on Zulip Riccardo Brasca (Jan 21 2021 at 19:03):

I was thinking to it, but I am really sure this doesn't work for making the inf\inf in the definition of the quotient norm a min\min. Of course it can still work for our elements for some reasons but still, something has to be done

view this post on Zulip Peter Scholze (Jan 21 2021 at 22:54):

Ah!

view this post on Zulip Peter Scholze (Jan 21 2021 at 22:54):

Sorry, indeed you caught something there. Let me think about this.

view this post on Zulip Peter Scholze (Jan 21 2021 at 22:55):

One option might be to change the meaning of k\leq k-exactness, to also include an inf

view this post on Zulip Peter Scholze (Jan 21 2021 at 22:59):

Hmm. It should be possible to fix this by a small tweaking of some definition, but let me try to figure out a good global fix to this. I'll keep you posted.

view this post on Zulip Peter Scholze (Jan 21 2021 at 23:50):

Probably this is just my mind making up a solution as I want to go to bed, but I think the following fix ought to work. Leave all the statements and definitions essentially unchanged, but replace all normed abelian groups with complete normed abelian groups. In particular, in 9.10, the quotient N=M/MN=M'/M is implicitly completed. Then I think 9.10 stays true as stated, except that one may have to replace k3+kk^3+k by something slightly different.

view this post on Zulip Peter Scholze (Jan 21 2021 at 23:51):

I'll try to update the file tomorrow

view this post on Zulip Sebastien Gouezel (Jan 22 2021 at 08:02):

I haven't followed the discussion closely, but let me still mention this: even in the setting of real Banach spaces and closed subspaces, the quotient norm is not always realized. I.e., there exists a closed hyperplane of c_0, say (the space of sequences tending to 0 with its sup norm) and a closed hyperplane H such that a point in c_0 / H of norm 1 has no preimage of norm 1 in c_0. Take H the kernel of the linear form (xn)2nxn(x_n) \mapsto \sum 2^{-n} x_n, for instance.

view this post on Zulip Sebastien Gouezel (Jan 22 2021 at 08:04):

Equivalently, points in c_0 but not in H don't have any distance-minimizing projection on H (because the would-be projection would be in \ell^\infty, but not in c_0).

view this post on Zulip Peter Scholze (Jan 22 2021 at 09:53):

OK, the fix still seems to work this morning. See the updated version of www.math.uni-bonn.de/people/scholze/Analytic.pdf

view this post on Zulip Johan Commelin (Jan 22 2021 at 09:55):

@Peter Scholze great! so you only changed 9.10, right?

view this post on Zulip Johan Commelin (Jan 22 2021 at 09:56):

Because you considered changing the def of k\le k-exactness, but it looks like that wasn't necessary?

view this post on Zulip Peter Scholze (Jan 22 2021 at 09:58):

Yes, I only changed 9.10 (and added the word "complete" in 9.6)

view this post on Zulip Peter Scholze (Jan 22 2021 at 10:05):

(If I had to change the definition of k\leq k-exactness, to include some infimum basically, the implication 9.4 --> 9.1 wouldn't have been obvious anymore. I'm glad it worked this way now! Let's see what other problems will come up...)

view this post on Zulip Riccardo Brasca (Jan 22 2021 at 11:47):

Very nice! I see that the statement is now a little less elementary: we should probably think about how to say in Lean that we take the quotient by the closure of the image of ff.

view this post on Zulip Adam Topaz (Jan 22 2021 at 13:45):

So it sounds like we should introduce the category CompleteNormedGroup?

view this post on Zulip Johan Commelin (Jan 22 2021 at 13:47):

Can't we just add [complete_space M] etc...?

view this post on Zulip Riccardo Brasca (Jan 22 2021 at 13:48):

In src/locally_constant/Vhat.lean there is already a lot of stuff

view this post on Zulip Johan Commelin (Jan 22 2021 at 13:48):

My guess is that it will be easier if we try to stay in one category.

view this post on Zulip Riccardo Brasca (Jan 22 2021 at 13:50):

Maybe we should add complete_system_of_complexes or something like that (we can also assume completeness for all objects)

view this post on Zulip Johan Commelin (Jan 22 2021 at 14:02):

Sure, we could extend system_of_complexes to a new structure that includes [\forall X, complete_space X] as a field.

view this post on Zulip Peter Scholze (Jan 23 2021 at 09:45):

Peter Scholze said:

(If I had to change the definition of k\leq k-exactness, to include some infimum basically, the implication 9.4 --> 9.1 wouldn't have been obvious anymore. I'm glad it worked this way now! Let's see what other problems will come up...)

Thinking more about this, that fix would work as well: i.e., in the definition of k\leq k-exactness, weaken the condition to say that for all ϵ>0\epsilon>0, one can find blah such that some inequality holds, where now the right-hand side contains a +ϵ+\epsilon. With this modification, I think all of 9.4 (and 9.6, 9.10 etc) should stay true as originally stated (so without completeness), but all of the proofs would now (necessarily) include some extra quantification over ϵ\epsilon's.

On the other hand, one can prove that this weakened of k\leq k-exactness holds for a system of complexes of normed abelian groups if and only if it holds for its completion, and that if this weakened notion holds for a system of complexes of complete normed abelian groups, then the strong version holds, up to replacing kk by k2+1k^2+1 or so. In this sense, the statements with the weak notion of k\leq k-exactness, stated without completeness hypothesis, and the statements with strong notion of k\leq k-exactness, stated with completeness hypothesis, are equivalent (up to slightly changing kk). It is not clear to me which one is easier to formalize; maybe there's not much difference?

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 13:12):

In my opinion proposition 9.10 with the +ε + \varepsilon-definition of k\leq k-exactness should be easy to formalize, I try doing it today. I don't know for the implication for complete spaces, but, at least in mathlib, we usually prefer cutting proofs in small pieces and stating explicitly all lemmas we use in the proofs, so my preferences is for this new approach.

view this post on Zulip Adam Topaz (Jan 23 2021 at 14:47):

I would be inclined to use complete normed groups. If we change the definition of k\le k exactness this then changes the statement of the "main" theorem in the repo, and some additional work would be required to prove the equivalence with the original definition for complete normed groups. On the other hand, it's possible we will have to do that additional work anyway...

For what it's worth, we at least have the universal property of completion already in the repo, so my guess is changing the snake lemma to assume completeness would be (slightly) less work.

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 14:52):

I mean something like defining defining is_weak_bdd_exact_for_bdd_degree_above_idx using the ε\varepsilon, proving proposition 9.10 with this one (I am sure it works without troubles) and proving that for complete things is_weak_bdd_exact_for_bdd_degree_above_idx implies is_bdd_exact_for_bdd_degree_above_idx, with a slightly different bound.

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 14:52):

But of course no problem if you think it is better have completed normed groups everywhere

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 19:24):

If someone is interested I have uploaded here https://github.com/leanprover-community/lean-liquid/blob/snake/src/normed_snake.lean some progress to prove the weakened statement that uses is_weak_bdd_exact_for_bdd_degree_above_idx.

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 19:25):

It's rather messy and I put some stupid lemmas before Proposition 9.10 that should be somewhere else, but it really seems that this weakened version poses no trouble

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:40):

@Riccardo Brasca nice work, I'm looking at it now

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:40):

at some point you suggested introducing def is_quotient, and I think this is a good idea.

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 19:43):

Some remark if you really want to read it:
I see that Peter has already updated the file on his website, I am following the following version
image.png

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 19:44):

The proof stops at the formula before "where similarly mk3ci+2m_{k^3c}''^{i+2} is the differential of..."

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 19:45):

Yes, I think introducing is_quotient will be useful in any case. I think we will the lemma quotient, whose proof can for surely be golfed a lot.

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:48):

so now snake assumes the strong exactness condition, and the result gives the weak version. Should we make the assumptions weak as well?

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 19:53):

Ah, you're right, this is probably harmless. In any case if we really use weak... at some point we need to prove that this implies the non weak version for complete groups

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 19:54):

Also I have the impression that Hf should hold with (hi : i ≤ m + 2) since all our indexes are shifted, but maybe I am lost with all the notation

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:55):

I pushed to your branch: the easy lemma that strong exactness implies weak exactness

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:56):

Riccardo Brasca said:

Also I have the impression that Hf should hold with (hi : i ≤ m + 2) since all our indexes are shifted, but maybe I am lost with all the notation

Ooh, that's a good point. We shouldn't forget about that

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 19:57):

Now I think it's OK :upside_down:

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 20:19):

It's probably better to have let c_new := k * (k * (k * c)), to apply Hf without having to use system_of_complexes.congr a lot

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 21:08):

I've added the inequality before "On the other hand...". It's becoming a little slow... maybe I will try to cut the proof in pieces

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 22:01):

Sometimes slowness can be the fault of just one tactic. Can you push and show me where it's slow? I can try and see if I can see what is making it slow. Trying to write code when you have to wait 5 seconds after every line is not fun

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 22:15):

It's here https://github.com/leanprover-community/lean-liquid/blob/snake/src/normed_snake.lean
Note that I use some other definition in the branch snake.
In any case the code is 1) not that slow, it is still usable 2) very messy and probably difficult to follow

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 22:45):

I am stopping working on it for today. If someone is interested feel free to continue, the end is not that far, but the rest of the work is not that interesting, it's a matter of not getting lost with all the variables and assumptions.

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 23:10):

I'm filling in some sorries

view this post on Zulip Riccardo Brasca (Jan 23 2021 at 23:13):

It's very possible that there is a coherent and clever way of killing a lot of the stupid inequalities I need, I din't really thought about it

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 23:13):

I'm just methodically killing them in dull ways

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 23:17):

You can use haveI instead of letI for Props, and it's sometimes easier to use set a := blah with ha than let a := blah because then you can rw ha to replace a by blah rather than just relying on the fact that they are defeq.

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 23:21):

i killed a few but now I have to stop too

view this post on Zulip Alex J. Best (Jan 24 2021 at 03:53):

I believe I made some progress (though I haven't followed the maths I thought it would be fun to have a go) I changed one sorry for the fact that N is admissible (which is mentioned in the theorem statement), if this looks good and you don't mind giving me push access I'll push it :smile:

diff --git a/src/normed_snake.lean b/src/normed_snake.lean
index cbfac16..401e9e5 100644
--- a/src/normed_snake.lean
+++ b/src/normed_snake.lean
@@ -91,7 +91,7 @@ begin
     rw add_mul,
     convert (le_add_iff_nonneg_right (k^3 * c)).2 (zero_le') using 1,
     ring },
-  let n := @system_of_complexes.res _ _ c_new _ _ norig,
+  set n := @system_of_complexes.res _ _ c_new _ _ norig with hn,
   set n₁ := N.d n with hn₁,
   let C := ∥n₁∥,
   haveI : fact (c ≤ c_new) := by
@@ -100,7 +100,21 @@ begin
     refine le_trans _ (le_mul_of_one_le_left' hk),
     refine le_trans (le_refl _) (le_mul_of_one_le_left' hk) },
   suffices hnorig : ∃ (y : (N.X c i)), ∥(N.res) n - (N.d) y∥ ≤ (k ^ 3 + k) * C + ε,
-  { sorry },
+  { refine Exists.imp _ hnorig,
+    rintro a ha,
+    simp only [system_of_complexes.res_res] at ha,
+    calc _ ≤ _ : ha
+       ... ≤ _ : _,
+    simp only [C, hn₁, hn, nnreal.coe_add, add_le_add_iff_right, nnreal.coe_pow],
+    apply mul_le_mul_of_nonneg_left,
+    { rw system_of_complexes.d_res,
+      have hN_adm : N.admissible :=
+      begin
+        sorry,
+      end,
+      convert hN_adm.res_norm_noninc _ _ _ _ (N.d norig),
+      simp, },
+    { exact_mod_cast (nnreal.coe_nonneg (k^3 + k)), }, },
   obtain ⟨m', hm'⟩ := hgsur _ _ n,
   let m₁' := M'.d m',
   have hm₁' : g.apply _ _ m₁' = n₁,

view this post on Zulip Riccardo Brasca (Jan 24 2021 at 10:07):

Thank you! Writing a small API to deal with quotients is in my TODO list, this result should definitely be there

view this post on Zulip Damiano Testa (Jan 25 2021 at 09:48):

Dear All,

having finally pushed out of my queue some chores that I had left, I am very interested in joining this project!

I get the impression that you have been working on a branch called snake: is it ok if I also take a look?

Thanks!

view this post on Zulip Johan Commelin (Jan 25 2021 at 09:53):

@Damiano Testa certainly!

view this post on Zulip Johan Commelin (Jan 25 2021 at 09:53):

the snake branch is devoted to proving the "normed snake lemma"

view this post on Zulip Johan Commelin (Jan 25 2021 at 09:53):

but feel free to also look at the other sorrys

view this post on Zulip Johan Commelin (Jan 25 2021 at 09:53):

I'll send you an invite for the repo

view this post on Zulip Damiano Testa (Jan 25 2021 at 09:54):

Ok, I will look through the various files, not just in the snake branch! Thanks!

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 10:15):

Hi! I am working on the proof of the snake lemma right now (I don't know if we are going to keep this version at end, but this is going to be useful anyway I think). There are something like 15 variables and assumptions so it is probably not reasonable for someone else to read it (and moreover it is not that fun...). If you are looking for something easy to do, in the file normed_snake.lean of the sneak branch there are two lemmas, commutes and commutes_res that are easy and that should be moved somewhere else (and with better names...). commutes_res moreover doesn't have a proof :grinning:

view this post on Zulip Johan Commelin (Jan 25 2021 at 10:18):

sounds like d_apply and res_apply (-; and the can probably go after the defn of apply.

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 10:30):

@Damiano Testa If you do it, can you please not touch normed_snake.lean? Just to make my git happy... I will erase them from there once they are somewhere else

view this post on Zulip Adam Topaz (Jan 25 2021 at 14:59):

@Riccardo Brasca I filled in a simple sorry in your branch. Are you happy for me to push to your branch on github?

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:01):

Go ahead! In five minutes I will push a semicomplete proof

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:01):

(after merging what you have done)

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:01):

semicomplete = the sorrys are unrelated to the snake lemma

view this post on Zulip Adam Topaz (Jan 25 2021 at 15:02):

Okay, pushed.

view this post on Zulip Adam Topaz (Jan 25 2021 at 15:03):

I'll try to fill in the commutes_reslemma too whhile I'm at it.

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:08):

I just pushed the proof

view this post on Zulip Adam Topaz (Jan 25 2021 at 15:09):

Oh :)

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:11):

There are five sorry in the file:
commutes_res: easy (and should be somewhere else)
N.admissible: the quotient of admissible stuff is admissible. Easy I think, it should be in the API of quotients
hzerok, hε₁ and kccnew are very easy inequalities about reals numbers

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:12):

Of course the proof can probably be golfed a lot

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:12):

But at least this is a reality check that we able to handle similar things

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:14):

And in any case I just called the lemma weak_normed_snake, since it uses is_weak_bdd_exact_for_bdd_degree_above_idx

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:16):

Riccardo Brasca said:

I just pushed the proof

@Adam Topaz I meant the almost complete proof of weak_normed_snake. commute_res is still a sorry.

view this post on Zulip Adam Topaz (Jan 25 2021 at 15:20):

Gotcha. I'm filling in the sorrys in the main proof now.

view this post on Zulip Kevin Buzzard (Jan 25 2021 at 15:22):

@Johan Commelin this is really interesting. Riccardo started things off (obviously building on your work), and then people have just been dropping in and filling in sorrys (me, Alex, Adam at least). What else is ready for this kind of game?

view this post on Zulip Johan Commelin (Jan 25 2021 at 15:23):

9.7

view this post on Zulip Johan Commelin (Jan 25 2021 at 15:23):

I'm working on the statement of 9.8

view this post on Zulip Johan Commelin (Jan 25 2021 at 15:23):

And people can start looking at the statement of 9.6

view this post on Zulip Johan Commelin (Jan 25 2021 at 15:24):

now that snake is almost ready

view this post on Zulip Johan Commelin (Jan 25 2021 at 15:24):

we'll need double complexes for that

view this post on Zulip Johan Commelin (Jan 25 2021 at 15:24):

so copy-paste the file on system_of_complexes, and make suitable modifications

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:32):

@Adam Topaz It is probably more convenient to replace hzerok by (0 : ℝ) < ↑k ^ 3 + 2 * ↑k + 1, so hε₁ should be immediate, and using ne_of_lt hzerok (or whatever is needed) at the end

view this post on Zulip Adam Topaz (Jan 25 2021 at 15:35):

Okay, I killed the easy sorrys in the proof.

view this post on Zulip Adam Topaz (Jan 25 2021 at 15:37):

The admissibility is the only sorry left in the main proof. I also didn't do commute_res.

view this post on Zulip Adam Topaz (Jan 25 2021 at 15:37):

Unfortunately, that's all the time I have for now.

view this post on Zulip Adam Topaz (Jan 25 2021 at 15:42):

Kevin Buzzard said:

Johan Commelin this is really interesting. Riccardo started things off (obviously building on your work), and then people have just been dropping in and filling in sorrys (me, Alex, Adam at least). What else is ready for this kind of game?

When will GPT2 be able to play this kind of game? :)

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 15:53):

I also have to stop :(
For the quotient, do you think that's better having an instance [is_quotient] or a normal assumption?

view this post on Zulip Johan Commelin (Jan 25 2021 at 18:59):

@Riccardo Brasca do you think it would already be a good time to merge everything into master? or would you rather finish all the sorrys first?

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 19:16):

I think we should at least move the lemmas about the composition of a morphism with d and res, with a reasonable name. They have nothing to do in that file

view this post on Zulip Johan Commelin (Jan 25 2021 at 19:16):

ok, sure

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 19:17):

BTW I have slightly reorganized the proof, now the easy inequalities are all at the beginning of the proof. If someone want to improve them they are there :)

view this post on Zulip Johan Commelin (Jan 25 2021 at 19:19):

I think it would be good to move things (roughly) into place, and merge into master. That would make it easier to keep the total overview.

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 19:29):

I can do it... hoping to not destroy everything changing/merging branch...

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 19:30):

If you prefer I can modify snake and let you do the merge into master

view this post on Zulip Johan Commelin (Jan 25 2021 at 19:31):

whatever you like best

view this post on Zulip Johan Commelin (Jan 25 2021 at 19:31):

In principle git should allow us to fix anything we break

view this post on Zulip Alex J. Best (Jan 25 2021 at 19:38):

Johan Commelin said:

so copy-paste the file on system_of_complexes, and make suitable modifications

I had a go at this last night in fact, I've now pushed it to https://github.com/leanprover-community/lean-liquid/blob/master/src/system_of_double_complexes.lean there was one key lemma I couldn't prove due to not being familiar enough with mathlibs category/homological machinery, d_comp_res for the vertical differential, due to the setup of double complexes as chain complexes of chain complexes there is a break in the symmetry which made one proof harder than the other for me. If someone wants to have a go at that, that would be great, I'm sure the proof is a 1-liner I just can't find the right way to fit the pieces together myself.

view this post on Zulip Johan Commelin (Jan 25 2021 at 19:43):

Thanks!

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 19:53):

I tried to put

variables {M M' N : system_of_complexes.{u}} (f : M  M') (g : M'  N)

def category_theory.has_hom.hom.apply (f : M  N) (c : 0) (i : ) :=
(f.app (op c)).f i

variables (M M' N)

lemma d_apply (f : M  N) {c : 0} {i : } (m : M.X c i) :
  N.d (f.apply c i m) = f.apply c (i + 1) (M.d m) :=
begin
  have h : ((M.obj (op c)).d i  (f.app (op c)).f (i + 1)) m =
    (f.app (op c)).f (i + 1) ((M.obj (op c)).d i m),
  { exact coe_comp ((M.obj (op c)).d i) ((f.app (op c)).f (i + 1)) m },
  rwa [homological_complex.comm_at (f.app (op c)) i] at h,
end

lemma res_apply (f : M  N) (c c' : 0) [h : fact (c  c')] {i : } (m : M.X c' i) :
  @system_of_complexes.res N c' c _ _ (f.apply c' i m) =
  f.apply c i (@system_of_complexes.res M c' c _ _ m) :=
begin
  sorry
end

inside src/system_of_complexes.lean, but Lean is not happy with N.d and f.apply, and I don't understand why... :thinking:

view this post on Zulip Alex J. Best (Jan 25 2021 at 19:57):

Did you paste it into the system_of_complexes namespace or after?

view this post on Zulip Alex J. Best (Jan 25 2021 at 19:57):

I think the category def would have to be outside that namespace at least

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 20:00):

Thank you, now it works

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 20:17):

@Johan Commelin I just pushed to snake a reorganization of some definition

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 20:18):

Now d_apply and res_apply are in src/system_of_complexes.lean, where there is also a quotientsection with the two results I used (we have to write the definition explicitely)

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 20:20):

I also moved normed_group_hom.is_strict and is_strict.injective to src/for_mathlib/normed_group_hom.lean, so in practice in normed_snake.lean there is just the snake lemma

view this post on Zulip Johan Commelin (Jan 25 2021 at 20:22):

lgtm

view this post on Zulip Johan Commelin (Jan 25 2021 at 20:23):

let's merge it into master

view this post on Zulip Johan Commelin (Jan 25 2021 at 20:23):

any other fixes can be done afterwards

view this post on Zulip Johan Commelin (Jan 25 2021 at 20:23):

merged, pushed

view this post on Zulip Johan Commelin (Jan 25 2021 at 20:25):

@Riccardo Brasca thanks for all the great work!

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 20:29):

It was my pleasure... and this is just the beginning! :)

view this post on Zulip Johan Commelin (Jan 25 2021 at 20:54):

Alex J. Best said:

there was one key lemma I couldn't prove due to not being familiar enough with mathlibs category/homological machinery, d_comp_res for the vertical differential, due to the setup of double complexes as chain complexes of chain complexes there is a break in the symmetry which made one proof harder than the other for me. If someone wants to have a go at that, that would be great, I'm sure the proof is a 1-liner I just can't find the right way to fit the pieces together myself.

done

view this post on Zulip Johan Commelin (Jan 25 2021 at 20:58):

So, to summarise what's left with regards to the snake lemma:

  • define is_quotient, and use it
  • a sorry about admissibility
  • prove that weak exactness is the same as strong exactness, in the complete case
  • derive the strong snake lemma for complete systems from the weak version.

view this post on Zulip Johan Commelin (Jan 25 2021 at 20:58):

@Riccardo Brasca please correct :up: if I got something wrong or missed something

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 20:59):

except that you probably mean complete instead of compact I agree

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 21:00):

The first two points are not difficult I think (the first one is just to write a definition as a def, and the second one seems immediate)

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 21:02):

Ah, concerning completions we will need that it preserves all the assumptions in the weak snake lemma (for example admissibility, strictness...)

view this post on Zulip Johan Commelin (Jan 25 2021 at 21:09):

res_apply is done

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 21:52):

Time to rest a bit for me. Tomorrow I have to prepare my teaching but if I have time and no one has already done it I will work on the definition and basic properties of quotients

view this post on Zulip Johan Commelin (Jan 25 2021 at 21:55):

I'm not sure we will even need a construction of the quotient... we'll have to see.

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 21:57):

I mean, write down the definition by hand, without any complicated property as stated in the snake lemma (to be able to put is_quotient g or similar) and prove that the quotient of an admissible thing is admissible

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:32):

I have created a new branch riccardobrasca where I just put the definition of quotient of systems of complexes and the proof that the quotient of an admissible system of complexes is admissible. I think it can be merged to master, but if someone wants to check it is better :)

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:32):

Note that I had to upgrade mathlib to use le_of_forall_pos_le_add

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:36):

Indeed CI is not happy with error: unknown identifier 'le_of_forall_pos_le_add'

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:36):

@Riccardo Brasca how did you upgrade mathlib?

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:36):

I don't see any changes to leanpkg.toml.

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:37):

The recommended way is leanproject up. This will change the toml for you.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:37):

leanproject upgrade-mathlib

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:37):

Does git status show you uncommitted changes?

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:38):

Yes, the toml file... I ignored it since I didn't know what it is

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:38):

I am pushing it

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:38):

Riccardo Brasca said:

Yes, the toml file... I ignored it since I didn't know what it is

It keeps track of which version of lean and mathlib you want to use :rofl:

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:40):

downloading the cache... with avg speeds of 318 kb/s :sad:

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:41):

('Connection broken: OSError("(104, \'ECONNRESET\')")', OSError("(104, 'ECONNRESET')"))

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:46):

@Riccardo Brasca lgtm. You already put it in the normed_group_hom namespace, right?
So we can use dot-notation and write (hf : f.is_quotient).

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:46):

Feel free to merge

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:48):

There are two is_quotient, the first one is normed_group_hom.is_quotientand the second one is system_of_complexes.is_quotient, with the obvious relation between the two.

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 12:49):

@Riccardo Brasca When working on mathlib directly, other people look after the toml for you. But when working on a different project which uses mathlib as a dependency it's really important that the project keeps track of exactly which commit of mathlib we are expecting the code to use. As mathlib moves on and makes no attempt at backwards compatibility, the contributors to the liquid project have to keep changing the toml manually and making sure that code which once compiled doesn't get broken. It's more of a juggling act than working on mathlib directly.

However we are lucky here that there are several people working on the liquid project who keep a careful eye on what is happening in mathlib and hopefully, if we keep "bumping" mathlib regularly (ie changing the toml so it points to today's mathlib) then any problems will be spotted quickly and fixed.

Nowadays we even have "continuous integration"which means that if a new change to mathlib breaks our project then people get notified quickly. This is a great improvement from back in the perfectoid days, when we would update mathlib once a month and discover that tons of things were broken and sometimes none of us knew why. This was bad for both the project and for mathlib, because we were writing code which should have been PRed to mathlib but we didn't get around to it, and any PR would of course break our code anyway.

It is for reasons like this that when someone comes along saying "can I do cyclotomic polynomials" we strongly encourage them to work on a mathlib branch directly, to avoid all these problems.

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 12:50):

downloading the cache... with avg speeds of 318 kb/s :sad:

When I was a post-doc we used to dream of such fast speeds, at least for our home internet.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:50):

@Kevin Buzzard Thank's for the explanation!

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 12:50):

When I was a PhD student we used to get 2400

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 12:54):

Merged into master, the proof of the weak snake lemma is now sorry free. Fun fact: there is no need of assuming that M is admissible (M'.admissible suffices).

view this post on Zulip Johan Commelin (Jan 26 2021 at 12:57):

Great job!

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:02):

Great!

view this post on Zulip Johan Commelin (Jan 26 2021 at 13:04):

@Peter Scholze I think you are interested in optimizing the constants, right? And this is one of the strengths of having a computer keep track of all the details. So that is certainly something I would like to support.

In that regard, it's better to work with weak exactness as long as possible, right?

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:09):

Yes, that's right

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:10):

In fact, in the implicit deduction of the real form of 9.4 (involving profinite SS) from the one you formalize (involving finite SS), one also implicitly goes back to the weak form and deduces the strong form

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:10):

So at this point one only really needs the weak form for finite SS, so you should optimize that

view this post on Zulip Johan Commelin (Jan 26 2021 at 13:10):

Ok, thanks for pointing that out

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:11):

If it's fine for you, I'll however keep the strong form in Analytic.pdf, as it's more readable (fewer ϵ\epsilon's floating around)

view this post on Zulip Johan Commelin (Jan 26 2021 at 13:11):

certainly

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:12):

In the normed snake lemma, both the hypothesis and the claim are now about the weak form, right?

view this post on Zulip Johan Commelin (Jan 26 2021 at 13:13):

yes, https://github.com/leanprover-community/lean-liquid/blob/master/src/normed_snake.lean#L13

view this post on Zulip Patrick Massot (Jan 26 2021 at 13:15):

I think it would be helpful to have more information about which constants you want to keep track of. And also whether keeping track is only knowing which constant depend on which constant or whether you are interested in actual formulas relating the different constants. I haven't looked closely at the lecture notes so feel free to ignore this comment if you think you already provided this information.

view this post on Zulip Johan Commelin (Jan 26 2021 at 13:16):

I think it's also about explicit bounds

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 13:16):

So there is no need of proving that weak exact implies exact for complete stuff? It shouldn't be difficult

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:16):

One does need that! But it might be just outside the scope of what you are trying to formalize right now

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:18):

@Patrick Massot Is Question 9.9 in www.math.uni-bonn.de/people/scholze/Analytic.pdf enough information? I'd like to understand how large the various things like kk (and NN, cc etc., in the proof of 9.5), have to be. The input variables are, I guess, rr, rr' and mm.

view this post on Zulip Patrick Massot (Jan 26 2021 at 13:18):

Riccardo Brasca said:

So there is no need of proving that weak exact implies exact for complete stuff? It shouldn't be difficult

This is probably a good sanity check in any case.

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:19):

I agree

view this post on Zulip Patrick Massot (Jan 26 2021 at 13:26):

Question 9.9 is probably not enough but combining with what you just wrote is better (having an explicit list of inputs and outputs). So possible answers could look like: "In Theorem 9.5, one can promise k is no larger than (r+r)exp(exp(m))(r + r')\exp(\exp(m))" or "There is some unknown universal constant C such that In Theorem 9.5, one can promise k is no larger than C(r+r)exp(exp(m))C(r + r')\exp(\exp(m))", right? (I'm inventing stupid formulas here, not claiming anything)

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:29):

Yes, that's what I have in mind. (Unfortunately, everything will also depend on the auxiliary constants c0,c1,c_0,c_1,\ldots that are "suitable" for the Breen-Deligne data. But Johan Commelin has an explicit example of such data, so one should be able to make these constants explicit as well, so one can get rid of this dependency.)

view this post on Zulip Patrick Massot (Jan 26 2021 at 13:37):

Ok, thanks for clarifying. This is typically something that will be much easier and safer with a formalization than on paper.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 13:55):

This must be my fault, but I just realized that I don't see how to prove (with pen and paper) that a complete system of complexes that is weakly k\leq k-exact is ?\leq ?-exact. This seemed easy yesterday, but now I am a little lost.

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:57):

Assume first that in this statement saying that for any xx there is some yy, you would also have some bound on y||y|| in terms of x||x||. Then I think it should follow by a direct Cauchy sequence argument.

view this post on Zulip Peter Scholze (Jan 26 2021 at 13:58):

Now you don't a priori have this bound, but if you replace kk by k2k^2 (to apply a deeper restriction), you can use weak exactness in one cohomological degree lower to change yy in order to achieve such a bound

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 14:01):

So do we need something like admissibility? In principle there are no bounds on the norm of the restriction

view this post on Zulip Peter Scholze (Jan 26 2021 at 14:02):

Sure, admissibility is always assumed

view this post on Zulip Peter Scholze (Jan 26 2021 at 15:11):

hmm, getting the bound on yy seems OK, but now I'm also confused about how to finish it off!

view this post on Zulip Peter Scholze (Jan 26 2021 at 15:19):

Hmm... maybe one has to prove 9.4 and 9.5 directly for profinite SS, which seems fine -- in the key lemma 9.8, one can indeed make the passage from finite SS to profinite SS by an application of Tychonoff. Let me check whether there is not a different way of getting the strong exactness after the fact. (Right now it seems to me that one has to carefully chase the strong exactness everywhere. Sorry for all the confusion!!)

view this post on Zulip Johan Commelin (Jan 26 2021 at 15:20):

No worries! You should blame Lean (-;

view this post on Zulip Peter Scholze (Jan 26 2021 at 15:21):

Of course this is exactly what I was hoping for!

view this post on Zulip Johan Commelin (Jan 26 2021 at 15:21):

But getting the statement of 9.4/9.5 for profinite S would require reworking Mbar a bit. That's fine. We would have to do that anyway if we aim for 9.1 as second_target.

view this post on Zulip Peter Scholze (Jan 26 2021 at 15:29):

hmm, I think one can deduce strong exactness from weak exactness in the complete case (more precisely, weak exactness for a system of complexes of non-complete groups implies strong exactness of the completion)... let me try to write the argument here

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 15:38):

For the snake lemma following the approach in the current version of the file is not a problem. We can prove your preliminary observation as you do. Modifying the current proof of the weak version to a proof of the strong version should then be straightforward (it is almost literally the same I think)

view this post on Zulip Peter Scholze (Jan 26 2021 at 15:41):

OK, here's an argument that weak exactness of a system of complexes of non-complete groups gives strong exactness of the completion, up to replacing kk by some other constant like k4+k2k^4+k^2 or whatever.

In general, any element of the completion xx can be written as x=x0+x1+x=x_0+x_1+\ldots with xiC2i||x_i||\leq C 2^{-i}. Then one can find yiy_i with with res(xi)d(yi)kd(xi)+2i||\mathrm{res}(x_i)-d(y_i)||\leq k||d(x_i)||+2^{-i}. In that case, d(yi)(k+1)x+2i((k+1)C+1)2i||d(y_i)||\leq (k+1)||x||+2^{-i} \leq ((k+1)C+1)2^{-i} as all maps are norm-nonincreasing, and then the weak exactness one degree lower means that we can find some ziz_i such that res(yi)d(zi)(k((k+1)C+1)+1)2i||\mathrm{res}(y_i)-d(z_i)||\leq (k((k+1)C+1)+1)2^{-i}. Let yi=res(yi)d(zi)y_i'=\mathrm{res}(y_i)-d(z_i). Then res2(xi)d(yi)kd(xi)+2i||\mathrm{res}^2(x_i)-d(y_i')||\leq k||d(x_i)||+2^{-i} and yi(k((k+1)C+1)+1)2i||y_i'||\leq (k((k+1)C+1)+1)2^{-i}. Thus y=y0+y1+y'=y_0'+y_1'+\ldots exists and res2(x)d(y)kd(x)+1||\mathrm{res}^2(x)-d(y')||\leq k||d(x)|| + 1. Replacing 11 by ϵ\epsilon in this argument, one gets weak exactness of the completed complex, with kk replaced by k2k^2.

Now comes the more interesting part, getting strong exactness. The only difference to weak exactness is that one needs to prove that if d(x)=0||d(x)||=0, then one can find yy such that res(x)=d(y)\mathrm{res}(x)=d(y). We know that for all ii, we can find yiy_i such that res(x)d(yi)2i||\mathrm{res}(x)-d(y_i)||\leq 2^{-i}. For each ii, we have in particular d(yiyi+1)21i||d(y_i-y_{i+1})||\leq 2^{1-i}, and by using weak exactness one degree lower, we can find ziz_i such that res(yiyi+1)d(zi)(k+1)21i||\mathrm{res}(y_i-y_{i+1})-d(z_i)||\leq (k+1)2^{1-i}. Let yi=res(yi)+d(zi)+d(zi+1)+y_i'=\mathrm{res}(y_i)+d(z_i)+d(z_{i+1})+\ldots. Then one has res2(x)d(yi)2i||\mathrm{res}^2(x)-d(y_i')||\leq 2^{-i} as d2=0d^2=0, while the yiy_i' form a Cauchy sequence. We can thus define yy' as the limit of the yiy_i', and then get in the limit res2(x)=d(y)\mathrm{res}^2(x)=d(y').

This is what we wanted, except for having replaced res\mathrm{res} by res2\mathrm{res}^2, which just means replacing kk by k2k^2.

view this post on Zulip Peter Scholze (Jan 26 2021 at 15:43):

@Riccardo Brasca Can you take a close look at this argument? I hope it's OK...

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 15:47):

I will try to formalize :)

view this post on Zulip Peter Scholze (Jan 26 2021 at 15:48):

That should settle it hopefully! :-)

view this post on Zulip Peter Scholze (Jan 26 2021 at 15:49):

If it works, you should stick with the weak version in the rest of the argument (in particular, in the current main goal)

view this post on Zulip Peter Scholze (Jan 26 2021 at 16:09):

Peter Scholze said:

OK, here's an argument that weak exactness of a system of complexes of non-complete groups gives strong exactness of the completion, up to replacing kk by some other constant like k4+k2k^4+k^2 or whatever. [...]

Just a warning that there's still something off here, namely I did not check that the sum d(zi)+d(zi+1)+d(z_i)+d(z_{i+1})+\ldots converges.

view this post on Zulip Peter Scholze (Jan 26 2021 at 16:41):

OK, I don't currently see how to do that argument. So for now it seems that one has to prove the strong version, and one has to do it directly for all profinite SS. Overall, the argument still looks fine to me, but I did not foresee these very subtle convergence questions; I had assumed the estimates that are in place are strong enough to handle them. Let's see what happens.

Note that I updated www.math.uni-bonn.de/people/scholze/Analytic.pdf to reflect the required changes

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 17:16):

OK :)
For the snake lemma what remains to do is formalize the "preliminary observation" in the current version of the pdf and then modifying the proof of the weak version to prove directly the strong one. The latter should really be easy, the proof is formally the same, without the ε\varepsilon's and with a different bound

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 17:17):

Once this is done we can probably throw away the definition of weak_...

view this post on Zulip Peter Scholze (Jan 26 2021 at 17:55):

Actually, the confusion carries on: I think weak exactness in the complete case does imply strong exactness. Let me modify my argument from earlier:

view this post on Zulip Peter Scholze (Jan 26 2021 at 17:56):

Peter Scholze said:

OK, here's an argument that weak exactness of a system of complexes of non-complete groups gives strong exactness of the completion, up to replacing kk by some other constant like k4+k2k^4+k^2 or whatever.

Modified:

In general, any element of the completion xx can be written as x=x0+x1+x=x_0+x_1+\ldots with xiC2i||x_i||\leq C 2^{-i}. Then one can find yiy_i with with res(xi)d(yi)kd(xi)+2i||\mathrm{res}(x_i)-d(y_i)||\leq k||d(x_i)||+2^{-i}. In that case, d(yi)(k+1)x+2i((k+1)C+1)2i||d(y_i)||\leq (k+1)||x||+2^{-i} \leq ((k+1)C+1)2^{-i} as all maps are norm-nonincreasing, and then the weak exactness one degree lower means that we can find some ziz_i such that res(yi)d(zi)(k((k+1)C+1)+1)2i||\mathrm{res}(y_i)-d(z_i)||\leq (k((k+1)C+1)+1)2^{-i}. Let yi=res(yi)d(zi)y_i'=\mathrm{res}(y_i)-d(z_i). Then res2(xi)d(yi)kd(xi)+2i||\mathrm{res}^2(x_i)-d(y_i')||\leq k||d(x_i)||+2^{-i} and yi(k((k+1)C+1)+1)2i||y_i'||\leq (k((k+1)C+1)+1)2^{-i}. Thus y=y0+y1+y'=y_0'+y_1'+\ldots exists and res2(x)d(y)kd(x)+1||\mathrm{res}^2(x)-d(y')||\leq k||d(x)|| + 1. Replacing 11 by ϵ\epsilon in this argument, one gets weak exactness of the completed complex, with kk replaced by k2k^2.

Now comes the more interesting part, getting strong exactness. The only difference to weak exactness is that one needs to prove that if d(x)=0||d(x)||=0, then one can find yy such that res(x)=d(y)\mathrm{res}(x)=d(y). We know that for all ii, we can find yiy_i such that res(x)d(yi)2i||\mathrm{res}(x)-d(y_i)||\leq 2^{-i}. For each ii, we have in particular d(yiyi+1)21i||d(y_i-y_{i+1})||\leq 2^{1-i}, and by using weak exactness one degree lower, we can find ziz_i such that res(yiyi+1)d(zi)(k+1)21i||\mathrm{res}(y_i-y_{i+1})-d(z_i)||\leq (k+1)2^{1-i}. Let yi=res(yi)d(zi1)d(z0)y_i'=\mathrm{res}(y_i)-d(z_{i-1})-\ldots-d(z_0). Then one has res2(x)d(yi)2i||\mathrm{res}^2(x)-d(y_i')||\leq 2^{-i} as d2=0d^2=0, while the yiy_i' form a Cauchy sequence. We can thus define yy' as the limit of the yiy_i', and then get in the limit res2(x)=d(y)\mathrm{res}^2(x)=d(y').

This is what we wanted, except for having replaced res\mathrm{res} by res2\mathrm{res}^2, which just means replacing kk by k2k^2.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 18:22):

I have read just the first part, it seems good to me. I don't if we have enough theory about convergent series to write it, but this is our problem :)

view this post on Zulip Johan Commelin (Jan 26 2021 at 18:25):

See tsum, there is quite a lot about it

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 18:28):

The "gotcha" with tsum is that it needs absolute convergence (1-1/2+1/3-1/4+.. will have a tsum of some junk value, rather than the limit of the finite sums from 1 to n, because it doesn't converge absolutely) but this shouldn't be an issue here.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 19:02):

I was thinking about the first sentence about writing an element of the completion as a series controlling the norm of the general term

view this post on Zulip Johan Commelin (Jan 26 2021 at 19:04):

Hmm, maybe someone who knows that analysis library knows if something like that is in mathlib already. @Sebastien Gouezel @Heather Macbeth ?

view this post on Zulip Adam Topaz (Jan 26 2021 at 19:06):

I'm certainly no expert in the analysis part of mathlib, but I don't recall seeing any api around complete normed abelian groups, so I suspect mathlib has no such fact.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 19:06):

To be honest I have to think to see why it is true :sweat_smile:

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 19:08):

It seems something like if xnxx_n \to x then consider the sequence x0,x1x0,x2(x0+x1),x_0, x_1-x_0, x_2-(x_0 + x_1), \ldots

view this post on Zulip Adam Topaz (Jan 26 2021 at 19:08):

Yeah, it's not so trivial to formalize right? I guess one can construct the sequence of xix_i recursively.

view this post on Zulip Heather Macbeth (Jan 26 2021 at 19:21):

There is some API for complete normed groups (which are abelian in mathlib, by definition), for example docs#summable_iff_vanishing_norm. But I'm not sure there's anything about the completion; do we even have its structure as a normed group? (Or have you guys recently added this?)

view this post on Zulip Johan Commelin (Jan 26 2021 at 19:23):

hah, that might be in the liquid repo :grinning:

view this post on Zulip Adam Topaz (Jan 26 2021 at 19:24):

https://github.com/leanprover-community/lean-liquid/blob/81b10397d3c0d26b951ba0c4ea8a1aac382bc490/src/locally_constant/Vhat.lean#L18

view this post on Zulip Johan Commelin (Jan 26 2021 at 19:25):

But I guess summable_iff_vanishing_norm gets us at least halfway to the statement we want.

view this post on Zulip Adam Topaz (Jan 26 2021 at 19:26):

Even better:
https://github.com/leanprover-community/lean-liquid/blob/81b10397d3c0d26b951ba0c4ea8a1aac382bc490/src/for_mathlib/locally_constant.lean#L40

view this post on Zulip Heather Macbeth (Jan 26 2021 at 19:28):

Trying to read the argument you linked ... what is res?

view this post on Zulip Johan Commelin (Jan 26 2021 at 19:30):

res is typically a restriction map. But where are you seeing it?

view this post on Zulip Johan Commelin (Jan 26 2021 at 19:31):

ooh, you mean in Peter's post? Yes, those are restriction maps in a "system of complexes"

view this post on Zulip Heather Macbeth (Jan 26 2021 at 19:31):

Peter Scholze said:

In general, any element of the completion xx can be written as x=x0+x1+x=x_0+x_1+\ldots with xiC2i||x_i||\leq C 2^{-i}. Then one can find yiy_i with with res(xi)d(yi)kd(xi)+2i||\mathrm{res}(x_i)-d(y_i)||\leq k||d(x_i)||+2^{-i}. In that case, d(yi)(k+1)x+2i((k+1)C+1)2i||d(y_i)||\leq (k+1)||x||+2^{-i} \leq ((k+1)C+1)2^{-i} as all maps are norm-nonincreasing, and then the weak exactness one degree lower means that we can find some ziz_i such that res(yi)d(zi)(k((k+1)C+1)+1)2i||\mathrm{res}(y_i)-d(z_i)||\leq (k((k+1)C+1)+1)2^{-i}. Let yi=res(yi)d(zi)y_i'=\mathrm{res}(y_i)-d(z_i). Then res2(xi)d(yi)kd(xi)+2i||\mathrm{res}^2(x_i)-d(y_i')||\leq k||d(x_i)||+2^{-i} and yi(k((k+1)C+1)+1)2i||y_i'||\leq (k((k+1)C+1)+1)2^{-i}. Thus y=y0+y1+y'=y_0'+y_1'+\ldots exists and res2(x)d(y)kd(x)+1||\mathrm{res}^2(x)-d(y')||\leq k||d(x)|| + 1. Replacing 11 by ϵ\epsilon in this argument, one gets weak exactness of the completed complex, with kk replaced by k2k^2.

This is the argument you're discussing, is that right?

view this post on Zulip Johan Commelin (Jan 26 2021 at 19:31):

yep

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 19:31):

In the above proof what we need is that res(x)x||res(x)|| \leq ||x||

view this post on Zulip Johan Commelin (Jan 26 2021 at 19:32):

@Heather Macbeth see https://math.commelin.net/web/index.html#system_of_complexes :grinning:

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 19:32):

Sorry, there is no ff

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 19:33):

The same is true for dd

view this post on Zulip Heather Macbeth (Jan 26 2021 at 19:39):

Is the point you need a lemma for, the existence of yy'? If so, what about docs#summable_of_norm_bounded?

view this post on Zulip Heather Macbeth (Jan 26 2021 at 19:39):

And docs#has_sum.norm_le_of_bounded would control its norm.

view this post on Zulip Sebastien Gouezel (Jan 26 2021 at 19:40):

There are a lot of computations like that around the proof of docs#exists_preimage_norm_le, but I don't think we have exactly this statement.

view this post on Zulip Heather Macbeth (Jan 26 2021 at 19:40):

There's also material on series whose terms are bounded by a geometric series, such as docs#cauchy_seq_finset_of_geometric_bound

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 19:53):

My impression is that we decide if we want to formalize this proof, that seems doable but with some work, or follow the approach currently in analytic.pdf: there are still Cauchy sequences, but no series (but we got a weaker result)

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:04):

Riccardo Brasca said:

It seems something like if xnxx_n \to x then consider the sequence x0,x1x0,x2(x0+x1),x_0, x_1-x_0, x_2-(x_0 + x_1), \ldots

I think you're making it more complicated than it needs to be (and less correct too). What about starting with a sequence yy which goes to xx, and starts at zero for convenience. Then extract a sub sequence that converges sufficient fast (still starting at zero) and set xn=yn+1ynx_n = y_{n+1} - y_n.

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:05):

I you need that argument I could formalize it.

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:06):

Patrick Massot said:

Riccardo Brasca said:

It seems something like if xnxx_n \to x then consider the sequence x0,x1x0,x2(x0+x1),x_0, x_1-x_0, x_2-(x_0 + x_1), \ldots

I think you're making it more complicated than it needs to be (and less correct too). What about starting with a sequence $y$ which goes to xx, and starts at zero for convenience. Then extract a sub sequence that converges sufficient fast (still starting at zero) and set xn=yn+1ynx_n = y_{n+1} - y_n.

What prevents me from taking an (eventually) constant sequence yy?

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:06):

I assume we want the sequence to be in the original group, not the completion...

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:08):

I don't have any context here, I read only the first sentence quoted by Heather.

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:08):

I see. I was envisioning formalizing the following statement:

import analysis.normed_space.basic

variables (A : Type*) [normed_group A] [complete_space A]

theorem foo {C : } (hC : 0 < C) (a : A) :  x :   A,
  has_sum x a   i,  x i   C / 2^i := sorry

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:09):

I was under the impression that we were going to assume everything was complete from the get go. But maybe I misunderstood some of the discussion above.

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:09):

I would be extremely surprised if this is the intended statement.

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:09):

@Adam Topaz Sorry, there's been considerable confusion (on my part) over the structure of the argument

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:10):

In particular, the argument that will now be formalized is different from the one in www.math.uni-bonn.de/people/scholze/Analytic.pdf

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:10):

What will happen in the project is that the notion of "k\leq k-exactness" of a system of complexes is replaced by a weakened notion, which includes some +ϵ+\epsilon in the main inequality

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:11):

Then 9.4 and 9.5 are formulated with this weaker version, and in this formulation, both easily reduce to the case that SS is finite

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:12):

Oh, so do we no longer need the fact that "weak" k\le k exactness is equivalent to "strong" k\le k exactness for complete normed abelian groups?

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:12):

Then 9.4 and 9.5 as stated in the lecture notes are recovered using the fact that for systems of complexes of complete abelian groups, the weak version implies the strong version (as stated in the lecture notes), up to changing kk (which is harmless)

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:12):

There's been confusion over whether this is actually true, but I posted an argument about 2 hours ago, and I think this one is actually sound

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:16):

So in the lecture notes, I use the strong version everywhere, and demand completeness everywhere, but in the argument that will be formalized, one uses the weak version everywhere, and then omit completeness hypotheses. One reason is that this will also give better constants in the end (while the version in the lecture notes is slightly cleaner to read, as there are fewer ϵ\epsilon's floating around).

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:18):

Okay, I think I'm following the discussion a bit better now. Thanks!

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:20):

You're welcome! And sorry again for this little mess, I'm just not good at estimates...

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 20:21):

Adam Topaz said:

I see. I was envisioning formalizing the following statement:

import analysis.normed_space.basic

variables (A : Type*) [normed_group A] [complete_space A]

theorem foo {C : } (hC : 0 < C) (a : A) :  x :   A,
  has_sum x a   i,  x i   C / 2^i := sorry

It is enough to prove this for some positive C if I am following the proof correctly, but the rest seems the correct statement

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:22):

Won't the CC depend on kk?

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 20:22):

Ah, and x i should be in the original group... so A is not complete but a is in the completion

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:23):

Yes, that I understand now. But I still think we might want it for arbitrary positive CC.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 20:23):

I guess that in practice this will be OK since x i will be constructed using a Cauchy sequence converging to a

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:24):

You can't take CC arbitrary as the sum will be bounded in norm by 2C2C

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 20:24):

For arbitrary C it is false I think, the norm of the sum will be less than 2 * C

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:24):

:face_palm: yes of course

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:25):

So this is what I wrote, right?

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:25):

(Also, there's probably other ways to argue, closer to what you have in mathlib -- I just wrote down the first argument that came to mind. You probably don't need such precise control on the convergence)

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:27):

That lemma seems very reasonable to have anyway (in a more general setting of course).

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:28):

sure!

view this post on Zulip Adam Topaz (Jan 26 2021 at 20:29):

Okay, now I'm confused again. What is CC? I guess the assertion is that this is true for any sufficiently large CC?

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:29):

Yes

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:30):

I think you can take the norm of xx

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 20:30):

The point is that the norm of xix_i shouldn't explode

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 20:30):

@Patrick Massot 's proof looks good to me

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:32):

Ok, let's say I'll handle that.

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:36):

Maybe it's best to formalize the version where xn||x_n|| for n>0n>0 is bounded by any nullsequence of positive reals, given in advance? (and x0||x_0|| bounded by x||x||)

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:40):

Sure, that's part of going to a more general version.

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:40):

can you filterize the statement?

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:40):

And if this goes to mathlib then it will probably start with a version where we have a uniform space with a countable basis of entourages.

view this post on Zulip Peter Scholze (Jan 26 2021 at 20:40):

OK, I see that this is all done in the proper way :-)

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:41):

Indeed Johan, that means filters.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 21:29):

@Johan Commelin In the project normed_group means that x=0x=0||x|| = 0 \Rightarrow x = 0, right? I am asking because as we noted some days ago this is not the same terminology used in the paper

view this post on Zulip Adam Topaz (Jan 26 2021 at 23:21):

@Riccardo Brasca the answer is yes, and this actually comes from mathlib docs#normed_group

view this post on Zulip Adam Topaz (Jan 26 2021 at 23:21):

docs#norm_eq_zero

view this post on Zulip Riccardo Brasca (Jan 27 2021 at 10:01):

If we really want to consider pseudo-normed abelian groups in the project the earlier we make the change the better it is I think... otherwise we risk to have to modify a lot of proofs

view this post on Zulip Peter Scholze (Jan 27 2021 at 10:06):

Which change?

view this post on Zulip Peter Scholze (Jan 27 2021 at 10:07):

Both concepts are relevant! There is M(S)\overline{\mathcal M}(S) that is pseudo-normed, and there is V^\hat{V} that is normed

view this post on Zulip Peter Scholze (Jan 27 2021 at 10:07):

for the normed snake lemma, the normed spectral sequence, it's all about normed things

view this post on Zulip Riccardo Brasca (Jan 27 2021 at 10:07):

Yes, I mean to introduce the concept of pseudo-normed abelian group, that we currently don't have

view this post on Zulip Peter Scholze (Jan 27 2021 at 10:09):

I think Johan Commelin is working on the pseudo-normed things; to be able to go cleanly from Hom(Λ,M(S))\mathrm{Hom}(\Lambda,\overline{\mathcal M}(S)) to the complex of 9.5, one has to give this beast the structure of a pseudo-normed group (where each c\bullet_{\leq c} is a profinite set)

view this post on Zulip Riccardo Brasca (Jan 27 2021 at 10:12):

Good! In any case my remark is really Lean-oriented, without any significant mathematical content. Unfortunately sentences like "all our theorem are about normed groups, but we had never used this property so they hold true for psuedo-normed groups" are a pain to formalize if there are a lot of dependecies

view this post on Zulip Peter Scholze (Jan 27 2021 at 10:14):

This will not come up!

view this post on Zulip Peter Scholze (Jan 27 2021 at 10:14):

The normed and the pseudo-normed things appear in separate contexts

view this post on Zulip Riccardo Brasca (Jan 27 2021 at 10:15):

Even better!

view this post on Zulip Johan Commelin (Jan 27 2021 at 10:17):

@Riccardo Brasca We want to use pseudo-normed groups, but they appear in another part, I think. Not in the snake lemma

view this post on Zulip Johan Commelin (Jan 27 2021 at 10:18):

oops, I had a lot of lag... so I missed the discussion above. Ignore my message

view this post on Zulip Johan Commelin (Jan 27 2021 at 10:19):

@Riccardo Brasca If you search for pseudo_normed_group in the repo, then you'll see that we already have it (-;

view this post on Zulip Johan Commelin (Jan 27 2021 at 10:20):

But we'll need to pack some special pseudo-normed groups into a category, and this has not been done yet. That category will serve as "input" for the construction that applies V^\hat V and builds the system of complexes (of "ordinary" complete normed groups)

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 12:41):

@Adam Topaz Are you working on weak exactness implies exactness? If not I can start doing it, assuming the lemma about writing xx as a sum of terms with controlled norm

view this post on Zulip Peter Scholze (Jan 28 2021 at 12:46):

I'll be a little relieved when that lemma is formalized :wink:

view this post on Zulip Adam Topaz (Jan 28 2021 at 13:49):

@Riccardo Brasca I started playing with it a couple of days ago. I can send you what I got so far in a few mins. Unfortunately, I won't have any time at all today for lean.

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 13:53):

I would be happy to fill some sorry

view this post on Zulip Adam Topaz (Jan 28 2021 at 13:54):

@Riccardo Brasca :down:

long

view this post on Zulip Adam Topaz (Jan 28 2021 at 13:55):

Feel free to build on it and/or completely ignore it!

view this post on Zulip Adam Topaz (Jan 28 2021 at 13:55):

I didn't get very far.

view this post on Zulip Adam Topaz (Jan 28 2021 at 13:58):

A few things to note:

  1. I was only focusing on the second paragraph of Peter's argument, so assuming everything is complete ahead of time.
  2. I'm not sure if the δ\delta is needed. I put it there just to get started.
  3. I'm not sure if I chose the correct real numbers (like kck \cdot c, etc.) in some places.
  4. As you can see, there may be some heq issues, since I construct some sequence in C.X _ i which I then need to identify with C.X _ (i-1+1).

view this post on Zulip Adam Topaz (Jan 28 2021 at 14:00):

Oh, and the #check cauchy_seq_tendsto_of_complete at the top was just for myself to remember the name of this useful lemma :)

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 14:02):

d_res_commute is already there, it is called d_res

view this post on Zulip Adam Topaz (Jan 28 2021 at 14:03):

Yeah, I figured we had it somewhere, but was too lazy to search.

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 14:03):

library_search found it for me :)

view this post on Zulip Adam Topaz (Jan 28 2021 at 14:04):

I guess I was REALLY lazy then! :rofl:

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 14:09):

Concerning the i-1+1+1 etc, in the proof the weak version I was able to completely avoid these problems : I never rewrote the indexes, so I had C ... (i + 1 + 1 + 1) but this is virtually invisible since you can always write _, Lean was very good at guessing and I let i be the smallest one, to avoid subtraction. Also, it was useful to write k^3*c as k * (k * (k * c)), since the lemmas are written this way. Otherwise you end up using congr a lot

view this post on Zulip Adam Topaz (Jan 28 2021 at 14:10):

This comes up from the argument since you first obtain some y in C.X _ i, but then you need to consider the sequence one index below, which puts you in i-1, and then you apply d which puts you back at i-1+1.

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 14:12):

Mmh, yeah, here it can be inevitable

view this post on Zulip Johan Commelin (Jan 28 2021 at 14:12):

There is C.congr to help with these annoyances

view this post on Zulip Adam Topaz (Jan 28 2021 at 14:13):

Johan Commelin said:

There is C.congr to help with these annoyances

Good to know!

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 14:13):

Sure, it is not a serious problem, but we are lazy :D

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 15:49):

@Peter Scholze Zulip is not happy if I try to quote your message for some reason, so you have to find it, sorry...

Just to be sure to understand the math. You write "...res2(x)d(y)kd(x)+1||\mathrm{res}^2(x)-d(y')||\leq k||d(x)|| + 1". We can write x=xix = \sum x_i and y=yiy' = \sum y_i', so we get res2(x)d(y)res2(xi)d(yi)kd(xi)+2i(kC2i+2i)=2kC+2||\mathrm{res}^2(x)-d(y')|| \leq \sum ||\mathrm{res}^2(x_i)-d(y'_i)|| \leq \sum k||d(x_i)||+2^{-i} \leq \sum(k C2^{-i} + 2^{-i}) = 2kC +2 . The 22's are not a problem, we can put ε\varepsilon instead, but CC is there. We can probably take C=xC= ||x|| or something similar, but d(x)d(x) can be 00. I didn't check if the argument in the second part of your post can deal with this case since you wrote kd(x)+1\ldots \leq k||d(x)|| + 1. Am I missing something?

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 15:50):

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/normed.20snake.20lemma
I can at least put a link :)

view this post on Zulip Peter Scholze (Jan 28 2021 at 16:31):

Sorry, I guess one should choose the sequence better, so that xx0||x-x_0|| is already very small. Then d(x0)||d(x_0)|| is close to d(x)||d(x)||, and the rest of the d(xi)||d(x_i)|| also contribute little.

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 17:03):

Ah yes, that seems to work. Analysis was easier when I was a student :rolling_eyes:

view this post on Zulip Riccardo Brasca (Jan 28 2021 at 19:09):

@Adam Topaz At the end I didn't had time to do anything except reading the argument. In any case I don't think δ\delta is necessary.

view this post on Zulip Patrick Massot (Jan 28 2021 at 22:07):

Quick note: I haven't forget that I promised to formalize a lemma here, but I haven't found any time yet. I hope I'll do it tomorrow.

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 13:07):

I wrote Peter's argument that weak k\leq k -exactness implies weak k2\leq k^2-exactness for the completion with full details here
https://webusers.imj-prg.fr/~riccardo.brasca/files/blueprint.pdf
in lemma 4.15. (I have to do other modifications before putting it in the official blueprint).
The proof is quite elementary, but I don't know how painful it is doing estimates of series in mathlib....
Some remarks:

  • at the beginning of the proof I write xx a sum of elements in the uncompleted group, we really need the three properties (in particular we need that x0x^0 is close enough to xx).
  • we need to prove that, under admissibility, d and res are continuous and hence commutes with infinite sum.

view this post on Zulip Johan Commelin (Jan 29 2021 at 13:12):

thanks a lot for doing this!

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 16:40):

I rewrote all Peter's argument in the stream, everything seems to be OK.
But now I forgot why we are doing this instead of following the current strategy in the pdf file (i.e. proving the preliminary observation and adapting the proof of the weak snake lemma to get a proof of the strong version): I thought this was to get better constants, but I have the impression are going in the opposite direction!

  • The current (full proved) weak snake lemma says: quotient of weak k\leq k exact stuff is k3+k\leq k^3 + k weak exact.
  • The version in the pdf says: completion of quotient of complete k\leq k exact stuff is max(k4,k3+k+1)\leq \max(k^4 , k^3 +k + 1) exact.
  • Weak k\leq k exactness implies weak k2\leq k^2 exactness of completion.
  • Weak k\leq k exactness and complete implies k2+δ\leq k^2 + \delta exactness
  • Together, the last two points give that weak k\leq k exactness implies k4+δ\leq k^4 + \delta exactness of completion. (We can probably modify the proof to obtain k2+δ\leq k^2 + \delta exactness).
    Now, in the strong snake lemma we assume MM and MM' to be complete and k\leq k exacts, but the weak version gives weak k3+k\leq k^3 + k exactness of NN, so (k3+k)4+δ\leq (k^3+k)^4 + \delta exactness of Nˉ\bar N. Even if we get to (k3+k)2+δ\leq (k^3+k)^2 + \delta exactness, this is worst than max(k4,k3+k+1)\leq \max(k^4 , k^3 +k + 1) exactness.

Now I am confused :thinking:

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 17:09):

Especially since the proof of the preliminary observation seems really easier then the other arguments

view this post on Zulip Peter Scholze (Jan 29 2021 at 20:37):

@Riccardo Brasca The point is that 9.10 will be applied very often, while that final argument will be applied precisely once

view this post on Zulip Peter Scholze (Jan 29 2021 at 20:39):

Also, in the file one has to seriously use profinite SS now, while in what Johan stated as the goal, finite SS are enough

view this post on Zulip Peter Scholze (Jan 29 2021 at 20:40):

(one could also make a reduction to finite SS, but it would then once more require that thing you just formalized

view this post on Zulip Peter Scholze (Jan 29 2021 at 20:40):

I'm very glad this worked, by the way!

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 20:58):

What I propose is to forget this new notion of weak exactness that we introduced as a fix to the problems in the original proof of 9.10 and to keep your actual proof, unless you see other reasons to keep it. This amounts to prove your "preliminary observation" about the quotient norm and then doing the rest of the proof using this.
Proving the preliminary observation is for sure easier than proving the third and fourth points of my previous message (the argument are similar and definitely easy, there are no series, just sequences): I checked these with pen and paper, but almost nothing is done in Lean. Modifying the current proof of the weak snake lemma is not a lot work.
And this is not only laziness, I have the impression that the strategy using weak exactness gives worst bounds. Of course I know only a very little part of the paper, essentially just Proposition 9.10, so my opinion can very well be irrelevant :)

view this post on Zulip Patrick Massot (Jan 29 2021 at 21:06):

I just pushed a proof of the controlled sum thing. Riccardo, could you check this is what you need?

view this post on Zulip Peter Scholze (Jan 29 2021 at 21:07):

Well, I don't mind much either way, but here are the arguments for doing the weak version:

a) Until the very last step, you can assume that SS is finite. This is surely making things a little easier. For example, whoever is trying to formalize 9.8 will probably appreciate that this profinite to finite reduction in the current version of Analytic.pdf will not have to be done (and instead a much easier profinite to finite reduction is done at the very end). Also, writing down the complexes of 9.4/9.5 is considerably easier when SS is finite.

b) It does give better constants. You observed that 9.10 gives roughly k3k^3 vs. roughly k4k^4, while that argument for weak exact => exact raises kk to the fourth power. So if you applied both once, the latter argument costs more. But 9.10 will be applied very very often in the argument, while the weak exact => exact argument will be applied exactly one time, at the very end.

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 21:13):

@Patrick Massot That's seems perfect, thank you!

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 21:29):

OK, I think I misunderstood the whole strategy: I thought you need in any case the strong snake lemma for completion (and the path weak snake lemma, then completions gives k12k^{12} instead of the current k4k^4), but what you propose is to use weak exactness everywhere and at the very end go to strong exactness.

view this post on Zulip Peter Scholze (Jan 29 2021 at 21:30):

Exactly, everything is weak up until the very end

view this post on Zulip Peter Scholze (Jan 29 2021 at 21:30):

By "weak exact => exact for complete" you could always at will pass to the strong version, but this would cost some constants

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 21:46):

I will let someone that knows better than me the analysis part of mathlib decide how difficult it is to formalize the arguments of 4.15 and 4.16 of https://webusers.imj-prg.fr/~riccardo.brasca/files/blueprint.pdf
The file contains currently the best of the two approaches, and if we have proofs of 4.15 and 4.16 we can surely do the beginning of 4.18 very quickly (and I can take care of the rest). Note that the beginning of 4.15 (writing xx as a sum) has been done by Patrick, the rest is very elementary but with a lot of small calculations.

view this post on Zulip Patrick Massot (Jan 29 2021 at 21:50):

It all looks straightforward to formalize. I don't say it will be fun, but it looks totally doable without too much thinking.

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 22:02):

This is very possible! But I remember when I literally spent two hours to prove that {1,3,5,7,15,21,35}\{1, 3, 5, 7, 15, 21, 35 \} has six seven elements (now I know that refl can do it) and now I prefer to ask :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (Jan 29 2021 at 22:03):

it has 7 tho

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 22:04):

ROTF

view this post on Zulip Patrick Massot (Jan 29 2021 at 22:05):

That's what we call number theorists those days...

view this post on Zulip Patrick Massot (Jan 29 2021 at 22:08):

It reminds me of a colloquium by Jean-Yves Welschinger about real enumerative geometry where he spent one hour explaining his job was to count geometric objects and then failed to draw five lines on the board (I don't remember whether he drew 4 or 6 lines).

view this post on Zulip Patrick Massot (Jan 29 2021 at 22:09):

Anyway, if you are sure those lemmas 4.15 and 4.16 are what you want and if you formalize the statements then I can probably handle the proofs at some point during the week.

view this post on Zulip Patrick Massot (Jan 29 2021 at 22:10):

But now I should go to bed.

view this post on Zulip Riccardo Brasca (Jan 29 2021 at 22:11):

As you said this is not going to be fun, so I prefer that someone else check that this is really what we want

view this post on Zulip Johan Commelin (Mar 13 2021 at 09:23):

The strictness assumption in 9.10 (normed snake) can be relaxed to norm-nonincreasing. I guess this is useful for our application in 9.6.

view this post on Zulip Johan Commelin (Mar 13 2021 at 14:04):

Hmm... we assume exactness at M' in the statement of weak_snake_lemma. But I think we should refactor this to say that kernel of g is the topological closure of the range of f.

view this post on Zulip Johan Commelin (Mar 15 2021 at 07:29):

@Riccardo Brasca Does this weakened hypothesis look plausible to you?

view this post on Zulip Johan Commelin (Mar 15 2021 at 07:29):

I didn't yet look into whether the proof can easily be refactored

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 08:49):

I will have a look at it later today, but I think we have everything we need to refactor the proof

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 09:09):

Concerning the refactor using the kernel of g, we should first of all prove that if 0M1M2M30 \to M_1 \to M_2 \to M_3 \to is exact (in some sense) then M3M_3 is isomorphic to the quotient M2/M1M_2/M_1. Another possibility is to prove the lemma directly for the quotient, without introducing a new complex

view this post on Zulip Johan Commelin (Mar 15 2021 at 09:12):

Nah, it's best to use the predicate, like we have now. Because in the application in 9.6 we don't get something that is definitionally the quotient. All the objects will be definitionally the quotient, but the system of complexes will probably not be.

view this post on Zulip Kevin Buzzard (Mar 15 2021 at 09:20):

@Riccardo Brasca we learnt this from the theory of localisation. If you define the field of fractions of an integral domain and then prove things about it, you can't deduce anything for the rational numbers because they're not literally equal to the field of fractions of the integers in the sense that they're not literally a built as a localisation.

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 13:04):

@Johan Commelin The assumption in the normed snake lemma is already norm-nonincreasing, isn't it?

lemma weak_normed_snake {k k' k'' K K' K'' : 0}
  [hk : fact (1  k)] [hk' : fact (1  k')] [hk'' : fact (1  k'')]
  {m : } {c₀ : 0}
  (hM : M.is_weak_bounded_exact k K (m+1) c₀)
  (hM' : M'.is_weak_bounded_exact k' K' (m+1) c₀)
  (hM'_adm : M'.admissible)
  (hf :  c i, (f.apply : M c i  M' c i).norm_noninc)
  (Hf :  (c : 0) [fact (c₀  c)] (i : ) (hi : i  m+1+1) (x : M (k'' * c) i),
    (res x : M c i)  K'' * f x)
  (hg :  c i, (g.apply : M' c i  N c i).ker = f.apply.range)
  (hgquot : system_of_complexes.is_quotient g) :
  N.is_weak_bounded_exact (k''*k*k') (K'*(K*K'' + 1)) m c₀ :=

view this post on Zulip Johan Commelin (Mar 15 2021 at 13:08):

Yes, I did that part

view this post on Zulip Johan Commelin (Mar 15 2021 at 13:08):

@Riccardo Brasca But we need another refactor, namely hg should be weakened

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 13:50):

OK, I had a look at it, and it is slightly longer than I thought: we need to prove Peter's "preliminary observation" (at the beginning of the proof of 9.10 in Analytic.pdf). This will modify some of the constants in the result (with something like k^4 if we use a single constant). If you're happy with this result I can work on it

view this post on Zulip Johan Commelin (Mar 15 2021 at 13:54):

@Riccardo Brasca Sounds good! It is one of the missing bits to complete the proof of 9.6.

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:19):

Hmm, the preliminary observation seems to require completeness . If this is the versions of the snake lemma we need I don't see point of having the notion of weak exactness. (Note that proving the strong snake lemma modifying the proof of the weak one is not that much work.)

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:20):

Ah, I see you also said that in the end we don't really need the weak version

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

@Peter Scholze What do you think? Should we just assume completeness everywhere?

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:21):

I didn't follow this discussion closely. It seemed to me that completeness shouldn't be needed, if one uses the weak notion of exactness

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:22):

where do you now use completeness?

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:22):

(Not using completeness should give slightly better constants in the end; I think this was the main argument for not assuming it.)

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:23):

The constants can't get worse by adding the extra assumption, right?

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:24):

Hmm they can, because the snake lemma more easily gives weak exactness than strong exactness

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:24):

or do you mean assume completeness + strong exactness?

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:24):

In the normed snake lemm we have MfMgNM \stackrel{f}{\to} M' \stackrel{g}{\to} N and we assume im(f)=ker(g)\text{im}(f) = \text{ker}(g).

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:24):

Concerning the normed snake lemma we have a version (completely proved) for weak exactness, that assumes that the image of f is closed

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:25):

wait, why should the image of f be closed?

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:25):

But I think we need ker(g)=im(f)\ker(g) = \overline{\text{im}(f)}

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:25):

right, we assume that it is, but in the proof of 9.6 we don't have that assumption. So there is a little hole there.

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:25):

hmm wait

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:26):

it's OK

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:26):

Peter Scholze said:

or do you mean assume completeness + strong exactness?

I meant assume completeness + weak exactness, and prove weak exactness.

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:26):

In the inductive step of 9.6, you just shouldn't take the quotient by the closure of the image

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:26):

Just take the quotient by the image

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:26):

But then the quotient isn't a normed group, is it?

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:26):

I was only taking the closure to keep things complete (as in the manuscript, everything is complete, and I want strong exactness)

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:26):

It is, I think

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:27):

Ooh, in your generalised sense!

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:27):

Wait, I'm confused...

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:29):

What's the Lean definition of a normed group?

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:29):

Right, you can't prove x=0    x=0\||x = 0\|| \iff x = 0 if the subgroup isn't closed

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:29):

Yes

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:29):

And lean assumes that axiom

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:29):

Ah

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:29):

But it doesn't assume completeness?

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:29):

Nope

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:29):

So separated, but not complete

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:29):

Right

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:30):

That's a weird convention then

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:30):

/-- A normed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥` defines
a metric space structure. -/
class normed_group (α : Type*) extends has_norm α, add_comm_group α, metric_space α :=
(dist_eq :  x y, dist x y = norm (x - y))

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:30):

I think it is because with this definition you can extends metric_space

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:31):

wait, a metric space also requires that?

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:31):

Yes....

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:31):

Weird... OK

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:31):

/-- Metric space

Each metric space induces a canonical `uniform_space` and hence a canonical `topological_space`.
This is enforced in the type class definition, by extending the `uniform_space` structure. When
instantiating a `metric_space` structure, the uniformity fields are not necessary, they will be
filled in by default. In the same way, each metric space induces an emetric space structure.
It is included in the structure, but filled in by default.
-/
class metric_space (α : Type u) extends has_dist α : Type u :=
(dist_self :  x : α, dist x x = 0)
(eq_of_dist_eq_zero :  {x y : α}, dist x y = 0  x = y)
(dist_comm :  x y : α, dist x y = dist y x)
(dist_triangle :  x y z : α, dist x z  dist x y + dist y z)
(edist : α  α  0 := λx y, ennreal.of_real (dist x y))
(edist_dist :  x y : α, edist x y = ennreal.of_real (dist x y) . control_laws_tac)
(to_uniform_space : uniform_space α := uniform_space_of_dist dist dist_self dist_comm dist_triangle)
(uniformity_dist : 𝓤 α =  ε>0, 𝓟 {p:α×α | dist p.1 p.2 < ε} . control_laws_tac)

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:31):

It seems that this is also the wikipedia definition

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:31):

The second axiom

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:32):

right

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:32):

In Leiden they also taught me that axiom for metric spaces

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:32):

It may very well be the standard

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:33):

@Sebastien Gouezel @Heather Macbeth what do you think... does it make sense to relax this axiom in mathlib?

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:33):

Maybe I am confused, but d(x,y)=0x=yd(x,y) = 0 \Rightarrow x = y seems pretty standard :thinking:

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:33):

I think algebraic geometers somehow got off the normal tracks when they changed from "prescheme/scheme" to "scheme/separated scheme"

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:34):

@Patrick Massot Can we easily see how much of the library we need to duplicate if we want to roll our own normed_group?

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:34):

We can just call it seminormed_group...

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:34):

Sure, but how many library lemmas do we need to reprove?

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:35):

Just joking :sweat_smile:

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:35):

@Peter Scholze But if we use weak exactness + complete normed groups, the constants should still be the good ones

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:35):

Hmm, I guess so

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:35):

And for the final application it doesn't matter either

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:35):

So that might be the easy way out (-;

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:36):

Hmm, OK, then indeed one has to modify 9.10 a bit to incorporate some passage to the completion

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:37):

I think that would actually make the constants slightly worse there

view this post on Zulip Julian Külshammer (Mar 15 2021 at 14:40):

I saw this being called a pseudometric space https://en.m.wikipedia.org/wiki/Pseudometric_space

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 14:41):

I really don't think it is a good idea to change the metric space definition in mathlib, which is the standard one. Whenever you do analysis, having unique limits is extremely useful! (That's why in all analysis books the L^p space is a space of equivalence classes of functions, for instance).

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:42):

@Sebastien Gouezel But if we call them pseudometric_space?

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:42):

85% of the lemmas will still be about metric_space, but some of the general facts can be proven for pseudometric_space

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 14:43):

Sure, why not. It's a little bit like non-separated topological groups: they show up sometimes, but whenever you want to do something serious, like extending a uniformly continuous function, you have to go to the separated quotient first.

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:43):

OK, I think that should be the solution: Just also introduce pseudometric_space and seminormed_group and use these things instead

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:43):

And similarly, we could then have seminormed_group. (It seems that pseudo_normed_group has recently be claimed...)

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:45):

Ok, great. Then we don't change the normed snake lemma.

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:47):

Any volunteers for the refactor? Otherwise I'll do it when I don't have inspiration for something else.

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:49):

@Sebastien Gouezel OK, I definitely don't want to change the definition of metric_space. It's just that from my experience in algebraic geometry, I always tend to explicitly think of separatedness as something that should not be included in the most primitive definition, only added later on top. This is probably an irrelevant consideration when doing analysis, but maybe a little relevant when setting up something like mathlib, so I think it would be good to include pseudometric_space now.

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:53):

But in any case for the snake lemma we cannot assume that f has closed image, right? And for that I have the impression that completeness is needed... or not?

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 14:53):

It certainly can't hurt. And indeed I've already been longing for this class to be in mathlib several times (for instance to put a uniform structure on the space of integrable functions).

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:53):

@Riccardo Brasca The current version is fine with the generalised definitions

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:53):

We can't assume that f has closed image. But we shouldn't need it...

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:54):

Because we can then drop is_closed from the instance of seminormed_group for quotients

view this post on Zulip Damiano Testa (Mar 15 2021 at 14:56):

I like the distinction metric vs pseudo-metric. For a specific example, the Kobayashi pseudo-metric is usually referred to as a pseudo-metric, even though the title (but not the body) of the Wikipedia page says otherwise:

https://en.wikipedia.org/wiki/Kobayashi_metric

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:57):

Ah sure! In that case I will give a try to the refactor!

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 14:58):

What is the general strategy? Introduce pseudometric_space and check by hand what stay true in this generality?

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:01):

One complication is whether we also want pseudo_emetric_space...

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:01):

(allowing \infty as distance)

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:02):

@Riccardo Brasca yes, that's the strategy that I would use. It might mean reorganizing a bunch of things into different sections, and maybe even split into different files

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:04):

I don't think infinite distances are relevant to what we're doing here... maybe leave that for another day then?

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:05):

It's not relevant for this project, I agree. But if we dive into a refactor, we might want to do both in one go...

view this post on Zulip Julian Külshammer (Mar 15 2021 at 15:10):

A pseudo_emetric shows for example up in topological data analysis.

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:11):

I didn't expect topological data analysis to come up in this stream ;-)

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 15:21):

Apperently in mathlib these things are called docs#premetric_space

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:22):

Ooh! So we have them already in some sense?

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:22):

That means we only need to do the seminormed_group stuff?

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 15:23):

Not really, nothing is proved for them, but at least we don't have to chose the name :D

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:24):

Should we call them prenormed_group as well?

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:24):

Because seminormed_group sounds like it might have something to do with seminorms

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:24):

Which isn't really the point that we try to make

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:27):

Isn't this exactly a seminorm?

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 15:27):

I thought a seminorm was exactly a norm without the assumption that x=0x=0||x|| = 0 \Rightarrow x=0

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:28):

Also, "pseudometric space" seems the standard name in the literature, so why use "premetric space" instead?

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:28):

ooh, you are right. so seminormed_group it is! :face_palm:

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 15:28):

Note that nothing is proved currently on premetric_space, I only introduced it some time ago as a gadget to construct metric spaces by taking a suitable quotient. For instance, there is currently no uniform space structure on a premetric space.

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:29):

We can rename premetric_space

view this post on Zulip Sebastien Gouezel (Mar 15 2021 at 15:30):

It will be a little bit strange to have pseudometric_space and seminormed_space, but hey, we all know that mathematics terminology is not always coherent :-)

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:31):

It is! But those seem to be the standard names...

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 16:29):

I gave a little try to understand what is needed for the refactor about pseudometric_space (or whatever name we choose), and I think I can do it. If I understand correctly how mathlib is set up, emetric_space is more fundamental than metric_space (this is clear looking at the imports), so I will start there

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:30):

Are there pre_emetric_spaces already? Otherwise, I think you can choose to skip that step. Whichever you prefer.

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 16:34):

No, there aren't, but it doesn't seem very complicated to do both

view this post on Zulip Riccardo Brasca (Mar 15 2021 at 20:31):

If someone wants to have a look I created #6694, for extended pseudo metric spaces.

view this post on Zulip Johan Commelin (Mar 15 2021 at 20:40):

Thanks, I left 1 comment (-;

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:32):

Hooray! normed_group_hom in mathlib is now refactored to work for semi normed groups.
Major thanks to Riccardo for the 5 or 6 PRs that performed the refactor!

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 13:34):

I have some time today to work on semi_normed_group in the LTE! leanproject upgrade-mathlib is all I have to do to ugrade mathlib? I am working in my branch

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:37):

Yes, leanproject up should get you started. But there might be unexpected breakage.

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:37):

So I can help with bumping mathlib, if you want.

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:38):

Hmm, we need to wait a bit longer. @Riccardo Brasca

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:39):

The oleans aren't available yet.

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 13:39):

No problem :)

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:55):

Now they are there, it seems

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 13:58):

leanproject up did its job. If I try to build the project I get a lot of errors, but I can work normally on normed_group_quotient.lean

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:59):

I'll look at the other errors

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:59):

Is your branch clean?

view this post on Zulip Johan Commelin (Apr 06 2021 at 14:00):

Or is there other stuff on it too, that might make a merge a bit more complicated?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 14:01):

I created a new branch, but it's very possibile that I messed up with leanproject build.

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 14:02):

The first error is

/imjprgpool/home/brasca/lean/lean-liquid/_target/deps/mathlib/src/category_theory/abelian/additive_functor.lean:1:0: error: file '/imjprgpool/home/brasca/lean/lean-liquid/_target/deps/mathlib/src/category_theory/abelian/additive_functor.lean' not found in the search path

So it's probably my fault

view this post on Zulip Johan Commelin (Apr 06 2021 at 14:02):

No, I got the same.

view this post on Zulip Johan Commelin (Apr 06 2021 at 14:02):

That file moved in mathlib. I'm fixing those errors in LTE right now (-;

view this post on Zulip Johan Commelin (Apr 06 2021 at 14:06):

@Riccardo Brasca I've pushed some fixes to bump-mathlib-2021-04-06

view this post on Zulip Johan Commelin (Apr 06 2021 at 14:06):

But now the errors are about NormedGroup and such

view this post on Zulip Johan Commelin (Apr 06 2021 at 14:06):

So that's probably more related to what you are doing

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 14:26):

Yes, that looks like a real error caused by something about normed_group_hom, that now accepts semi_normed_group. I am playing with it to see if I can fix it without too much work... I am not very familiar to declaration like def NormedGroup : Type (u+1) := bundled normed_group.

view this post on Zulip Johan Commelin (Apr 06 2021 at 14:27):

I think you should just generalize it to semi_normed_group

view this post on Zulip Johan Commelin (Apr 06 2021 at 14:27):

And see what breaks after that (-;

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 16:51):

I started in the branch semi_normed the refactor to include semi_normed_group in the LTE. What I did is to generalize the files
src/for_mathlib/normed_group src/for_mathlib/normed_group_hom_equalizer, src/for_mathlib/normed_group_hom and src/for_mathlib/normed_group_quotient: no problem here.

Then I started working on src/normed_group/NormedGroup: I essentially wrote semi everywhere (but I didn't change the name of the category, even if this should be done) and erased the lemma coker.exists_norm_le that is useless since now we take the algebraic quotient (without taking the closure).

Now Lean complains about other places where NormedGroup is used, for example in src/locally_constant/NormedGroup. I am not very familiar with the category theory part of mathlib, so it probably makes more sense if someone else look at this, at least to have a plan of what we have to do. For example, do we want locally constant functions with values in a pseudo_metric_space? Do we need both the category SemiNormedGroup and the category NormedGroup?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 16:52):

I guess the authors of almost everything in this part of the project are @Johan Commelin and @Adam Topaz

view this post on Zulip Adam Topaz (Apr 06 2021 at 16:54):

@Riccardo Brasca I can take a look in about an hour.

view this post on Zulip Adam Topaz (Apr 06 2021 at 16:59):

Well, just looking very quickly, it seems that there is no seminormed_group instance on locally constant functors, and that's the source of the issue in src/locally_constant/NormedGroup.lean

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:03):

Yes, the problem is for sure that one. What confuses me is that there is a normed_group instance, and so also a semi_normed_group instance. In any case the question is if we should generalize everything to semi_normed_group or rather convince Lean that here everything is automatically a semi_normed_group.

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:04):

But the instance is there only for locally constant functions into a normed group.

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:04):

So locally_constant/analysis.lean should be generalised.

view this post on Zulip Adam Topaz (Apr 06 2021 at 17:08):

looks like locally_constant.pseudo_metric_space is missing

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:10):

I pushed a fix

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:10):

I just did it, locally_constant/analysis.lean is now for pseudo_metric_space.

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:10):

But maybe we want to keep the results for metric_space

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:11):

@Riccardo Brasca ooh, you might want to pull

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:12):

failed to synthesize type class instance for
V : NormedGroup
 semi_normed_group (completion V)

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:12):

This is hopefully in mathlib?

view this post on Zulip Adam Topaz (Apr 06 2021 at 17:14):

Is this true?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:14):

I thought about that, but complete means t1 in mathlib

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:14):

And maybe even in standard mathematics, I am not sure

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:14):

But that is not a problem right?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:16):

It means that is probably even a normed_group

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:17):

Right, I think that the completion of a semi_normed_group is always a normed_group.

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:18):

So we might need another mathlib PR that generalizes topology.metric_space.completion

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:18):

Yes :expressionless:

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:18):

I can do it very quickly

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:24):

#7066

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:26):

Wow! I expected a much larger diff.

view this post on Zulip Patrick Massot (Apr 06 2021 at 17:28):

Don't forget the backbone of all this is the general uniform space completion that doesn't see any difference between pseudo-norms and norms, it way more general.

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:31):

Hmmm, so now we are stuck for a couple of hours... or can we quickly duplicate this instance in some for_mathlib/temp.lean?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 17:34):

Dinner time for me, but fell free to modify my branch

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:56):

I did this, but now we need to do a bit of maths.

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:57):

Completion.lift uses is_closed_eq in its proof.

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:57):

This no longer works. So I need to think about what is the correct move.

view this post on Zulip Adam Topaz (Apr 06 2021 at 17:58):

Is this pushed to the branch?

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:58):

yes

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:58):

Ooh, it's actually quite obvious. We should just assume that the target of the lift is a t2_space

view this post on Zulip Johan Commelin (Apr 06 2021 at 17:58):

Because clearly you can't lift V -> W to the completion of V for arbitrary W.

view this post on Zulip Adam Topaz (Apr 06 2021 at 17:59):

Doesn't complete imply t2?

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:00):

Hmm, maybe it does, because t1 => t2 for groups?

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:00):

But mathlib doesn't seem to realize this

view this post on Zulip Adam Topaz (Apr 06 2021 at 18:00):

hmmm....

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:02):

docs#uniform_space.completion says "Hausdorff completion of α", so it should be t2... I think

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:02):

Idem dito, it can't find [separated_space W]. So we are missing complete_space => separated_space

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:04):

I've just added these redundant hyps with a comment. So we can remove them later.

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:04):

Pushed.

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:05):

Why docs#uniform_space.completion.separated_space doesn't work?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:06):

Hm, I see

view this post on Zulip Adam Topaz (Apr 06 2021 at 18:07):

Yeah, it's a bit silly.

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:09):

Should we call NormedGroup SemiNormedGroup (and maybe recreate NormedGroup)? This will break a lot of files of course, but it is more clear

view this post on Zulip Adam Topaz (Apr 06 2021 at 18:11):

NB. https://github.com/leanprover-community/mathlib/blob/d7f6bd6188fc10f085bbcfcf513942467a071dc3/src/topology/uniform_space/completion.lean#L453

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:16):

The correct thing to do is the following I think: if M and N are semi_normed_group (or pseudo_metric_space, or whatever), and f : M → N then the induced map completion M → completion N is given by considering the natural map i : N → completion N, so now i ∘ f : M → completion N can be extendend.

view this post on Zulip Adam Topaz (Apr 06 2021 at 18:20):

That's fine for the completion functor, but not for lift

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

On the other hand, I don't know whether we actually need Completion.lift?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:24):

Ah sorry, you're right. But complete means separated, so that's OK anyway

view this post on Zulip Adam Topaz (Apr 06 2021 at 18:29):

Is this actually true for arbitrary uniform spaces?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:31):

docs#uniform_space.completion.separated_space seems to say this

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:31):

I just pushed fix rescale.normed_group

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:31):

If complete implies equal to the completion

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:37):

It seems that there are 3 or 4 errors left

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:39):

Oups, one error is my fault, I erased NormedGroup.coker.exists_norm_le

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:42):

Another one is trickier.

lemma to_exact (hC : C.is_weak_bounded_exact k K m c₀) {δ : 0} ( : 0 < δ)
  (H :  c  c₀,  i  m,  x : C (k * c) i,  j, i+1 = j 
    C.d _ j x = 0   (i₀ : ) (hi₀ : i₀ = i - 1) (y : C c i₀), res x = C.d _ _ y) :
  C.is_bounded_exact k (K + δ) m c₀ :=

is no longer obviously true

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:44):

Which is used in

lemma strong_of_complete [hk : fact (1  k)] [hk' : fact (1  k')]
  (hC : C.is_weak_bounded_exact k K m c₀)
  (hC' : admissible C) [ c i, complete_space (C c i)] :
   δ > 0, C.is_bounded_exact (k^2) (K + δ) m c₀ :=

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:45):

These proofs currently make actual use of norm_eq_zero_iff and friends

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:46):

@Riccardo Brasca But exists_norm_le maybe also needs a bit of refactoring, right?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:47):

The lemma says

lemma coker.exists_norm_le {f : A  B} (y₁ y₂ : B)
  (h : (coker.π y₁ : coker f) = coker.π y₂) (ε : ) ( : 0 < ε) :
   x, y₁ - f x  y₂ + ε :=

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:47):

Now it is true even for ε = 0, isn't it?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:48):

The ε does not come from the quotient norm, it comes from the closure of the kernel

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:48):

So the proof simplifies?

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:50):

I mean that the statement is completely trivial, if y₁ and y₂ are equal in the cokernel the difference is in the image of f, since we are taking the algebraic quotient

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 18:53):

I have to stop now, sorry!

view this post on Zulip Johan Commelin (Apr 06 2021 at 18:58):

Ooh, of course :smiley: I forgot what the statement actually said.

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:10):

That problem is now solved: git commit -am "fix src/system_of_complexes/truncate.lean"

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:11):

So now there are two errors left, related to this strong_of_complete

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:11):

Besides that, this mathlib bump is finished.

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:24):

Do you still have questions about completeness and separation?

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:25):

Johan Commelin said:

Idem dito, it can't find [separated_space W]. So we are missing complete_space => separated_space

This implication is not correct (at least not with our definition of complete, which is also Bourbaki's definition of complete). However completion X is always separated, even if X isn't.

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:26):

The subcategory of complete but not necessarily separated uniform spaces has no good categorical properties.

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:41):

@Patrick Massot So completion can do something nontrivial to a complete space?

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:42):

No, it can make it smaller

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:42):

In strong_of_complete we are assuming that we have complete_space and semi_normed_group.
That should still imply normed_group, because t1 implies t2 for topological groups.

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:42):

But turning this into an instance is of course tricky. Because it will start looping.

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:43):

Yes, t1 implies t2 for topological groups.

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:45):

Is there code to fix? On which branch?

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:48):

@Patrick Massot semi_normed is the branch

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:49):

I just checked: the final sorry in normed_spectral (9.6) just vanished completely :happy:

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:50):

Is there anything to fix then?

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:50):

Yes

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:50):

strong_of_complete is broken

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:51):

Because it assumes that the objects are normed_groups

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:51):

And Lean doesn't know that semi_normed_group + complete_space implies normed_group.

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:51):

We'll even have to think about how to state that implication without creating loops or diamonds.

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:52):

This isn't true

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:52):

I think you mean semi_normed_group + separated implies normed_group

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:52):

But complete_space implies t1, right?

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:53):

why?

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:53):

I thought someone said that. I didn't check mathlib.

view this post on Zulip Adam Topaz (Apr 06 2021 at 19:53):

Is it not true that a complete pseudo_metric_space is T2?

view this post on Zulip Adam Topaz (Apr 06 2021 at 19:54):

I agree about general uniform spaces btw

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:56):

It is certainly true if you put separation in the definition of complete, but a priori I don't see why it would be automatic

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 19:56):

Johan Commelin said:

I thought someone said that. I didn't check mathlib.

I said that... I thought that the completion of a complete space was the same as the space :sweat_smile:

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:56):

Right, defn 8.16(3) puts separated in the definition of complete.

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:57):

@Patrick Massot For me it's fine if we prove strong_of_complete assuming separated. Because we will only ever apply it to completion foobar.

view this post on Zulip Johan Commelin (Apr 06 2021 at 19:57):

But to make the proof work, we still need some glue to move from separated_space to norm_eq_zero_iff.

view this post on Zulip Patrick Massot (Apr 06 2021 at 19:58):

The name completion is maybe a bit unfortunate, but separated_completion seemed too long.

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:00):

And of course Bourbaki calls it completion only.

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:01):

Assuming semi_normed and separated is a bit silly, this is equivalent to normed_group, right?

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:03):

Yes, but you are handed a system_of_complexes, whose objects are by definition semi_normed_group.

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:03):

If normed_group was a mixin on top of semi_normed_group, there wouldn't be a problem. But of course that would be a gigantic refactor, and it's not even clear if it is desirable from a UX point of view.

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:05):

I see

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:07):

@Patrick Massot Do you want to give it a shot?

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:07):

cauchy_seq_of_le_geometric is also used there, so it's not only about elements with norm zero.

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:09):

Maybe we can write a def normed_group_of_separated and lift the semi_normed_group structure to a normed_group manually?

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:09):

Then we just add a line to the top of the proof, and hopefully the rest of the proof just works.

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:10):

That sounds like a cheap workaround, but actually this situation may be quite rare and not deserving a big refactor.

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:10):

So maybe we should be lazy

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:11):

Do we already have a def upgrading a pseudo normed group to a normed group using a proof of norm x = 0 implies x = 0?

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:12):

pseudo normed groups don't even have a has_norm at the moment. (And note that there can be elements with norm \infty).

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:12):

Or did you mean semi_normed_group?

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:12):

In the latter case, @Riccardo Brasca did you write such a constructor?

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:15):

Yes, I meant semi normed group

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 20:18):

I don't remember writing it, but maybe it is more or less already there. The difference between semi_normed_group and normed_group is that the first extends pseudo_metric_space, the latter metric_space

view this post on Zulip Riccardo Brasca (Apr 06 2021 at 20:18):

And metric_space extends pseudo_metric_space

view this post on Zulip Patrick Massot (Apr 06 2021 at 20:29):

I need to do something else, but you should feel free to use:

lemma