normed snake lemma

Stream: condensed mathematics

[Johan Commelin]

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

[Riccardo Brasca]

Great! This looks like something not too hard

[Riccardo Brasca]

You probably forgot a lemma normed_snake at the of the file

[Riccardo Brasca]

I mean, you forgot to write the statement :)

[Johan Commelin]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

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

[Johan Commelin]

I fixed a typo in the statement.

[Riccardo Brasca]

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?

[Adam Topaz]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Riccardo Brasca]

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.

[Riccardo Brasca]

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

[Johan Commelin]

Yep... I wrote a hasty statement

[Johan Commelin]

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.

[Johan Commelin]

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!

[Riccardo Brasca]

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

[Adam Topaz]

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?

[Johan Commelin]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

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?

[Adam Topaz]

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

[Riccardo Brasca]

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

[Johan Commelin]

sure, that condition should be removed

[Adam Topaz]

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

[Riccardo Brasca]

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

[Johan Commelin]

Right, me stupid :oops: :rofl:

[Riccardo Brasca]

But I don't think this property characterize the projection

[Johan Commelin]

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.

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

Hmm, maybe we only have it for linear maps

[Riccardo Brasca]

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?

[Riccardo Brasca]

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

[Johan Commelin]

normed groups aren't assumed to be complete

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

Something is happening here: if $a \in \bar Y$ but $a \not \in Y$ then $||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$ iff $a=0$)

[Johan Commelin]

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

[Johan Commelin]

so we should change the definition in Lean

[Johan Commelin]

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

[Johan Commelin]

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.

[Riccardo Brasca]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

because the subgroups might not be closed? makes sense

[Johan Commelin]

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

[Riccardo Brasca]

If you require separateness then the quotient exist for closed subspace

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

oh that's what you wrote :)

[Adam Topaz]

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

[Johan Commelin]

there is a thorough api for separation and completion.

[Riccardo Brasca]

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 $||\pi(x)|| \leq ||x||$ where $\pi$ is the projection

[Johan Commelin]

maybe we should just try formalizing it

[Johan Commelin]

the proof looks very Leanable

[Johan Commelin]

does someone want to livestream their attempt?

[Riccardo Brasca]

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

[Heather Macbeth]

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

[Riccardo Brasca]

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

[Johan Commelin]

hmmm, the hN still looks wrong, right?

[Johan Commelin]

should that = be \le?

[Riccardo Brasca]

Ops, I thought I did it

[Johan Commelin]

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

[Adam Topaz]

Johan Commelin said:

does someone want to livestream their attempt?

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

[Peter Scholze]

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 $M$ to $M'$ is "pro-injective" (any element in the kernel gets killed by some (explicit) restriction map), but on the norm-$0$-part arbitrary things can happen. Fortunately, the notion of $\leq k$-exactness actually only depends on the separated quotients! So I think what I wrote should be OK.

[Johan Commelin]

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

[Johan Commelin]

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

[Peter Scholze]

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

[Bhavik Mehta]

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

[Riccardo Brasca]

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₀

[Riccardo Brasca]

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

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

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

Here $N_{k^3c}^{i+1}$ is the quotient by the image of $f_{k^3c}^{i+1}$ and the projection of $m_{k^3c}'^{i+1}$ is $n_{k^3c}^{i+1}$ by definition. In particular we also have $\pi(m_{k^3c}''^{i+1}) = n_{k^3c}^{i+1}$, so $||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$ in the definition of the quotient norm is a $\min$, attained at $m_{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?

[Johan Commelin]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

@Adam Topaz Yes, that's what I mean

[Adam Topaz]

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

[Adam Topaz]

Just trying to orient myself (I just woke up)

[Riccardo Brasca]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Riccardo Brasca]

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

[Adam Topaz]

@Riccardo Brasca Are you formalizing the proof?

[Riccardo Brasca]

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

[Adam Topaz]

There was some talk of live streaming? ;)

[Adam Topaz]

Is there a good reason to introduce k_new separately?

[Riccardo Brasca]

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

[Adam Topaz]

Perhaps you should push the corrected statement of the theorem?

[Johan Commelin]

Adam Topaz said:

Is there a good reason to introduce k_new separately?

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

Sure, I guess we need

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

[Adam Topaz]

This works:

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

will do.

[Adam Topaz]

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

[Adam Topaz]

Ah okay, I can use this: docs#one_le_pow_iff

[Adam Topaz]

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

[Riccardo Brasca]

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)

[Adam Topaz]

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

[Riccardo Brasca]

I am working on a copy :)

[Adam Topaz]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Adam Topaz]

Sure.

[Adam Topaz]

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

[Adam Topaz]

pushed.

[Johan Commelin]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Johan Commelin]

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

[Riccardo Brasca]

I am riccardobrasca on GitHub

[Johan Commelin]

invitation sent

[Riccardo Brasca]

Pushed to branch snake

[Adam Topaz]

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

[Riccardo Brasca]

Good to know!

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Heather Macbeth]

docs#le_of_forall_le_of_dense ?

[Heather Macbeth]

or even closer, docs#le_of_forall_pos_le_add

[Riccardo Brasca]

@Heather Macbeth perfect, thank's!

[Riccardo Brasca]

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

[Adam Topaz]

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

/-- 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∥ })
  (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) :
  N.is_bdd_exact_for_bdd_degree_above_idx (k^3 + k) (m-1) c₀ :=
begin
  intros c hc i hi n,
  set k_new := k^3 + k with hknew,
  suffices : ∃ (y : N.X c i), ∀ ε : ℝ≥0, 0 < ε → ∥ N.res n - N.d y ∥ ≤ (k_new + ε) * ∥ N.d n ∥,
  { rcases this with ⟨y, hy⟩,
    use y,
    have : ↑k_new * ∥ N.d n ∥ = Inf { r | ∃ (ε : ℝ≥0) (hε : 0 < ε), r = (k_new + ε) * ∥ N.d n ∥},
    { refine le_antisymm _ _,
      { rw real.le_Inf,
        { rintros z ⟨ε,hε,rfl⟩,
          simp only [le_add_iff_nonneg_right, add_mul],
          exact mul_nonneg (le_of_lt hε) (by simp) },
        { use (k_new + 1) * ∥ N.d n ∥,
          refine ⟨1, zero_lt_one, rfl⟩ },
        { use k_new * ∥ N.d n ∥,
          rintro y ⟨ε,hε,rfl⟩,
          simp only [le_add_iff_nonneg_right, add_mul],
          exact mul_nonneg (le_of_lt hε) (by simp) } },
      { sorry } },
    rw this,
    rw real.le_Inf,
    { rintros r ⟨ε,hε,rfl⟩,
      exact hy _ hε },
    { use (k_new + 1) * ∥ N.d n ∥,
      refine ⟨1, zero_lt_one, rfl⟩ },
    { use k_new * ∥ N.d n ∥,
      rintros y ⟨ε,hε,rfl⟩,
      simp only [le_add_iff_nonneg_right, add_mul],
      exact mul_nonneg (le_of_lt hε) (by simp) } },
  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

[Adam Topaz]

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

[Adam Topaz]

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.

[Adam Topaz]

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

[Riccardo Brasca]

It seems good to me

[Adam Topaz]

Okay great :)

[Adam Topaz]

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

[Riccardo Brasca]

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'

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Adam Topaz]

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

[Adam Topaz]

Trying to update mathlib now...

[Riccardo Brasca]

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

[Adam Topaz]

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

[Riccardo Brasca]

How can I update mathlib?

[Adam Topaz]

I used leanproject upgrade-mathlib

[Adam Topaz]

@Riccardo Brasca This is a mess....

LONG

/-- 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∥ })
  (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) :
  N.is_bdd_exact_for_bdd_degree_above_idx (k^3 + k) (m-1) c₀ :=
begin
  intros c hc i hi n,
  set k_new := k^3 + k with hknew,
  suffices : ∃ (y : N.X c i), ∀ ε : ℝ, 0 < ε → ∥ N.res n - N.d y ∥ ≤ (k_new + ε) * ∥ N.d n ∥,
  { rcases this with ⟨y, hy⟩,
    use y,
    have : ↑k_new * ∥ N.d n ∥ = Inf { r | ∃ (ε : ℝ) (hε : 0 < ε), r = (k_new + ε) * ∥ N.d n ∥},
    { refine le_antisymm _ _,
      { rw real.le_Inf,
        { rintros z ⟨ε,hε,rfl⟩,
          simp only [le_add_iff_nonneg_right, add_mul],
          exact mul_nonneg (le_of_lt hε) (by simp) },
        { use (k_new + 1) * ∥ N.d n ∥,
          refine ⟨1, zero_lt_one, rfl⟩ },
        { use k_new * ∥ N.d n ∥,
          rintro y ⟨ε,hε,rfl⟩,
          simp only [le_add_iff_nonneg_right, add_mul],
          exact mul_nonneg (le_of_lt hε) (by simp) } },
      { by_cases ∥ N.d n ∥ ≤ 0,
        { simp at h,
          simp only [h, norm_zero, exists_and_distrib_right, mul_zero],
          have : {r : ℝ | ∃ (ε : ℝ) (hε : 0 < ε), r = 0 } = {0},
          { ext t,
            refine ⟨λ ⟨r,hr,h⟩, h, λ ht, ⟨1,zero_lt_one, ht⟩⟩ },
          rw this,
          simp },
        apply le_of_forall_pos_le_add,
        intros ε hε,
        apply real.Inf_le,
        { use k_new * ∥ N.d n ∥,
          rintro y ⟨ε,hε,rfl⟩,
          simp only [le_add_iff_nonneg_right, add_mul],
          exact mul_nonneg (le_of_lt hε) (by simp) },
        { use ε / ∥ N.d n ∥,
          simp at h,
          split,
          apply div_pos hε,
          rwa norm_pos_iff,
          simp [add_mul],
          field_simp [h] } } },
    rw this,
    rw real.le_Inf,
    { rintros r ⟨ε,hε,rfl⟩,
      exact hy _ hε },
    { use (k_new + 1) * ∥ N.d n ∥,
      refine ⟨1, zero_lt_one, rfl⟩ },
    { use k_new * ∥ N.d n ∥,
      rintros y ⟨ε,hε,rfl⟩,
      simp only [le_add_iff_nonneg_right, add_mul],
      exact mul_nonneg (le_of_lt hε) (by simp) } },
  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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Adam Topaz]

Ah right.

[Adam Topaz]

Let me fix that. one sec.

[Adam Topaz]

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

[Adam Topaz]

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

[Riccardo Brasca]

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?

[Riccardo Brasca]

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

[Riccardo Brasca]

OK, that's what you did, sorry

[Riccardo Brasca]

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)

[Riccardo Brasca]

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

[Adam Topaz]

Yeah exactly. This is what I was worried about.

[Adam Topaz]

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

[Riccardo Brasca]

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

[Peter Scholze]

Ah!

[Peter Scholze]

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

[Peter Scholze]

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

[Peter Scholze]

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.

[Peter Scholze]

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'/M$ is implicitly completed. Then I think 9.10 stays true as stated, except that one may have to replace $k^3+k$ by something slightly different.

[Peter Scholze]

I'll try to update the file tomorrow

[Sebastien Gouezel]

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 $(x_n) \mapsto \sum 2^{-n} x_n$, for instance.

[Sebastien Gouezel]

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

[Peter Scholze]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Peter Scholze]

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

[Peter Scholze]

(If I had to change the definition of $\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...)

[Riccardo Brasca]

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 $f$.

[Adam Topaz]

So it sounds like we should introduce the category CompleteNormedGroup?

[Johan Commelin]

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

[Riccardo Brasca]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Johan Commelin]

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

[Peter Scholze]

Peter Scholze said:

(If I had to change the definition of $\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 $\leq k$-exactness, weaken the condition to say that for all $\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 $\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 $k$ by $k^2+1$ or so. In this sense, the statements with the weak notion of $\leq k$-exactness, stated without completeness hypothesis, and the statements with strong notion of $\leq k$-exactness, stated with completeness hypothesis, are equivalent (up to slightly changing $k$). It is not clear to me which one is easier to formalize; maybe there's not much difference?

[Riccardo Brasca]

In my opinion proposition 9.10 with the $+ \varepsilon$-definition of $\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.

[Adam Topaz]

I would be inclined to use complete normed groups. If we change the definition of $\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.

[Riccardo Brasca]

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.

[Riccardo Brasca]

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

[Riccardo Brasca]

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.

[Riccardo Brasca]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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.

[Johan Commelin]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

Now I think it's OK :upside_down:

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Kevin Buzzard]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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.

[Kevin Buzzard]

I'm filling in some sorries

[Riccardo Brasca]

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

[Kevin Buzzard]

I'm just methodically killing them in dull ways

[Kevin Buzzard]

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.

[Kevin Buzzard]

i killed a few but now I have to stop too

[Alex J. Best]

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₁,

[Riccardo Brasca]

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

[Damiano Testa]

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!

[Johan Commelin]

@Damiano Testa certainly!

[Johan Commelin]

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

[Johan Commelin]

but feel free to also look at the other sorrys

[Johan Commelin]

I'll send you an invite for the repo

[Damiano Testa]

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

[Riccardo Brasca]

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:

[Johan Commelin]

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

[Riccardo Brasca]

@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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

(after merging what you have done)

[Riccardo Brasca]

semicomplete = the sorrys are unrelated to the snake lemma

[Adam Topaz]

Okay, pushed.

[Adam Topaz]

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

[Riccardo Brasca]

I just pushed the proof

[Adam Topaz]

Oh :)

[Riccardo Brasca]

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

[Riccardo Brasca]

Of course the proof can probably be golfed a lot

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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.

[Adam Topaz]

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

[Kevin Buzzard]

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

[Johan Commelin]

9.7

[Johan Commelin]

I'm working on the statement of 9.8

[Johan Commelin]

And people can start looking at the statement of 9.6

[Johan Commelin]

now that snake is almost ready

[Johan Commelin]

we'll need double complexes for that

[Johan Commelin]

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

[Riccardo Brasca]

@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

[Adam Topaz]

Okay, I killed the easy sorrys in the proof.

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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? :)

[Riccardo Brasca]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Johan Commelin]

ok, sure

[Riccardo Brasca]

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

[Johan Commelin]

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.

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Johan Commelin]

whatever you like best

[Johan Commelin]

In principle git should allow us to fix anything we break

[Alex J. Best]

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.

[Johan Commelin]

Thanks!

[Riccardo Brasca]

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:

[Alex J. Best]

Did you paste it into the system_of_complexes namespace or after?

[Alex J. Best]

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

[Riccardo Brasca]

Thank you, now it works

[Riccardo Brasca]

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

[Riccardo Brasca]

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)

[Riccardo Brasca]

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

[Johan Commelin]

lgtm

[Johan Commelin]

let's merge it into master

[Johan Commelin]

any other fixes can be done afterwards

[Johan Commelin]

merged, pushed

[Johan Commelin]

@Riccardo Brasca thanks for all the great work!

[Riccardo Brasca]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Riccardo Brasca]

except that you probably mean complete instead of compact I agree

[Riccardo Brasca]

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)

[Riccardo Brasca]

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

[Johan Commelin]

res_apply is done

[Riccardo Brasca]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

Note that I had to upgrade mathlib to use le_of_forall_pos_le_add

[Riccardo Brasca]

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

[Johan Commelin]

@Riccardo Brasca how did you upgrade mathlib?

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

leanproject upgrade-mathlib

[Johan Commelin]

Does git status show you uncommitted changes?

[Riccardo Brasca]

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

[Riccardo Brasca]

I am pushing it

[Johan Commelin]

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:

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

@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).

[Johan Commelin]

Feel free to merge

[Riccardo Brasca]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Riccardo Brasca]

@Kevin Buzzard Thank's for the explanation!

[Kevin Buzzard]

When I was a PhD student we used to get 2400

[Riccardo Brasca]

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

[Johan Commelin]

Great job!

[Peter Scholze]

Great!

[Johan Commelin]

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

[Peter Scholze]

Yes, that's right

[Peter Scholze]

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

[Peter Scholze]

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

[Johan Commelin]

Ok, thanks for pointing that out

[Peter Scholze]

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)

[Johan Commelin]

certainly

[Peter Scholze]

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

[Johan Commelin]

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

[Patrick Massot]

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.

[Johan Commelin]

I think it's also about explicit bounds

[Riccardo Brasca]

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

[Peter Scholze]

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

[Peter Scholze]

@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 $k$ (and $N$, $c$ etc., in the proof of 9.5), have to be. The input variables are, I guess, $r$, $r'$ and $m$.

[Patrick Massot]

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.

[Peter Scholze]

I agree

[Patrick Massot]

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))$" 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))$", right? (I'm inventing stupid formulas here, not claiming anything)

[Peter Scholze]

Yes, that's what I have in mind. (Unfortunately, everything will also depend on the auxiliary constants $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.)

[Patrick Massot]

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

[Riccardo Brasca]

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 $\leq k$-exact is $\leq ?$-exact. This seemed easy yesterday, but now I am a little lost.

[Peter Scholze]

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

[Peter Scholze]

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

[Riccardo Brasca]

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

[Peter Scholze]

Sure, admissibility is always assumed

[Peter Scholze]

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

[Peter Scholze]

Hmm... maybe one has to prove 9.4 and 9.5 directly for profinite $S$, which seems fine -- in the key lemma 9.8, one can indeed make the passage from finite $S$ to profinite $S$ 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!!)

[Johan Commelin]

No worries! You should blame Lean (-;

[Peter Scholze]

Of course this is exactly what I was hoping for!

[Johan Commelin]

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.

[Peter Scholze]

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

[Riccardo Brasca]

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)

[Peter Scholze]

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 $k$ by some other constant like $k^4+k^2$ or whatever.

In general, any element of the completion $x$ can be written as $x=x_0+x_1+\ldots$ with $||x_i||\leq C 2^{-i}$. Then one can find $y_i$ with with $||\mathrm{res}(x_i)-d(y_i)||\leq k||d(x_i)||+2^{-i}$. In that case, $||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 $z_i$ such that $||\mathrm{res}(y_i)-d(z_i)||\leq (k((k+1)C+1)+1)2^{-i}$. Let $y_i'=\mathrm{res}(y_i)-d(z_i)$. Then $||\mathrm{res}^2(x_i)-d(y_i')||\leq k||d(x_i)||+2^{-i}$ and $||y_i'||\leq (k((k+1)C+1)+1)2^{-i}$. Thus $y'=y_0'+y_1'+\ldots$ exists and $||\mathrm{res}^2(x)-d(y')||\leq k||d(x)|| + 1$. Replacing $1$ by $\epsilon$ in this argument, one gets weak exactness of the completed complex, with $k$ replaced by $k^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$, then one can find $y$ such that $\mathrm{res}(x)=d(y)$. We know that for all $i$, we can find $y_i$ such that $||\mathrm{res}(x)-d(y_i)||\leq 2^{-i}$. For each $i$, we have in particular $||d(y_i-y_{i+1})||\leq 2^{1-i}$, and by using weak exactness one degree lower, we can find $z_i$ such that $||\mathrm{res}(y_i-y_{i+1})-d(z_i)||\leq (k+1)2^{1-i}$. Let $y_i'=\mathrm{res}(y_i)+d(z_i)+d(z_{i+1})+\ldots$. Then one has $||\mathrm{res}^2(x)-d(y_i')||\leq 2^{-i}$ as $d^2=0$, while the $y_i'$ form a Cauchy sequence. We can thus define $y'$ as the limit of the $y_i'$, and then get in the limit $\mathrm{res}^2(x)=d(y')$.

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

[Peter Scholze]

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

[Riccardo Brasca]

I will try to formalize :)

[Peter Scholze]

That should settle it hopefully! :-)

[Peter Scholze]

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

[Peter Scholze]

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 $k$ by some other constant like $k^4+k^2$ or whatever. [...]

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

[Peter Scholze]

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 $S$. 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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Peter Scholze]

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

[Peter Scholze]

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 $k$ by some other constant like $k^4+k^2$ or whatever.

Modified:

In general, any element of the completion $x$ can be written as $x=x_0+x_1+\ldots$ with $||x_i||\leq C 2^{-i}$. Then one can find $y_i$ with with $||\mathrm{res}(x_i)-d(y_i)||\leq k||d(x_i)||+2^{-i}$. In that case, $||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 $z_i$ such that $||\mathrm{res}(y_i)-d(z_i)||\leq (k((k+1)C+1)+1)2^{-i}$. Let $y_i'=\mathrm{res}(y_i)-d(z_i)$. Then $||\mathrm{res}^2(x_i)-d(y_i')||\leq k||d(x_i)||+2^{-i}$ and $||y_i'||\leq (k((k+1)C+1)+1)2^{-i}$. Thus $y'=y_0'+y_1'+\ldots$ exists and $||\mathrm{res}^2(x)-d(y')||\leq k||d(x)|| + 1$. Replacing $1$ by $\epsilon$ in this argument, one gets weak exactness of the completed complex, with $k$ replaced by $k^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$, then one can find $y$ such that $\mathrm{res}(x)=d(y)$. We know that for all $i$, we can find $y_i$ such that $||\mathrm{res}(x)-d(y_i)||\leq 2^{-i}$. For each $i$, we have in particular $||d(y_i-y_{i+1})||\leq 2^{1-i}$, and by using weak exactness one degree lower, we can find $z_i$ such that $||\mathrm{res}(y_i-y_{i+1})-d(z_i)||\leq (k+1)2^{1-i}$. Let $y_i'=\mathrm{res}(y_i)-d(z_{i-1})-\ldots-d(z_0)$. Then one has $||\mathrm{res}^2(x)-d(y_i')||\leq 2^{-i}$ as $d^2=0$, while the $y_i'$ form a Cauchy sequence. We can thus define $y'$ as the limit of the $y_i'$, and then get in the limit $\mathrm{res}^2(x)=d(y')$.

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

[Riccardo Brasca]

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

[Johan Commelin]

See tsum, there is quite a lot about it

[Kevin Buzzard]

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.

[Riccardo Brasca]

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

[Johan Commelin]

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

[Adam Topaz]

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.

[Riccardo Brasca]

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

[Riccardo Brasca]

It seems something like if $x_n \to x$ then consider the sequence $x_0, x_1-x_0, x_2-(x_0 + x_1), \ldots$

[Adam Topaz]

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

[Heather Macbeth]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Heather Macbeth]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Heather Macbeth]

Peter Scholze said:

In general, any element of the completion $x$ can be written as $x=x_0+x_1+\ldots$ with $||x_i||\leq C 2^{-i}$. Then one can find $y_i$ with with $||\mathrm{res}(x_i)-d(y_i)||\leq k||d(x_i)||+2^{-i}$. In that case, $||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 $z_i$ such that $||\mathrm{res}(y_i)-d(z_i)||\leq (k((k+1)C+1)+1)2^{-i}$. Let $y_i'=\mathrm{res}(y_i)-d(z_i)$. Then $||\mathrm{res}^2(x_i)-d(y_i')||\leq k||d(x_i)||+2^{-i}$ and $||y_i'||\leq (k((k+1)C+1)+1)2^{-i}$. Thus $y'=y_0'+y_1'+\ldots$ exists and $||\mathrm{res}^2(x)-d(y')||\leq k||d(x)|| + 1$. Replacing $1$ by $\epsilon$ in this argument, one gets weak exactness of the completed complex, with $k$ replaced by $k^2$.

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

[Johan Commelin]

yep

[Riccardo Brasca]

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

[Johan Commelin]

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

[Riccardo Brasca]

Sorry, there is no $f$

[Riccardo Brasca]

The same is true for $d$

[Heather Macbeth]

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

[Heather Macbeth]

And docs#has_sum.norm_le_of_bounded would control its norm.

[Sebastien Gouezel]

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.

[Heather Macbeth]

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

[Riccardo Brasca]

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)

[Patrick Massot]

Riccardo Brasca said:

It seems something like if $x_n \to x$ then consider the sequence $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 $x$, and starts at zero for convenience. Then extract a sub sequence that converges sufficient fast (still starting at zero) and set $x_n = y_{n+1} - y_n$.

[Patrick Massot]

I you need that argument I could formalize it.

[Adam Topaz]

Patrick Massot said:

Riccardo Brasca said:

It seems something like if $x_n \to x$ then consider the sequence $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 $x$, and starts at zero for convenience. Then extract a sub sequence that converges sufficient fast (still starting at zero) and set $x_n = y_{n+1} - y_n$.

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

[Patrick Massot]

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

[Patrick Massot]

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

[Adam Topaz]

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

[Adam Topaz]

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.

[Patrick Massot]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Adam Topaz]

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

[Peter Scholze]

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 $k$ (which is harmless)

[Peter Scholze]

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

[Peter Scholze]

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

[Adam Topaz]

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

[Peter Scholze]

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

[Riccardo Brasca]

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

[Adam Topaz]

Won't the $C$ depend on $k$?

[Riccardo Brasca]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Peter Scholze]

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

[Riccardo Brasca]

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

[Adam Topaz]

:face_palm: yes of course

[Patrick Massot]

So this is what I wrote, right?

[Peter Scholze]

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

[Patrick Massot]

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

[Peter Scholze]

sure!

[Adam Topaz]

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

[Peter Scholze]

Yes

[Peter Scholze]

I think you can take the norm of $x$

[Riccardo Brasca]

The point is that the norm of $x_i$ shouldn't explode

[Riccardo Brasca]

@Patrick Massot 's proof looks good to me

[Patrick Massot]

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

[Peter Scholze]

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

[Patrick Massot]

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

[Johan Commelin]

can you filterize the statement?

[Patrick Massot]

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.

[Peter Scholze]

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

[Patrick Massot]

Indeed Johan, that means filters.

[Riccardo Brasca]

@Johan Commelin In the project normed_group means that $||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

[Adam Topaz]

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

[Adam Topaz]

docs#norm_eq_zero

[Riccardo Brasca]

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

[Peter Scholze]

Which change?

[Peter Scholze]

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

[Peter Scholze]

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

[Riccardo Brasca]

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

[Peter Scholze]

I think Johan Commelin is working on the pseudo-normed things; to be able to go cleanly from $\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 $\bullet_{\leq c}$ is a profinite set)

[Riccardo Brasca]

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

[Peter Scholze]

This will not come up!

[Peter Scholze]

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

[Riccardo Brasca]

Even better!

[Johan Commelin]

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

[Johan Commelin]

oops, I had a lot of lag... so I missed the discussion above. Ignore my message

[Johan Commelin]

@Riccardo Brasca If you search for pseudo_normed_group in the repo, then you'll see that we already have it (-;

[Johan Commelin]

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 $\hat V$ and builds the system of complexes (of "ordinary" complete normed groups)

[Riccardo Brasca]

@Adam Topaz Are you working on weak exactness implies exactness? If not I can start doing it, assuming the lemma about writing $x$ as a sum of terms with controlled norm

[Peter Scholze]

I'll be a little relieved when that lemma is formalized :wink:

[Adam Topaz]

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

[Riccardo Brasca]

I would be happy to fill some sorry

[Adam Topaz]

@Riccardo Brasca :down:

long

#check cauchy_seq_tendsto_of_complete

lemma d_res_commute {c c' : ℝ≥0} [fact (c' ≤ c)] {i} {x : C.X c i} : C.d (C.res x : C.X c' i) = C.res (C.d x) :=
begin
  sorry,
end

theorem weak_iff_strong_of_complete {δ : ℝ≥0} [fact (0 < δ)] {k : ℝ≥0} {m : ℤ} [hk : fact (1 ≤ k)] {c₀ : ℝ≥0}
  [∀ c i, complete_space (C.X c i)] (adm : C.admissible) :
  is_weak_bdd_exact_for_bdd_degree_above_idx C k m c₀ → is_bdd_exact_for_bdd_degree_above_idx C (k^2 + δ) m c₀ :=
begin
  intros cond c hc i hi x,
  have cond' := cond,
  letI : fact (k * (k * c) ≤ (k^2 + δ) * c) := sorry,
  letI : fact (k * c ≤ (k^2 + δ) * c) := sorry,
  specialize cond (k * (c)) _ i hi (C.res x),
  by_cases hh : 0 < ∥ C.d x ∥,
  { sorry },
  simp at hh,
  simp [hh],
  let f := λ (j : ℤ), classical.some (cond ((1 : ℝ) / 2^j) _),
  have hf : ∀ (j : ℤ), ∥ C.d (f j - f (j+1)) ∥ ≤ (2 : ℝ) / 2^j,
  { /-
    intros j,
    rw (show C.d (f j - f (j+1)) = (C.res x - C.d (f (j+1))) + -(C.res x - C.d (f j)), by simp),
    rw (show (2 : ℝ)/2^j = 1 / 2^j + 1 / 2^j, by ring),
    refine le_trans (norm_add_le _ _) (add_le_add _ _),
    refine le_trans _ (_ : (1 : ℝ) / 2^(j+1) ≤ _),
    convert classical.some_spec (cond ((1 : ℝ) / 2^(j + 1)) _),
    simp,
    simp,
    right,
    rw [d_res_commute, hh],
    simp,
    sorry,
    rw norm_neg,
    convert classical.some_spec (cond ((1 : ℝ) / 2^j) _),
    simp,
    simp,
    right,
    rw [d_res_commute, hh],
    simp,
    -/
    sorry,
  },
  have hi : i = i - 1 + 1, by ring,
  let ff : ℤ → C.X (k * c) (i - 1 + 1) := λ i, eq.rec (f i - f (i+1)) hi,
  specialize cond' c hc (i-1) _,
  let g := λ (j : ℤ), classical.some (cond' (ff j) (k * 2 / 2^j) _),
  have hg : ∀ (j : ℤ), ∥ C.res (ff j) - C.d (g j) ∥ ≤ k * 2^2 / 2^j,
  { intros j,
    have := classical.some_spec (cond' (ff j) (k * 2 / 2^j) _),
    refine le_trans this _,
    rw (show ((k : ℝ)) * 2^2 / 2^j = k * 2 / 2^j + k * 2 / 2^j, by ring),
    simp,
    refine mul_le_mul _ _ _ _,
    sorry,
    --refine le_trans (hf j) _, -- we now have eq.rec issues :(
    sorry,
    simp,
    norm_cast,
    simp },

  sorry,
end

[Adam Topaz]

Feel free to build on it and/or completely ignore it!

[Adam Topaz]

I didn't get very far.

[Adam Topaz]

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 $k \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).

[Adam Topaz]

Oh, and the #check cauchy_seq_tendsto_of_complete at the top was just for myself to remember the name of this useful lemma :)

[Riccardo Brasca]

d_res_commute is already there, it is called d_res

[Adam Topaz]

Yeah, I figured we had it somewhere, but was too lazy to search.

[Riccardo Brasca]

library_search found it for me :)

[Adam Topaz]

I guess I was REALLY lazy then! :rofl:

[Riccardo Brasca]

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

[Adam Topaz]

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.

[Riccardo Brasca]

Mmh, yeah, here it can be inevitable

[Johan Commelin]

There is C.congr to help with these annoyances

[Adam Topaz]

Johan Commelin said:

There is C.congr to help with these annoyances

Good to know!

[Riccardo Brasca]

Sure, it is not a serious problem, but we are lazy :D

[Riccardo Brasca]

@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 "...$||\mathrm{res}^2(x)-d(y')||\leq k||d(x)|| + 1$". We can write $x = \sum x_i$ and $y' = \sum y_i'$, so we get $||\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 $2$'s are not a problem, we can put $\varepsilon$ instead, but $C$ is there. We can probably take $C= ||x||$ or something similar, but $d(x)$ can be $0$. I didn't check if the argument in the second part of your post can deal with this case since you wrote $\ldots \leq k||d(x)|| + 1$. Am I missing something?

[Riccardo Brasca]

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/normed.20snake.20lemma
I can at least put a link :)

[Peter Scholze]

Sorry, I guess one should choose the sequence better, so that $||x-x_0||$ is already very small. Then $||d(x_0)||$ is close to $||d(x)||$, and the rest of the $||d(x_i)||$ also contribute little.

[Riccardo Brasca]

Ah yes, that seems to work. Analysis was easier when I was a student :rolling_eyes:

[Riccardo Brasca]

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

[Patrick Massot]

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.

[Riccardo Brasca]

I wrote Peter's argument that weak $\leq k$-exactness implies weak $\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 $x$ a sum of elements in the uncompleted group, we really need the three properties (in particular we need that $x^0$ is close enough to $x$).
• we need to prove that, under admissibility, d and res are continuous and hence commutes with infinite sum.

[Johan Commelin]

thanks a lot for doing this!

[Riccardo Brasca]

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 $\leq k$ exact stuff is $\leq k^3 + k$ weak exact.
• The version in the pdf says: completion of quotient of complete $\leq k$ exact stuff is $\leq \max(k^4 , k^3 +k + 1)$ exact.
• Weak $\leq k$ exactness implies weak $\leq k^2$ exactness of completion.
• Weak $\leq k$ exactness and complete implies $\leq k^2 + \delta$ exactness
• Together, the last two points give that weak $\leq k$ exactness implies $\leq k^4 + \delta$ exactness of completion. (We can probably modify the proof to obtain $\leq k^2 + \delta$ exactness).
  Now, in the strong snake lemma we assume $M$ and $M'$ to be complete and $\leq k$ exacts, but the weak version gives weak $\leq k^3 + k$ exactness of $N$, so $\leq (k^3+k)^4 + \delta$ exactness of $\bar N$. Even if we get to $\leq (k^3+k)^2 + \delta$ exactness, this is worst than $\leq \max(k^4 , k^3 +k + 1)$ exactness.

Now I am confused :thinking:

[Riccardo Brasca]

Especially since the proof of the preliminary observation seems really easier then the other arguments

[Peter Scholze]

@Riccardo Brasca The point is that 9.10 will be applied very often, while that final argument will be applied precisely once

[Peter Scholze]

Also, in the file one has to seriously use profinite $S$ now, while in what Johan stated as the goal, finite $S$ are enough

[Peter Scholze]

(one could also make a reduction to finite $S$, but it would then once more require that thing you just formalized

[Peter Scholze]

I'm very glad this worked, by the way!

[Riccardo Brasca]

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

[Patrick Massot]

I just pushed a proof of the controlled sum thing. Riccardo, could you check this is what you need?

[Peter Scholze]

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 $S$ 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 $S$ is finite.

b) It does give better constants. You observed that 9.10 gives roughly $k^3$ vs. roughly $k^4$, while that argument for weak exact => exact raises $k$ 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.

[Riccardo Brasca]

@Patrick Massot That's seems perfect, thank you!

[Riccardo Brasca]

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 $k^{12}$ instead of the current $k^4$), but what you propose is to use weak exactness everywhere and at the very end go to strong exactness.

[Peter Scholze]

Exactly, everything is weak up until the very end

[Peter Scholze]

By "weak exact => exact for complete" you could always at will pass to the strong version, but this would cost some constants

[Riccardo Brasca]

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 $x$ as a sum) has been done by Patrick, the rest is very elementary but with a lot of small calculations.

[Patrick Massot]

It all looks straightforward to formalize. I don't say it will be fun, but it looks totally doable without too much thinking.

[Riccardo Brasca]

This is very possible! But I remember when I literally spent two hours to prove that $\{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:

[Mario Carneiro]

it has 7 tho

[Riccardo Brasca]

ROTF

[Patrick Massot]

That's what we call number theorists those days...

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

But now I should go to bed.

[Riccardo Brasca]

As you said this is not going to be fun, so I prefer that someone else check that this is really what we want

[Johan Commelin]

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.

[Johan Commelin]

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.

[Johan Commelin]

@Riccardo Brasca Does this weakened hypothesis look plausible to you?

[Johan Commelin]

I didn't yet look into whether the proof can easily be refactored

[Riccardo Brasca]

I will have a look at it later today, but I think we have everything we need to refactor the proof

[Riccardo Brasca]

Concerning the refactor using the kernel of g, we should first of all prove that if $0 \to M_1 \to M_2 \to M_3 \to$ is exact (in some sense) then $M_3$ is isomorphic to the quotient $M_2/M_1$. Another possibility is to prove the lemma directly for the quotient, without introducing a new complex

[Johan Commelin]

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.

[Kevin Buzzard]

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

[Riccardo Brasca]

@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₀ :=

[Johan Commelin]

Yes, I did that part

[Johan Commelin]

@Riccardo Brasca But we need another refactor, namely hg should be weakened

[Riccardo Brasca]

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

[Johan Commelin]

@Riccardo Brasca Sounds good! It is one of the missing bits to complete the proof of 9.6.

[Riccardo Brasca]

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

[Riccardo Brasca]

Ah, I see you also said that in the end we don't really need the weak version

[Johan Commelin]

@Peter Scholze What do you think? Should we just assume completeness everywhere?

[Peter Scholze]

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

[Peter Scholze]

where do you now use completeness?

[Peter Scholze]

(Not using completeness should give slightly better constants in the end; I think this was the main argument for not assuming it.)

[Johan Commelin]

The constants can't get worse by adding the extra assumption, right?

[Peter Scholze]

Hmm they can, because the snake lemma more easily gives weak exactness than strong exactness

[Peter Scholze]

or do you mean assume completeness + strong exactness?

[Johan Commelin]

In the normed snake lemm we have $M \stackrel{f}{\to} M' \stackrel{g}{\to} N$ and we assume $\text{im}(f) = \text{ker}(g)$.

[Riccardo Brasca]

Concerning the normed snake lemma we have a version (completely proved) for weak exactness, that assumes that the image of f is closed

[Peter Scholze]

wait, why should the image of f be closed?

[Johan Commelin]

But I think we need $\ker(g) = \overline{\text{im}(f)}$

[Johan Commelin]

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.

[Peter Scholze]

hmm wait

[Peter Scholze]

it's OK

[Johan Commelin]

Peter Scholze said:

or do you mean assume completeness + strong exactness?

I meant assume completeness + weak exactness, and prove weak exactness.

[Peter Scholze]

In the inductive step of 9.6, you just shouldn't take the quotient by the closure of the image

[Peter Scholze]

Just take the quotient by the image

[Johan Commelin]

But then the quotient isn't a normed group, is it?

[Peter Scholze]

I was only taking the closure to keep things complete (as in the manuscript, everything is complete, and I want strong exactness)

[Peter Scholze]

It is, I think

[Johan Commelin]

Ooh, in your generalised sense!

[Johan Commelin]

Wait, I'm confused...

[Peter Scholze]

What's the Lean definition of a normed group?

[Johan Commelin]

Right, you can't prove $\||x = 0\|| \iff x = 0$ if the subgroup isn't closed

[Peter Scholze]

Yes

[Johan Commelin]

And lean assumes that axiom

[Peter Scholze]

Ah

[Peter Scholze]

But it doesn't assume completeness?

[Johan Commelin]

Nope

[Johan Commelin]

So separated, but not complete

[Peter Scholze]

Right

[Peter Scholze]

That's a weird convention then

[Johan Commelin]

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

[Johan Commelin]

I think it is because with this definition you can extends metric_space

[Peter Scholze]

wait, a metric space also requires that?

[Johan Commelin]

Yes....

[Peter Scholze]

Weird... OK

[Johan Commelin]

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

[Peter Scholze]

It seems that this is also the wikipedia definition

[Johan Commelin]

The second axiom

[Peter Scholze]

right

[Johan Commelin]

In Leiden they also taught me that axiom for metric spaces

[Peter Scholze]

It may very well be the standard

[Johan Commelin]

@Sebastien Gouezel @Heather Macbeth what do you think... does it make sense to relax this axiom in mathlib?

[Riccardo Brasca]

Maybe I am confused, but $d(x,y) = 0 \Rightarrow x = y$ seems pretty standard :thinking:

[Peter Scholze]

I think algebraic geometers somehow got off the normal tracks when they changed from "prescheme/scheme" to "scheme/separated scheme"

[Johan Commelin]

@Patrick Massot Can we easily see how much of the library we need to duplicate if we want to roll our own normed_group?

[Riccardo Brasca]

We can just call it seminormed_group...

[Johan Commelin]

Sure, but how many library lemmas do we need to reprove?

[Riccardo Brasca]

Just joking :sweat_smile:

[Johan Commelin]

@Peter Scholze But if we use weak exactness + complete normed groups, the constants should still be the good ones

[Peter Scholze]

Hmm, I guess so

[Johan Commelin]

And for the final application it doesn't matter either

[Johan Commelin]

So that might be the easy way out (-;

[Peter Scholze]

Hmm, OK, then indeed one has to modify 9.10 a bit to incorporate some passage to the completion

[Peter Scholze]

I think that would actually make the constants slightly worse there

[Julian Külshammer]

I saw this being called a pseudometric space https://en.m.wikipedia.org/wiki/Pseudometric_space

[Sebastien Gouezel]

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

[Johan Commelin]

@Sebastien Gouezel But if we call them pseudometric_space?

[Johan Commelin]

85% of the lemmas will still be about metric_space, but some of the general facts can be proven for pseudometric_space

[Sebastien Gouezel]

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.

[Peter Scholze]

OK, I think that should be the solution: Just also introduce pseudometric_space and seminormed_group and use these things instead

[Johan Commelin]

And similarly, we could then have seminormed_group. (It seems that pseudo_normed_group has recently be claimed...)

[Johan Commelin]

Ok, great. Then we don't change the normed snake lemma.

[Johan Commelin]

Any volunteers for the refactor? Otherwise I'll do it when I don't have inspiration for something else.

[Peter Scholze]

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

[Riccardo Brasca]

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?

[Sebastien Gouezel]

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

[Johan Commelin]

@Riccardo Brasca The current version is fine with the generalised definitions

[Peter Scholze]

We can't assume that f has closed image. But we shouldn't need it...

[Johan Commelin]

Because we can then drop is_closed from the instance of seminormed_group for quotients

[Damiano Testa]

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

[Riccardo Brasca]

Ah sure! In that case I will give a try to the refactor!

[Riccardo Brasca]

What is the general strategy? Introduce pseudometric_space and check by hand what stay true in this generality?

[Johan Commelin]

One complication is whether we also want pseudo_emetric_space...

[Johan Commelin]

(allowing $\infty$ as distance)

[Johan Commelin]

@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

[Peter Scholze]

I don't think infinite distances are relevant to what we're doing here... maybe leave that for another day then?

[Johan Commelin]

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

[Julian Külshammer]

A pseudo_emetric shows for example up in topological data analysis.

[Peter Scholze]

I didn't expect topological data analysis to come up in this stream ;-)

[Riccardo Brasca]

Apperently in mathlib these things are called docs#premetric_space

[Johan Commelin]

Ooh! So we have them already in some sense?

[Johan Commelin]

That means we only need to do the seminormed_group stuff?

[Riccardo Brasca]

Not really, nothing is proved for them, but at least we don't have to chose the name :D

[Johan Commelin]

Should we call them prenormed_group as well?

[Johan Commelin]

Because seminormed_group sounds like it might have something to do with seminorms

[Johan Commelin]

Which isn't really the point that we try to make

[Peter Scholze]

Isn't this exactly a seminorm?

[Riccardo Brasca]

I thought a seminorm was exactly a norm without the assumption that $||x|| = 0 \Rightarrow x=0$

[Peter Scholze]

Also, "pseudometric space" seems the standard name in the literature, so why use "premetric space" instead?

[Johan Commelin]

ooh, you are right. so seminormed_group it is! :face_palm:

[Sebastien Gouezel]

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.

[Johan Commelin]

We can rename premetric_space

[Sebastien Gouezel]

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

[Peter Scholze]

It is! But those seem to be the standard names...

[Riccardo Brasca]

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

[Johan Commelin]

Are there pre_emetric_spaces already? Otherwise, I think you can choose to skip that step. Whichever you prefer.

[Riccardo Brasca]

No, there aren't, but it doesn't seem very complicated to do both

[Riccardo Brasca]

If someone wants to have a look I created #6694, for extended pseudo metric spaces.

[Johan Commelin]

Thanks, I left 1 comment (-;

[Johan Commelin]

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!

[Riccardo Brasca]

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

[Johan Commelin]

Yes, leanproject up should get you started. But there might be unexpected breakage.

[Johan Commelin]

So I can help with bumping mathlib, if you want.

[Johan Commelin]

Hmm, we need to wait a bit longer. @Riccardo Brasca

[Johan Commelin]

The oleans aren't available yet.

[Riccardo Brasca]

No problem :)

[Johan Commelin]

Now they are there, it seems

[Riccardo Brasca]

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

[Johan Commelin]

I'll look at the other errors

[Johan Commelin]

Is your branch clean?

[Johan Commelin]

Or is there other stuff on it too, that might make a merge a bit more complicated?

[Riccardo Brasca]

I created a new branch, but it's very possibile that I messed up with leanproject build.

[Riccardo Brasca]

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

[Johan Commelin]

No, I got the same.

[Johan Commelin]

That file moved in mathlib. I'm fixing those errors in LTE right now (-;

[Johan Commelin]

@Riccardo Brasca I've pushed some fixes to bump-mathlib-2021-04-06

[Johan Commelin]

But now the errors are about NormedGroup and such

[Johan Commelin]

So that's probably more related to what you are doing

[Riccardo Brasca]

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.

[Johan Commelin]

I think you should just generalize it to semi_normed_group

[Johan Commelin]

And see what breaks after that (-;

[Riccardo Brasca]

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?

[Riccardo Brasca]

I guess the authors of almost everything in this part of the project are @Johan Commelin and @Adam Topaz

[Adam Topaz]

@Riccardo Brasca I can take a look in about an hour.

[Adam Topaz]

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

[Riccardo Brasca]

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.

[Johan Commelin]

But the instance is there only for locally constant functions into a normed group.

[Johan Commelin]

So locally_constant/analysis.lean should be generalised.

[Adam Topaz]

looks like locally_constant.pseudo_metric_space is missing

[Johan Commelin]

I pushed a fix

[Riccardo Brasca]

I just did it, locally_constant/analysis.lean is now for pseudo_metric_space.

[Riccardo Brasca]

But maybe we want to keep the results for metric_space

[Johan Commelin]

@Riccardo Brasca ooh, you might want to pull

[Johan Commelin]

failed to synthesize type class instance for
V : NormedGroup
⊢ semi_normed_group (completion ↥V)

[Johan Commelin]

This is hopefully in mathlib?

[Adam Topaz]

Is this true?

[Riccardo Brasca]

I thought about that, but complete means t1 in mathlib

[Riccardo Brasca]

And maybe even in standard mathematics, I am not sure

[Johan Commelin]

But that is not a problem right?

[Riccardo Brasca]

It means that is probably even a normed_group

[Johan Commelin]

Right, I think that the completion of a semi_normed_group is always a normed_group.

[Johan Commelin]

So we might need another mathlib PR that generalizes topology.metric_space.completion

[Riccardo Brasca]

Yes :expressionless:

[Riccardo Brasca]

I can do it very quickly

[Riccardo Brasca]

#7066

[Johan Commelin]

Wow! I expected a much larger diff.

[Patrick Massot]

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.

[Johan Commelin]

Hmmm, so now we are stuck for a couple of hours... or can we quickly duplicate this instance in some for_mathlib/temp.lean?

[Riccardo Brasca]

Dinner time for me, but fell free to modify my branch

[Johan Commelin]

I did this, but now we need to do a bit of maths.

[Johan Commelin]

Completion.lift uses is_closed_eq in its proof.

[Johan Commelin]

This no longer works. So I need to think about what is the correct move.

[Adam Topaz]

Is this pushed to the branch?

[Johan Commelin]

yes

[Johan Commelin]

Ooh, it's actually quite obvious. We should just assume that the target of the lift is a t2_space

[Johan Commelin]

Because clearly you can't lift V -> W to the completion of V for arbitrary W.

[Adam Topaz]

Doesn't complete imply t2?

[Johan Commelin]

Hmm, maybe it does, because t1 => t2 for groups?

[Johan Commelin]

But mathlib doesn't seem to realize this

[Adam Topaz]

hmmm....

[Riccardo Brasca]

docs#uniform_space.completion says "Hausdorff completion of α", so it should be t2... I think

[Johan Commelin]

Idem dito, it can't find [separated_space W]. So we are missing complete_space => separated_space

[Johan Commelin]

I've just added these redundant hyps with a comment. So we can remove them later.

[Johan Commelin]

Pushed.

[Riccardo Brasca]

Why docs#uniform_space.completion.separated_space doesn't work?

[Riccardo Brasca]

Hm, I see

[Adam Topaz]

Yeah, it's a bit silly.

[Riccardo Brasca]

Should we call NormedGroup SemiNormedGroup (and maybe recreate NormedGroup)? This will break a lot of files of course, but it is more clear

[Adam Topaz]

NB. https://github.com/leanprover-community/mathlib/blob/d7f6bd6188fc10f085bbcfcf513942467a071dc3/src/topology/uniform_space/completion.lean#L453

[Riccardo Brasca]

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.

[Adam Topaz]

That's fine for the completion functor, but not for lift

[Adam Topaz]

On the other hand, I don't know whether we actually need Completion.lift?

[Riccardo Brasca]

Ah sorry, you're right. But complete means separated, so that's OK anyway

[Adam Topaz]

Is this actually true for arbitrary uniform spaces?

[Riccardo Brasca]

docs#uniform_space.completion.separated_space seems to say this

[Johan Commelin]

I just pushed fix rescale.normed_group

[Riccardo Brasca]

If complete implies equal to the completion

[Johan Commelin]

It seems that there are 3 or 4 errors left

[Riccardo Brasca]

Oups, one error is my fault, I erased NormedGroup.coker.exists_norm_le

[Johan Commelin]

Another one is trickier.

lemma to_exact (hC : C.is_weak_bounded_exact k K m c₀) {δ : ℝ≥0} (hδ : 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

[Johan Commelin]

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₀ :=

[Johan Commelin]

These proofs currently make actual use of norm_eq_zero_iff and friends

[Johan Commelin]

@Riccardo Brasca But exists_norm_le maybe also needs a bit of refactoring, right?

[Riccardo Brasca]

The lemma says

lemma coker.exists_norm_le {f : A ⟶ B} (y₁ y₂ : B)
  (h : (coker.π y₁ : coker f) = coker.π y₂) (ε : ℝ) (hε : 0 < ε) :
  ∃ x, ∥y₁ - f x∥ ≤ ∥y₂∥ + ε :=

[Riccardo Brasca]

Now it is true even for ε = 0, isn't it?

[Riccardo Brasca]

The ε does not come from the quotient norm, it comes from the closure of the kernel

[Johan Commelin]

So the proof simplifies?

[Riccardo Brasca]

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

[Riccardo Brasca]

I have to stop now, sorry!

[Johan Commelin]

Ooh, of course :smiley: I forgot what the statement actually said.

[Johan Commelin]

That problem is now solved: git commit -am "fix src/system_of_complexes/truncate.lean"

[Johan Commelin]

So now there are two errors left, related to this strong_of_complete

[Johan Commelin]

Besides that, this mathlib bump is finished.

[Patrick Massot]

Do you still have questions about completeness and separation?

[Patrick Massot]

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.

[Patrick Massot]

The subcategory of complete but not necessarily separated uniform spaces has no good categorical properties.

[Johan Commelin]

@Patrick Massot So completion can do something nontrivial to a complete space?

[Patrick Massot]

No, it can make it smaller

[Johan Commelin]

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.

[Johan Commelin]

But turning this into an instance is of course tricky. Because it will start looping.

[Patrick Massot]

Yes, t1 implies t2 for topological groups.

[Patrick Massot]

Is there code to fix? On which branch?

[Johan Commelin]

@Patrick Massot semi_normed is the branch

[Johan Commelin]

I just checked: the final sorry in normed_spectral (9.6) just vanished completely :happy:

[Patrick Massot]

Is there anything to fix then?

[Johan Commelin]

Yes

[Johan Commelin]

strong_of_complete is broken

[Johan Commelin]

Because it assumes that the objects are normed_groups

[Johan Commelin]

And Lean doesn't know that semi_normed_group + complete_space implies normed_group.

[Johan Commelin]

We'll even have to think about how to state that implication without creating loops or diamonds.

[Patrick Massot]

This isn't true

[Patrick Massot]

I think you mean semi_normed_group + separated implies normed_group

[Johan Commelin]

But complete_space implies t1, right?

[Patrick Massot]

why?

[Johan Commelin]

I thought someone said that. I didn't check mathlib.

[Adam Topaz]

Is it not true that a complete pseudo_metric_space is T2?

[Adam Topaz]

I agree about general uniform spaces btw

[Patrick Massot]

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

[Riccardo Brasca]

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:

[Johan Commelin]

Right, defn 8.16(3) puts separated in the definition of complete.

[Johan Commelin]

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

[Johan Commelin]

But to make the proof work, we still need some glue to move from separated_space to norm_eq_zero_iff.

[Patrick Massot]

The name completion is maybe a bit unfortunate, but separated_completion seemed too long.

[Patrick Massot]

And of course Bourbaki calls it completion only.

[Patrick Massot]

Assuming semi_normed and separated is a bit silly, this is equivalent to normed_group, right?

[Johan Commelin]

Yes, but you are handed a system_of_complexes, whose objects are by definition semi_normed_group.

[Johan Commelin]

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.

[Patrick Massot]

I see

[Johan Commelin]

@Patrick Massot Do you want to give it a shot?

[Patrick Massot]

cauchy_seq_of_le_geometric is also used there, so it's not only about elements with norm zero.

[Johan Commelin]

Maybe we can write a def normed_group_of_separated and lift the semi_normed_group structure to a normed_group manually?

[Johan Commelin]

Then we just add a line to the top of the proof, and hopefully the rest of the proof just works.

[Patrick Massot]

That sounds like a cheap workaround, but actually this situation may be quite rare and not deserving a big refactor.

[Patrick Massot]

So maybe we should be lazy

[Patrick Massot]

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?

[Johan Commelin]

pseudo normed groups don't even have a has_norm at the moment. (And note that there can be elements with norm $\infty$).

[Johan Commelin]

Or did you mean semi_normed_group?

[Johan Commelin]

In the latter case, @Riccardo Brasca did you write such a constructor?

[Patrick Massot]

Yes, I meant semi normed group

[Riccardo Brasca]

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

[Riccardo Brasca]

And metric_space extends pseudo_metric_space

[Patrick Massot]

I need to do something else, but you should feel free to use:

lemma norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G] {g : G} :
  ∥g∥ ≤ 0 ↔ g = 0 :=
begin
  have : g = 0 ↔ g ∈ closure ({0} : set G),
  by simpa only [separated_space.out, mem_id_rel, sub_zero] using group_separation_rel g (0 : G),
  rw [this, normed_group.mem_closure_iff],
  simp [forall_lt_iff_le']
end

lemma norm_eq_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G] {g : G} :
  ∥g∥ = 0 ↔ g = 0 :=
begin
  conv_rhs { rw ← norm_le_zero_iff' },
  split ; intro h,
  { rw h },
  { exact le_antisymm h (norm_nonneg g) }
end

[Patrick Massot]

I'll come back to this tomorrow night if there is something to do

[Johan Commelin]

@Patrick Massot thanks! I'll add the to for_mathlib

[Johan Commelin]

Patrick Massot said:

cauchy_seq_of_le_geometric is also used there, so it's not only about elements with norm zero.

This seems to be the only problem now

[Johan Commelin]

I guess analysis/specific_limits can be (partly?) generalised to pseudo_metric_space.

[Johan Commelin]

cauchy_seq_of_le_geometric might just be true for pseudo_metric_spaces

[Johan Commelin]

I'm done for today. If someone wants to look at this last bit, please go ahead

[Riccardo Brasca]

This seems to work

lemma test {α : Type*} [pseudo_metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
  (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f :=
begin
  refine metric.cauchy_seq_iff'.2 (λε εpos, _),
  replace hd : cauchy_seq (λ (n : ℕ), ∑ x in range n, d x) :=
    let ⟨_, H⟩ := hd in H.tendsto_sum_nat.cauchy_seq,
  refine (metric.cauchy_seq_iff'.1 hd ε εpos).imp (λ N hN n hn, _),
  have hsum := hN n hn,
  rw [real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum,
  calc dist (f n) (f N) = dist (f N) (f n) : dist_comm _ _
  ... ≤ ∑ x in Ico N n, d x : dist_le_Ico_sum_of_dist_le hn (λ k _ _, hf k)
  ... ≤ abs (∑ x in Ico N n, d x) : le_abs_self _
  ... < ε : hsum
end

lemma test1 {α : Type*} [pseudo_metric_space α] {r C : ℝ} (hr : r < 1) {f : ℕ → α}
  (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) :
    has_sum (λ (n : ℕ), C * r ^ n) (C / (1 - r)) :=
begin
  rcases sign_cases_of_C_mul_pow_nonneg (λ n, dist_nonneg.trans (hu n)) with rfl | ⟨C₀, r₀⟩,
  { simp [has_sum_zero] },
  { refine has_sum.mul_left C _,
    simpa using has_sum_geometric_of_lt_1 r₀ hr }
end

lemma test2 {α : Type*} [pseudo_metric_space α] (r C : ℝ) (hr : r < 1) {f : ℕ → α}
  (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) : cauchy_seq f :=
test _ hu ⟨_, test1 hr hu⟩

The third lemma is cauchy_seq_of_le_geometric for pseudo_metric_space. If we only need this lemma I think we can just add it, to avoid to do a quite long refactor in mathlib.

[Riccardo Brasca]

I just copy/paste from mathlib the lemmas needed to prove it

[Riccardo Brasca]

I pushed to the semi_normed branch this modification. The lemmas are in for_mathlib/pseudo_metric.lean. It should now compile...

[Riccardo Brasca]

No errors! :smile:

[Johan Commelin]

Fantastic!

[Johan Commelin]

I merged this branch into master

[Johan Commelin]

We can do the little cleanups later, when things like #7066 are merged into mathlib

[Johan Commelin]

I'm now trying to see if the project compiles when we generalise polyhedral_lattice to semi_normed_group.

[Johan Commelin]

It looks like the proof of lem9.8 (combinatorial lemma) becomes a bit more complicated.

[Johan Commelin]

We'll need to pass to the separated_quotient of $\Lambda$.

[Johan Commelin]

Which might not be worth it. But if we keep normed_group in the defn of polyhedral_lattice, then we need to show that when we form the cosimplicial polyhedral lattice, all the quotients are by closed subgroups.

[Johan Commelin]

This is of course math-trivial, because normed_group_polyhedral_lattices are discrete.

[Johan Commelin]

But convincing Lean of that fact doesn't look like much fun.

[Johan Commelin]

An algebraic compromise might be to require that all the (nonzero?) generators of the polyhedral norm actually have nonzero norm.

[Johan Commelin]

This is math-equivalent to being a normed_group. But now we can just take the quotient as semi_normed_group.

[Riccardo Brasca]

I don't exactly what we need in the definition of polyhedral_lattice, but maybe the quotient by the closure will do it?

[Johan Commelin]

I think it will make proofs later on uglier.

[Johan Commelin]

Because you would like to know that taking the closure didn't do anything.

[Johan Commelin]

I finished this refactor, and pushed to master.

[Riccardo Brasca]

I am trying to generalize for_mathlib/normed_group_hom_completion.lean to semi_normed_group, but someow it doesn't find the instance you added to for_mathlib/normed_group.lean (the PR is on the queue).

lemma test {G : Type*} [semi_normed_group G] : normed_group (completion G) :=
begin
  exact completion.remove_me_soon G,
end

says

type mismatch at application
  completion.remove_me_soon G
term
  G
has type
  Type u_1 : Type (u_1+1)
but is expected to have type
  Type (max ? ?) : Type ((max ? ?)+1)

So it seems to be something related to universes... and so something I don't understand :hurt:

[Riccardo Brasca]

I just used

instance remove_me_soon (V : Type u) [semi_normed_group V] : normed_group (completion V)

(with Type u instead of Type*) and now it works.

[Filippo A. E. Nuccio]

The everlasting magic of the Universe...

[Riccardo Brasca]

src/for_mathlib/normed_group_hom_completion.lean is now generalized to semi_normed_group. The first part of the proof of normed_group_hom.ker_completion (where we deal with the stupid case C ≤ 0, that is now a little less stupid) has now a lot of duplicate code... I don't know, probably there is a better proof.. or maybe we can just assume 0 ≤ C.

[Riccardo Brasca]

This is in the semi_normed branch.

[Johan Commelin]

@Riccardo Brasca since you proved it already, I would just leave it like it is for now

[Johan Commelin]

But there shouldn't be any harm in assuming 0 \le C.

[Riccardo Brasca]

I upgrade mathlib (#7066 has been merged). There is some problem in toric/lem97.lean... maybe @Filippo A. E. Nuccio wants to have a quick look? It doesn't seem anything serious

[Filippo A. E. Nuccio]

I will have a look immediately

[Riccardo Brasca]

It's in the branch semi_normed

[Filippo A. E. Nuccio]

I can't find the branch. Is it part of the lean-liquid project?

[Riccardo Brasca]

Yes. You should probably do git remote update origin --prune to update the branch list

[Filippo A. E. Nuccio]

(I see that also in master the file toric'/lem97.lean does not compile at any rate...)

[Filippo A. E. Nuccio]

Found! :octopus:

[Riccardo Brasca]

You also have to do leanproject get-mathlib-cache... and maybe also leanproject get-cache (I am not completely sure about the difference).

[Filippo A. E. Nuccio]

(it actually worked without it)

[Filippo A. E. Nuccio]

Ok, solved and pushed to semi_normed.

[Filippo A. E. Nuccio]

(I have actually seen that the same issue shows up in master as well; when are you going to merge the two branches?)

[Riccardo Brasca]

I think that it shows up for you in master because your VS Code uses the cached olean files from semi_normed. But the "real" master compiles without errors

[Riccardo Brasca]

If you checkout master and get the correct olean it should work (but maybe I have misunderstood how this works)

[Filippo A. E. Nuccio]

it could be, although I got the issue in master before being able to checkout to semi_normed. So the problem should be elsewhere.

[Filippo A. E. Nuccio]

I am trying to get the "right" olean though, let's see.

[Filippo A. E. Nuccio]

Nope, it was still broken. I ended up making the same small modification in master and pushing there as well.

[Riccardo Brasca]

Ah, I just merged into master semi_normed!

[Riccardo Brasca]

Maybe it just realized that the two modification are the same and so everything works automagically.

[Filippo A. E. Nuccio]

I think so! After all, I copied-pasted, so if it did not realize they are equal, there is something autotragic going on...

[Riccardo Brasca]

In any case I erased the part that was in #7066, and now I have the impression that everything is for semi_normed_group.

I lost a little bit the big picture: @Johan Commelin is there something else to do related to semi_normed_group?

[Johan Commelin]

I think almost everything is now done

[Johan Commelin]

We might still find some small bits... but we can fix them on the go

[Johan Commelin]

Thanks again for the massive refactor!