# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: normed snake lemma

#### Johan Commelin (Jan 20 2021 at 12:43):

I pushed a statement of Proposition 9.10 (the normed snake lemma) to the file `normed_snake.lean`

.

(cc @Riccardo Brasca)

#### Riccardo Brasca (Jan 20 2021 at 12:53):

Great! This looks like something not too hard

#### Riccardo Brasca (Jan 20 2021 at 12:53):

You probably forgot a `lemma normed_snake`

at the of the file

#### Riccardo Brasca (Jan 20 2021 at 12:54):

I mean, you forgot to write the statement :)

#### Johan Commelin (Jan 20 2021 at 12:55):

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

#### Adam Topaz (Jan 20 2021 at 15:02):

In case anyone is working on this -- I just fixed the docstring (make sure to pull :smile: )

https://github.com/leanprover-community/lean-liquid/blob/9eca62d7c442709436ef5ce2f22a9b327c486914/src/normed_snake.lean#L28

#### Riccardo Brasca (Jan 20 2021 at 15:04):

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

#### Adam Topaz (Jan 20 2021 at 15:13):

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

#### Johan Commelin (Jan 20 2021 at 15:16):

I fixed a typo in the statement.

#### Riccardo Brasca (Jan 20 2021 at 16:26):

In the statement of `normed_snake`

I think that the fact that `N`

is the quotient `M'/M`

is missing: there is `hg : ∀ c i, function.surjective (g.apply c i)`

, but `g`

seems unrelated to `M`

. Am I missing something?

#### Adam Topaz (Jan 20 2021 at 16:37):

I think that's implied by the assumption `hg`

, right?

#### Adam Topaz (Jan 20 2021 at 16:38):

Oh, maybe the assumption that `M`

is the kernel of `g`

is missing?

#### Riccardo Brasca (Jan 20 2021 at 16:40):

Yes `hg`

says that `g`

is surjective, but not that `M`

is its kernel

#### Adam Topaz (Jan 20 2021 at 16:42):

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

#### Johan Commelin (Jan 20 2021 at 16:50):

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

#### Riccardo Brasca (Jan 20 2021 at 17:21):

Also the quotient norm I don't think satisfies the written property `hN : ∀ c i x, ∥g.apply c i x∥ = ∥x∥`

: usually the norm on the quotient is the `inf`

over all the representative of an element.

#### Riccardo Brasca (Jan 20 2021 at 17:22):

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

and assume that

#### Johan Commelin (Jan 20 2021 at 17:26):

Yep... I wrote a hasty statement

#### Johan Commelin (Jan 20 2021 at 17:27):

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

#### Johan Commelin (Jan 20 2021 at 17:28):

Riccardo Brasca said:

I have to think a little bit about it, but we probably need something like a proposition

`is_quotient g`

and assume that

I like this idea!

#### Riccardo Brasca (Jan 20 2021 at 17:32):

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

#### Adam Topaz (Jan 20 2021 at 17:49):

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

#### Johan Commelin (Jan 20 2021 at 17:50):

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

#### Adam Topaz (Jan 20 2021 at 17:51):

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

.

#### Riccardo Brasca (Jan 20 2021 at 17:51):

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

#### Adam Topaz (Jan 20 2021 at 17:52):

Riccardo Brasca said:

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

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

#### Adam Topaz (Jan 20 2021 at 17:52):

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

#### Riccardo Brasca (Jan 20 2021 at 17:53):

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

#### Johan Commelin (Jan 20 2021 at 17:53):

sure, that condition should be removed

#### Adam Topaz (Jan 20 2021 at 17:54):

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

#### Riccardo Brasca (Jan 20 2021 at 17:54):

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

#### Johan Commelin (Jan 20 2021 at 17:54):

Right, me stupid :oops: :rofl:

#### Riccardo Brasca (Jan 20 2021 at 17:54):

But I don't think this property characterize the projection

#### Johan Commelin (Jan 20 2021 at 17:55):

I think your `inf`

idea sounded good. But the best thing would be to define `is_quotient`

and prove that it has the univ. property.

#### Adam Topaz (Jan 20 2021 at 18:07):

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

```
(⊤ : add_subgroup V₁).map f.to_add_monoid_hom
```

Seems a bit silly...

#### Johan Commelin (Jan 20 2021 at 18:11):

There should be `add_monoid_hom.image`

but we might want to add a copy of that for `normed_group_hom`

.

#### Adam Topaz (Jan 20 2021 at 18:11):

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

#### Johan Commelin (Jan 20 2021 at 18:15):

Hmm, maybe we only have it for linear maps

#### Riccardo Brasca (Jan 20 2021 at 18:53):

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

#### Riccardo Brasca (Jan 20 2021 at 18:53):

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

#### Johan Commelin (Jan 20 2021 at 18:56):

normed groups aren't assumed to be complete

#### Riccardo Brasca (Jan 20 2021 at 18:58):

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 (Jan 20 2021 at 18:58):

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

#### Riccardo Brasca (Jan 20 2021 at 19:02):

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 (Jan 20 2021 at 19:04):

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

#### Johan Commelin (Jan 20 2021 at 19:04):

so we should change the definition in Lean

#### Johan Commelin (Jan 20 2021 at 19:05):

maybe we can call those `prenormed_groups`

or something like that. (So they aren't metric spaces, because you can have a nontrivial subgroup of elements with norm `0`

.)

#### Johan Commelin (Jan 20 2021 at 19:07):

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

#### Riccardo Brasca (Jan 20 2021 at 19:09):

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

#### Johan Commelin (Jan 20 2021 at 19:10):

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

#### Johan Commelin (Jan 20 2021 at 19:10):

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

#### Riccardo Brasca (Jan 20 2021 at 19:12):

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

#### Johan Commelin (Jan 20 2021 at 19:13):

So in Lean `normed_group`

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

#### Adam Topaz (Jan 20 2021 at 19:13):

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

#### Johan Commelin (Jan 20 2021 at 19:14):

because the subgroups might not be closed? makes sense

#### Johan Commelin (Jan 20 2021 at 19:14):

So my guess is that we should introduce `seminormed_group`

or something like that, which drops the separatedness.

#### Riccardo Brasca (Jan 20 2021 at 19:14):

If you require separateness then the quotient exist for closed subspace

#### Adam Topaz (Jan 20 2021 at 19:15):

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

#### Riccardo Brasca (Jan 20 2021 at 19:16):

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

#### Adam Topaz (Jan 20 2021 at 19:16):

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

#### Riccardo Brasca (Jan 20 2021 at 19:16):

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

#### Adam Topaz (Jan 20 2021 at 19:16):

oh that's what you wrote :)

#### Adam Topaz (Jan 20 2021 at 19:20):

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

#### Johan Commelin (Jan 20 2021 at 19:22):

there is a thorough api for separation and completion.

#### Riccardo Brasca (Jan 20 2021 at 19:24):

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

#### Johan Commelin (Jan 20 2021 at 19:26):

maybe we should just try formalizing it

#### Johan Commelin (Jan 20 2021 at 19:26):

the proof looks very Leanable

#### Johan Commelin (Jan 20 2021 at 19:26):

does someone want to livestream their attempt?

#### Riccardo Brasca (Jan 20 2021 at 19:26):

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

#### Heather Macbeth (Jan 20 2021 at 19:27):

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

#### Riccardo Brasca (Jan 20 2021 at 20:03):

I think this is a sensible statement

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

I've added

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

In `src/for_mathlib/normed_group_hom.lean`

(I didn't check, but all the basic properties, like for the kernel, should be immediate).

#### Johan Commelin (Jan 20 2021 at 20:04):

hmmm, the `hN`

still looks wrong, right?

#### Johan Commelin (Jan 20 2021 at 20:04):

should that `=`

be `\le`

?

#### Riccardo Brasca (Jan 20 2021 at 20:05):

Ops, I thought I did it

#### Johan Commelin (Jan 20 2021 at 20:05):

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

#### Adam Topaz (Jan 20 2021 at 20:07):

Johan Commelin said:

does someone want to livestream their attempt?

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

#### Peter Scholze (Jan 20 2021 at 20:17):

You are really making me a bit nervous about the things I've written. Exactly as it should be! :-)

In 9.10, the hypothesis imposed is ensuring that on separated completions, the map from $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 (Jan 20 2021 at 20:23):

@Peter Scholze so what would you suggest/prefer... that we work with the separated notion `normed_group`

, or that we generalize (like in your notes) to include the non-separated case?

#### Johan Commelin (Jan 20 2021 at 20:24):

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

#### Peter Scholze (Jan 20 2021 at 20:44):

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

#### Bhavik Mehta (Jan 20 2021 at 21:44):

Johan Commelin said:

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

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

#### Riccardo Brasca (Jan 21 2021 at 12:39):

In my previous version of the lemma I also forgot that `g`

must be surjective. Here is a new statement.

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

#### Riccardo Brasca (Jan 21 2021 at 14:05):

Mmm, we should really have a definition of the "quotient norm".

For me, it is the following: let $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 (Jan 21 2021 at 14:14):

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

#### Adam Topaz (Jan 21 2021 at 14:17):

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

#### Riccardo Brasca (Jan 21 2021 at 14:17):

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

#### Riccardo Brasca (Jan 21 2021 at 14:17):

@Adam Topaz Yes, that's what I mean

#### Adam Topaz (Jan 21 2021 at 14:19):

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

#### Adam Topaz (Jan 21 2021 at 14:19):

Just trying to orient myself (I just woke up)

#### Riccardo Brasca (Jan 21 2021 at 14:22):

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

#### Peter Scholze (Jan 21 2021 at 14:23):

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

#### Peter Scholze (Jan 21 2021 at 14:26):

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

#### Peter Scholze (Jan 21 2021 at 14:31):

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

#### Riccardo Brasca (Jan 21 2021 at 14:34):

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 (Jan 21 2021 at 14:52):

@Riccardo Brasca Are you formalizing the proof?

#### Riccardo Brasca (Jan 21 2021 at 14:55):

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

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

#### Adam Topaz (Jan 21 2021 at 15:00):

There was some talk of live streaming? ;)

#### Adam Topaz (Jan 21 2021 at 15:02):

Is there a good reason to introduce `k_new`

separately?

#### Riccardo Brasca (Jan 21 2021 at 15:02):

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

#### Adam Topaz (Jan 21 2021 at 15:03):

Perhaps you should push the corrected statement of the theorem?

#### Johan Commelin (Jan 21 2021 at 15:04):

Adam Topaz said:

Is there a good reason to introduce

`k_new`

separately?

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

.

#### Johan Commelin (Jan 21 2021 at 15:05):

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

#### Johan Commelin (Jan 21 2021 at 15:05):

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

#### Adam Topaz (Jan 21 2021 at 15:05):

Sure, I guess we need

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

#### Adam Topaz (Jan 21 2021 at 15:07):

This works:

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

#### Johan Commelin (Jan 21 2021 at 15:10):

But more generally, we could provide two instances: one for `k^n`

and one for `k + k'`

.

#### Adam Topaz (Jan 21 2021 at 15:14):

Okay, here's a quick sketch for that:

```
instance one_le_add {a b : ℝ≥0} [ha : fact (1 ≤ a)] [hb : fact (1 ≤ b)] : fact (1 ≤ a + b) := le_trans ha $ by simp
instance one_le_pow {n : ℕ} {a : ℝ≥0} [h : fact (1 ≤ a)] : fact (1 ≤ a^n) :=
begin
induction n with n hn,
{ simp [le_refl] },
{ change 1 ≤ a * a^n,
have : 1 * a^n ≤ a * a^n, by exact mul_le_mul_right' h (a ^ n),
rw [one_mul] at this,
refine le_trans hn this }
end
example {k : ℝ≥0} [h : fact (1 ≤ k)] : fact (1 ≤ k^3 + k) := by apply_instance
```

#### Johan Commelin (Jan 21 2021 at 15:15):

Is `one_le_pow`

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

#### Adam Topaz (Jan 21 2021 at 15:16):

will do.

#### Adam Topaz (Jan 21 2021 at 15:17):

Johan Commelin said:

Is

`one_le_pow`

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

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

#### Adam Topaz (Jan 21 2021 at 15:18):

Ah okay, I can use this: docs#one_le_pow_iff

#### Adam Topaz (Jan 21 2021 at 15:20):

Oh, but that has an annoying assumption that `n`

is nonzero... (which is used for the implication that we don't need.)

#### Riccardo Brasca (Jan 21 2021 at 15:21):

If you are also modifying the statement I don't if using `Inf`

as I did is the more convenient way of stating that property (I've never used `Inf`

)

#### Adam Topaz (Jan 21 2021 at 15:21):

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

#### Riccardo Brasca (Jan 21 2021 at 15:22):

I am working on a copy :)

#### Adam Topaz (Jan 21 2021 at 15:26):

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

.

#### Riccardo Brasca (Jan 21 2021 at 15:27):

I've added

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

In `src/for_mathlib/normed_group_hom.lean`

#### Riccardo Brasca (Jan 21 2021 at 15:27):

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

#### Adam Topaz (Jan 21 2021 at 15:27):

Sure.

#### Adam Topaz (Jan 21 2021 at 15:28):

Well, let me push my changes to `facts.lean`

. After that, I suggest changing the statement of the normed snake lemma to the following:

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

#### Adam Topaz (Jan 21 2021 at 15:29):

pushed.

#### Johan Commelin (Jan 21 2021 at 15:29):

@Riccardo Brasca can you push what you have? If you don't want to push to `master`

, feel free to create `snake`

:wink: :snake:

#### Riccardo Brasca (Jan 21 2021 at 15:33):

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

#### Riccardo Brasca (Jan 21 2021 at 15:37):

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

#### Johan Commelin (Jan 21 2021 at 15:41):

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

#### Riccardo Brasca (Jan 21 2021 at 15:41):

I am riccardobrasca on GitHub

#### Johan Commelin (Jan 21 2021 at 15:42):

invitation sent

#### Riccardo Brasca (Jan 21 2021 at 15:44):

Pushed to branch `snake`

#### Adam Topaz (Jan 21 2021 at 16:04):

@Riccardo Brasca FWIW, regarding using `Inf`

, my limited experience with it is that the api for `Inf`

is very pleasant to use.

#### Riccardo Brasca (Jan 21 2021 at 16:05):

Good to know!

#### Riccardo Brasca (Jan 21 2021 at 16:06):

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

#### Riccardo Brasca (Jan 21 2021 at 16:07):

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 (Jan 21 2021 at 16:15):

docs#le_of_forall_le_of_dense ?

#### Heather Macbeth (Jan 21 2021 at 16:17):

or even closer, docs#le_of_forall_pos_le_add

#### Riccardo Brasca (Jan 21 2021 at 16:18):

@Heather Macbeth perfect, thank's!

#### Riccardo Brasca (Jan 21 2021 at 16:18):

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

#### Adam Topaz (Jan 21 2021 at 16:43):

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

LONG

#### Adam Topaz (Jan 21 2021 at 16:44):

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

#### Adam Topaz (Jan 21 2021 at 16:44):

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

#### Adam Topaz (Jan 21 2021 at 16:53):

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

statement.

#### Riccardo Brasca (Jan 21 2021 at 16:54):

It seems good to me

#### Adam Topaz (Jan 21 2021 at 16:54):

Okay great :)

#### Adam Topaz (Jan 21 2021 at 16:54):

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

#### Riccardo Brasca (Jan 21 2021 at 17:13):

The proof of the suffices statement should be an immediate consequence of `le_of_forall_pos_le_add`

, but Lean is not happy about it:

```
unknown identifier 'le_of_forall_pos_le_add'
```

#### Riccardo Brasca (Jan 21 2021 at 17:14):

`le_of_forall_pos_le_add'`

is in `algebra.ordered_group`

in mathlib, but not in the file `algebra.ordered_group`

of the project

#### Riccardo Brasca (Jan 21 2021 at 17:21):

If I modify that file to include `le_of_forall_pos_le_add'`

then I get `excessive memory consumption detected at 'replace'`

everywhere :dizzy:

#### Adam Topaz (Jan 21 2021 at 17:23):

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

#### Adam Topaz (Jan 21 2021 at 17:24):

Trying to update mathlib now...

#### Riccardo Brasca (Jan 21 2021 at 17:24):

I see that you put mathlib in `_target/...`

that makes clear to me you did something I don't understand :sweat_smile:

#### Adam Topaz (Jan 21 2021 at 17:25):

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

#### Riccardo Brasca (Jan 21 2021 at 17:31):

How can I update mathlib?

#### Adam Topaz (Jan 21 2021 at 17:35):

I used `leanproject upgrade-mathlib`

#### Adam Topaz (Jan 21 2021 at 17:41):

@Riccardo Brasca This is a mess....

LONG

#### Adam Topaz (Jan 21 2021 at 17:42):

I pushed to the branch `AT-snake`

in case you want access to the code.

#### Riccardo Brasca (Jan 21 2021 at 17:53):

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

#### Riccardo Brasca (Jan 21 2021 at 17:53):

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

#### Adam Topaz (Jan 21 2021 at 17:55):

Ah right.

#### Adam Topaz (Jan 21 2021 at 17:57):

Let me fix that. one sec.

#### Adam Topaz (Jan 21 2021 at 18:06):

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

#### Adam Topaz (Jan 21 2021 at 18:07):

#### Riccardo Brasca (Jan 21 2021 at 18:09):

Given `ε`

, assuming `∥ N.res n - N.d y ∥ ≤ k_new * (∥ N.d n ∥+ ε1)`

for all `ε1`

, why doesn't apply it for `ε1= ε/ k_new`

?

#### Riccardo Brasca (Jan 21 2021 at 18:09):

I mean, there are of course problems with `0≤...`

but mathematically that's what I would do

#### Riccardo Brasca (Jan 21 2021 at 18:11):

OK, that's what you did, sorry

#### Riccardo Brasca (Jan 21 2021 at 18:38):

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

#### Riccardo Brasca (Jan 21 2021 at 18:49):

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

#### Adam Topaz (Jan 21 2021 at 18:58):

Yeah exactly. This is what I was worried about.

#### Adam Topaz (Jan 21 2021 at 19:01):

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

#### Riccardo Brasca (Jan 21 2021 at 19:03):

I was thinking to it, but I am really sure this doesn't work for making the $\inf$ 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 (Jan 21 2021 at 22:54):

Ah!

#### Peter Scholze (Jan 21 2021 at 22:54):

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

#### Peter Scholze (Jan 21 2021 at 22:55):

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

#### Peter Scholze (Jan 21 2021 at 22:59):

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

#### Peter Scholze (Jan 21 2021 at 23:50):

Probably this is just my mind making up a solution as I want to go to bed, but I think the following fix ought to work. Leave all the statements and definitions essentially unchanged, but replace all normed abelian groups with complete normed abelian groups. In particular, in 9.10, the quotient $N=M'/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 (Jan 21 2021 at 23:51):

I'll try to update the file tomorrow

#### Sebastien Gouezel (Jan 22 2021 at 08:02):

I haven't followed the discussion closely, but let me still mention this: even in the setting of real Banach spaces and closed subspaces, the quotient norm is not always realized. I.e., there exists a closed hyperplane of `c_0`

, say (the space of sequences tending to `0`

with its sup norm) and a closed hyperplane `H`

such that a point in `c_0 / H`

of norm `1`

has no preimage of norm `1`

in `c_0`

. Take `H`

the kernel of the linear form $(x_n) \mapsto \sum 2^{-n} x_n$, for instance.

#### Sebastien Gouezel (Jan 22 2021 at 08:04):

Equivalently, points in `c_0`

but not in `H`

don't have any distance-minimizing projection on `H`

(because the would-be projection would be in $\ell^\infty$, but not in `c_0`

).

#### Peter Scholze (Jan 22 2021 at 09:53):

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

#### Johan Commelin (Jan 22 2021 at 09:55):

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

#### Johan Commelin (Jan 22 2021 at 09:56):

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

#### Peter Scholze (Jan 22 2021 at 09:58):

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

#### Peter Scholze (Jan 22 2021 at 10:05):

(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 (Jan 22 2021 at 11:47):

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

#### Adam Topaz (Jan 22 2021 at 13:45):

So it sounds like we should introduce the category `CompleteNormedGroup`

?

#### Johan Commelin (Jan 22 2021 at 13:47):

Can't we just add `[complete_space M]`

etc...?

#### Riccardo Brasca (Jan 22 2021 at 13:48):

In `src/locally_constant/Vhat.lean`

there is already a lot of stuff

#### Johan Commelin (Jan 22 2021 at 13:48):

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

#### Riccardo Brasca (Jan 22 2021 at 13:50):

Maybe we should add `complete_system_of_complexes`

or something like that (we can also assume completeness for all objects)

#### Johan Commelin (Jan 22 2021 at 14:02):

Sure, we could extend `system_of_complexes`

to a new structure that includes `[\forall X, complete_space X]`

as a field.

#### Peter Scholze (Jan 23 2021 at 09:45):

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 (Jan 23 2021 at 13:12):

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 (Jan 23 2021 at 14:47):

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 (Jan 23 2021 at 14:52):

I mean something like defining defining `is_weak_bdd_exact_for_bdd_degree_above_idx`

using the $\varepsilon$, proving proposition 9.10 with this one (I am sure it works without troubles) and proving that for complete things `is_weak_bdd_exact_for_bdd_degree_above_idx`

implies `is_bdd_exact_for_bdd_degree_above_idx`

, with a slightly different bound.

#### Riccardo Brasca (Jan 23 2021 at 14:52):

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

#### Riccardo Brasca (Jan 23 2021 at 19:24):

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

.

#### Riccardo Brasca (Jan 23 2021 at 19:25):

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

#### Johan Commelin (Jan 23 2021 at 19:40):

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

#### Johan Commelin (Jan 23 2021 at 19:40):

at some point you suggested introducing `def is_quotient`

, and I think this is a good idea.

#### Riccardo Brasca (Jan 23 2021 at 19:43):

Some remark if you really want to read it:

I see that Peter has already updated the file on his website, I am following the following version

image.png

#### Riccardo Brasca (Jan 23 2021 at 19:44):

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

#### Riccardo Brasca (Jan 23 2021 at 19:45):

Yes, I think introducing `is_quotient`

will be useful in any case. I think we will the lemma `quotient`

, whose proof can for surely be golfed a lot.

#### Johan Commelin (Jan 23 2021 at 19:48):

so now `snake`

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

#### Riccardo Brasca (Jan 23 2021 at 19:53):

Ah, you're right, this is probably harmless. In any case if we really use `weak...`

at some point we need to prove that this implies the non weak version for complete groups

#### Riccardo Brasca (Jan 23 2021 at 19:54):

Also I have the impression that `Hf`

should hold with `(hi : i ≤ m + 2)`

since all our indexes are shifted, but maybe I am lost with all the notation

#### Johan Commelin (Jan 23 2021 at 19:55):

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

#### Johan Commelin (Jan 23 2021 at 19:56):

Riccardo Brasca said:

Also I have the impression that

`Hf`

should hold with`(hi : i ≤ m + 2)`

since all our indexes are shifted, but maybe I am lost with all the notation

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

#### Riccardo Brasca (Jan 23 2021 at 19:57):

Now I think it's OK :upside_down:

#### Riccardo Brasca (Jan 23 2021 at 20:19):

It's probably better to have `let c_new := k * (k * (k * c)),`

to apply `Hf`

without having to use `system_of_complexes.congr`

a lot

#### Riccardo Brasca (Jan 23 2021 at 21:08):

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

#### Kevin Buzzard (Jan 23 2021 at 22:01):

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

#### Riccardo Brasca (Jan 23 2021 at 22:15):

It's here https://github.com/leanprover-community/lean-liquid/blob/snake/src/normed_snake.lean

Note that I use some other definition in the branch `snake`

.

In any case the code is 1) not that slow, it is still usable 2) very messy and probably difficult to follow

#### Riccardo Brasca (Jan 23 2021 at 22:45):

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

#### Kevin Buzzard (Jan 23 2021 at 23:10):

I'm filling in some sorries

#### Riccardo Brasca (Jan 23 2021 at 23:13):

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

#### Kevin Buzzard (Jan 23 2021 at 23:13):

I'm just methodically killing them in dull ways

#### Kevin Buzzard (Jan 23 2021 at 23:17):

You can use `haveI`

instead of `letI`

for Props, and it's sometimes easier to use `set a := blah with ha`

than `let a := blah`

because then you can `rw ha`

to replace `a`

by `blah`

rather than just relying on the fact that they are defeq.

#### Kevin Buzzard (Jan 23 2021 at 23:21):

i killed a few but now I have to stop too

#### Alex J. Best (Jan 24 2021 at 03:53):

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

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

#### Riccardo Brasca (Jan 24 2021 at 10:07):

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

#### Damiano Testa (Jan 25 2021 at 09:48):

Dear All,

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

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

Thanks!

#### Johan Commelin (Jan 25 2021 at 09:53):

@Damiano Testa certainly!

#### Johan Commelin (Jan 25 2021 at 09:53):

the `snake`

branch is devoted to proving the "normed snake lemma"

#### Johan Commelin (Jan 25 2021 at 09:53):

but feel free to also look at the other sorrys

#### Johan Commelin (Jan 25 2021 at 09:53):

I'll send you an invite for the repo

#### Damiano Testa (Jan 25 2021 at 09:54):

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

#### Riccardo Brasca (Jan 25 2021 at 10:15):

Hi! I am working on the proof of the snake lemma right now (I don't know if we are going to keep this version at end, but this is going to be useful anyway I think). There are something like 15 variables and assumptions so it is probably not reasonable for someone else to read it (and moreover it is not that fun...). If you are looking for something easy to do, in the file `normed_snake.lean`

of the `sneak`

branch there are two lemmas, `commutes`

and `commutes_res`

that are easy and that should be moved somewhere else (and with better names...). `commutes_res`

moreover doesn't have a proof :grinning:

#### Johan Commelin (Jan 25 2021 at 10:18):

sounds like `d_apply`

and `res_apply`

(-; and the can probably go after the defn of `apply`

.

#### Riccardo Brasca (Jan 25 2021 at 10:30):

@Damiano Testa If you do it, can you please not touch `normed_snake.lean`

? Just to make my `git`

happy... I will erase them from there once they are somewhere else

#### Adam Topaz (Jan 25 2021 at 14:59):

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

#### Riccardo Brasca (Jan 25 2021 at 15:01):

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

#### Riccardo Brasca (Jan 25 2021 at 15:01):

(after merging what you have done)

#### Riccardo Brasca (Jan 25 2021 at 15:01):

semicomplete = the sorrys are unrelated to the snake lemma

#### Adam Topaz (Jan 25 2021 at 15:02):

Okay, pushed.

#### Adam Topaz (Jan 25 2021 at 15:03):

I'll try to fill in the `commutes_res`

lemma too whhile I'm at it.

#### Riccardo Brasca (Jan 25 2021 at 15:08):

I just pushed the proof

#### Adam Topaz (Jan 25 2021 at 15:09):

Oh :)

#### Riccardo Brasca (Jan 25 2021 at 15:11):

There are five `sorry`

in the file:

`commutes_res`

: easy (and should be somewhere else)

`N.admissible`

: the quotient of admissible stuff is admissible. Easy I think, it should be in the API of quotients

`hzerok`

, `hε₁`

and `kccnew`

are very easy inequalities about reals numbers

#### Riccardo Brasca (Jan 25 2021 at 15:12):

Of course the proof can probably be golfed *a lot*

#### Riccardo Brasca (Jan 25 2021 at 15:12):

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

#### Riccardo Brasca (Jan 25 2021 at 15:14):

And in any case I just called the lemma `weak_normed_snake`

, since it uses `is_weak_bdd_exact_for_bdd_degree_above_idx`

#### Riccardo Brasca (Jan 25 2021 at 15:16):

Riccardo Brasca said:

I just pushed the proof

@Adam Topaz I meant the almost complete proof of `weak_normed_snake`

. `commute_res`

is still a sorry.

#### Adam Topaz (Jan 25 2021 at 15:20):

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

#### Kevin Buzzard (Jan 25 2021 at 15:22):

@Johan Commelin this is really interesting. Riccardo started things off (obviously building on your work), and then people have just been dropping in and filling in `sorry`

s (me, Alex, Adam at least). What else is ready for this kind of game?

#### Johan Commelin (Jan 25 2021 at 15:23):

9.7

#### Johan Commelin (Jan 25 2021 at 15:23):

I'm working on the statement of 9.8

#### Johan Commelin (Jan 25 2021 at 15:23):

And people can start looking at the statement of 9.6

#### Johan Commelin (Jan 25 2021 at 15:24):

now that `snake`

is almost ready

#### Johan Commelin (Jan 25 2021 at 15:24):

we'll need double complexes for that

#### Johan Commelin (Jan 25 2021 at 15:24):

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

#### Riccardo Brasca (Jan 25 2021 at 15:32):

@Adam Topaz It is probably more convenient to replace `hzerok`

by `(0 : ℝ) < ↑k ^ 3 + 2 * ↑k + 1`

, so `hε₁`

should be immediate, and using `ne_of_lt hzerok`

(or whatever is needed) at the end

#### Adam Topaz (Jan 25 2021 at 15:35):

Okay, I killed the easy sorrys in the proof.

#### Adam Topaz (Jan 25 2021 at 15:37):

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

#### Adam Topaz (Jan 25 2021 at 15:37):

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

#### Adam Topaz (Jan 25 2021 at 15:42):

Kevin Buzzard said:

Johan Commelin this is really interesting. Riccardo started things off (obviously building on your work), and then people have just been dropping in and filling in

`sorry`

s (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 (Jan 25 2021 at 15:53):

I also have to stop :(

For the quotient, do you think that's better having an instance `[is_quotient]`

or a normal assumption?

#### Johan Commelin (Jan 25 2021 at 18:59):

@Riccardo Brasca do you think it would already be a good time to merge everything into `master`

? or would you rather finish all the `sorry`

s first?

#### Riccardo Brasca (Jan 25 2021 at 19:16):

I think we should at least move the lemmas about the composition of a morphism with `d`

and `res`

, with a reasonable name. They have nothing to do in that file

#### Johan Commelin (Jan 25 2021 at 19:16):

ok, sure

#### Riccardo Brasca (Jan 25 2021 at 19:17):

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

#### Johan Commelin (Jan 25 2021 at 19:19):

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

#### Riccardo Brasca (Jan 25 2021 at 19:29):

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

#### Riccardo Brasca (Jan 25 2021 at 19:30):

If you prefer I can modify `snake`

and let you do the merge into `master`

#### Johan Commelin (Jan 25 2021 at 19:31):

whatever you like best

#### Johan Commelin (Jan 25 2021 at 19:31):

In principle `git`

should allow us to fix anything we break

#### Alex J. Best (Jan 25 2021 at 19:38):

Johan Commelin said:

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

I had a go at this last night in fact, I've now pushed it to https://github.com/leanprover-community/lean-liquid/blob/master/src/system_of_double_complexes.lean there was one key lemma I couldn't prove due to not being familiar enough with mathlibs category/homological machinery, `d_comp_res`

for the vertical differential, due to the setup of double complexes as chain complexes of chain complexes there is a break in the symmetry which made one proof harder than the other for me. If someone wants to have a go at that, that would be great, I'm sure the proof is a 1-liner I just can't find the right way to fit the pieces together myself.

#### Johan Commelin (Jan 25 2021 at 19:43):

Thanks!

#### Riccardo Brasca (Jan 25 2021 at 19:53):

I tried to put

```
variables {M M' N : system_of_complexes.{u}} (f : M ⟶ M') (g : M' ⟶ N)
def category_theory.has_hom.hom.apply (f : M ⟶ N) (c : ℝ≥0) (i : ℤ) :=
(f.app (op c)).f i
variables (M M' N)
lemma d_apply (f : M ⟶ N) {c : ℝ≥0} {i : ℤ} (m : M.X c i) :
N.d (f.apply c i m) = f.apply c (i + 1) (M.d m) :=
begin
have h : ((M.obj (op c)).d i ≫ (f.app (op c)).f (i + 1)) m =
(f.app (op c)).f (i + 1) ((M.obj (op c)).d i m),
{ exact coe_comp ((M.obj (op c)).d i) ((f.app (op c)).f (i + 1)) m },
rwa [homological_complex.comm_at (f.app (op c)) i] at h,
end
lemma res_apply (f : M ⟶ N) (c c' : ℝ≥0) [h : fact (c ≤ c')] {i : ℤ} (m : M.X c' i) :
@system_of_complexes.res N c' c _ _ (f.apply c' i m) =
f.apply c i (@system_of_complexes.res M c' c _ _ m) :=
begin
sorry
end
```

inside `src/system_of_complexes.lean`

, but Lean is not happy with `N.d`

and `f.apply`

, and I don't understand why... :thinking:

#### Alex J. Best (Jan 25 2021 at 19:57):

Did you paste it into the system_of_complexes namespace or after?

#### Alex J. Best (Jan 25 2021 at 19:57):

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

#### Riccardo Brasca (Jan 25 2021 at 20:00):

Thank you, now it works

#### Riccardo Brasca (Jan 25 2021 at 20:17):

@Johan Commelin I just pushed to `snake`

a reorganization of some definition

#### Riccardo Brasca (Jan 25 2021 at 20:18):

Now `d_apply`

and `res_apply`

are in `src/system_of_complexes.lean`

, where there is also a `quotient`

section with the two results I used (we have to write the definition explicitely)

#### Riccardo Brasca (Jan 25 2021 at 20:20):

I also moved `normed_group_hom.is_strict`

and `is_strict.injective`

to `src/for_mathlib/normed_group_hom.lean`

, so in practice in `normed_snake.lean`

there is just the snake lemma

#### Johan Commelin (Jan 25 2021 at 20:22):

lgtm

#### Johan Commelin (Jan 25 2021 at 20:23):

let's merge it into `master`

#### Johan Commelin (Jan 25 2021 at 20:23):

any other fixes can be done afterwards

#### Johan Commelin (Jan 25 2021 at 20:23):

merged, pushed

#### Johan Commelin (Jan 25 2021 at 20:25):

@Riccardo Brasca thanks for all the great work!

#### Riccardo Brasca (Jan 25 2021 at 20:29):

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

#### Johan Commelin (Jan 25 2021 at 20:54):

Alex J. Best said:

there was one key lemma I couldn't prove due to not being familiar enough with mathlibs category/homological machinery,

`d_comp_res`

for the vertical differential, due to the setup of double complexes as chain complexes of chain complexes there is a break in the symmetry which made one proof harder than the other for me. If someone wants to have a go at that, that would be great, I'm sure the proof is a 1-liner I just can't find the right way to fit the pieces together myself.

done

#### Johan Commelin (Jan 25 2021 at 20:58):

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

- define
`is_quotient`

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

#### Johan Commelin (Jan 25 2021 at 20:58):

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

#### Riccardo Brasca (Jan 25 2021 at 20:59):

except that you probably mean complete instead of compact I agree

#### Riccardo Brasca (Jan 25 2021 at 21:00):

The first two points are not difficult I think (the first one is just to write a definition as a `def`

, and the second one seems immediate)

#### Riccardo Brasca (Jan 25 2021 at 21:02):

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

#### Johan Commelin (Jan 25 2021 at 21:09):

`res_apply`

is done

#### Riccardo Brasca (Jan 25 2021 at 21:52):

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

#### Johan Commelin (Jan 25 2021 at 21:55):

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

#### Riccardo Brasca (Jan 25 2021 at 21:57):

I mean, write down the definition by hand, without any complicated property as stated in the snake lemma (to be able to put `is_quotient g`

or similar) and prove that the quotient of an admissible thing is admissible

#### Riccardo Brasca (Jan 26 2021 at 12:32):

I have created a new branch `riccardobrasca`

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

#### Riccardo Brasca (Jan 26 2021 at 12:32):

Note that I had to upgrade mathlib to use `le_of_forall_pos_le_add`

#### Riccardo Brasca (Jan 26 2021 at 12:36):

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

#### Johan Commelin (Jan 26 2021 at 12:36):

@Riccardo Brasca how did you upgrade mathlib?

#### Johan Commelin (Jan 26 2021 at 12:36):

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

.

#### Johan Commelin (Jan 26 2021 at 12:37):

The recommended way is `leanproject up`

. This will change the `toml`

for you.

#### Riccardo Brasca (Jan 26 2021 at 12:37):

`leanproject upgrade-mathlib`

#### Johan Commelin (Jan 26 2021 at 12:37):

Does `git status`

show you uncommitted changes?

#### Riccardo Brasca (Jan 26 2021 at 12:38):

Yes, the `toml`

file... I ignored it since I didn't know what it is

#### Riccardo Brasca (Jan 26 2021 at 12:38):

I am pushing it

#### Johan Commelin (Jan 26 2021 at 12:38):

Riccardo Brasca said:

Yes, the

`toml`

file... I ignored it since I didn't know what it is

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

#### Johan Commelin (Jan 26 2021 at 12:40):

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

#### Johan Commelin (Jan 26 2021 at 12:41):

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

#### Johan Commelin (Jan 26 2021 at 12:46):

@Riccardo Brasca lgtm. You already put it in the `normed_group_hom`

namespace, right?

So we can use dot-notation and write `(hf : f.is_quotient)`

.

#### Johan Commelin (Jan 26 2021 at 12:46):

Feel free to merge

#### Riccardo Brasca (Jan 26 2021 at 12:48):

There are two `is_quotient`

, the first one is `normed_group_hom.is_quotient`

and the second one is `system_of_complexes.is_quotient`

, with the obvious relation between the two.

#### Kevin Buzzard (Jan 26 2021 at 12:49):

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

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

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

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

#### Kevin Buzzard (Jan 26 2021 at 12:50):

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

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

#### Riccardo Brasca (Jan 26 2021 at 12:50):

@Kevin Buzzard Thank's for the explanation!

#### Kevin Buzzard (Jan 26 2021 at 12:50):

When I was a PhD student we used to get 2400

#### Riccardo Brasca (Jan 26 2021 at 12:54):

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

is admissible (`M'.admissible`

suffices).

#### Johan Commelin (Jan 26 2021 at 12:57):

Great job!

#### Peter Scholze (Jan 26 2021 at 13:02):

Great!

#### Johan Commelin (Jan 26 2021 at 13:04):

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

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

#### Peter Scholze (Jan 26 2021 at 13:09):

Yes, that's right

#### Peter Scholze (Jan 26 2021 at 13:10):

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 (Jan 26 2021 at 13:10):

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

#### Johan Commelin (Jan 26 2021 at 13:10):

Ok, thanks for pointing that out

#### Peter Scholze (Jan 26 2021 at 13:11):

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

#### Johan Commelin (Jan 26 2021 at 13:11):

certainly

#### Peter Scholze (Jan 26 2021 at 13:12):

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

#### Johan Commelin (Jan 26 2021 at 13:13):

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

#### Patrick Massot (Jan 26 2021 at 13:15):

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

#### Johan Commelin (Jan 26 2021 at 13:16):

I think it's also about explicit bounds

#### Riccardo Brasca (Jan 26 2021 at 13:16):

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

#### Peter Scholze (Jan 26 2021 at 13:16):

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

#### Peter Scholze (Jan 26 2021 at 13:18):

@Patrick Massot Is Question 9.9 in www.math.uni-bonn.de/people/scholze/Analytic.pdf enough information? I'd like to understand how large the various things like $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 (Jan 26 2021 at 13:18):

Riccardo Brasca said:

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

This is probably a good sanity check in any case.

#### Peter Scholze (Jan 26 2021 at 13:19):

I agree

#### Patrick Massot (Jan 26 2021 at 13:26):

Question 9.9 is probably not enough but combining with what you just wrote is better (having an explicit list of inputs and outputs). So possible answers could look like: "In Theorem 9.5, one can promise k is no larger than $(r + r')\exp(\exp(m))$" 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 (Jan 26 2021 at 13:29):

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 (Jan 26 2021 at 13:37):

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

#### Riccardo Brasca (Jan 26 2021 at 13:55):

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

#### Peter Scholze (Jan 26 2021 at 13:57):

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 (Jan 26 2021 at 13:58):

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 (Jan 26 2021 at 14:01):

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

#### Peter Scholze (Jan 26 2021 at 14:02):

Sure, admissibility is always assumed

#### Peter Scholze (Jan 26 2021 at 15:11):

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

#### Peter Scholze (Jan 26 2021 at 15:19):

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 (Jan 26 2021 at 15:20):

No worries! You should blame Lean (-;

#### Peter Scholze (Jan 26 2021 at 15:21):

Of course this is exactly what I was hoping for!

#### Johan Commelin (Jan 26 2021 at 15:21):

But getting the statement of 9.4/9.5 for profinite `S`

would require reworking `Mbar`

a bit. That's fine. We would have to do that anyway if we aim for 9.1 as `second_target`

.

#### Peter Scholze (Jan 26 2021 at 15:29):

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

#### Riccardo Brasca (Jan 26 2021 at 15:38):

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

#### Peter Scholze (Jan 26 2021 at 15:41):

OK, here's an argument that weak exactness of a system of complexes of non-complete groups gives strong exactness of the completion, up to replacing $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 (Jan 26 2021 at 15:43):

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

#### Riccardo Brasca (Jan 26 2021 at 15:47):

I will try to formalize :)

#### Peter Scholze (Jan 26 2021 at 15:48):

That should settle it hopefully! :-)

#### Peter Scholze (Jan 26 2021 at 15:49):

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

#### Peter Scholze (Jan 26 2021 at 16:09):

Peter Scholze said:

OK, here's an argument that weak exactness of a system of complexes of non-complete groups gives strong exactness of the completion, up to replacing $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 (Jan 26 2021 at 16:41):

OK, I don't currently see how to do that argument. So for now it seems that one has to prove the strong version, and one has to do it directly for all profinite $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 (Jan 26 2021 at 17:16):

OK :)

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

#### Riccardo Brasca (Jan 26 2021 at 17:17):

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

#### Peter Scholze (Jan 26 2021 at 17:55):

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

#### Peter Scholze (Jan 26 2021 at 17:56):

Peter Scholze said:

OK, here's an argument that weak exactness of a system of complexes of non-complete groups gives strong exactness of the completion, up to replacing $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 (Jan 26 2021 at 18:22):

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

#### Johan Commelin (Jan 26 2021 at 18:25):

See `tsum`

, there is quite a lot about it

#### Kevin Buzzard (Jan 26 2021 at 18:28):

The "gotcha" with `tsum`

is that it needs absolute convergence (1-1/2+1/3-1/4+.. will have a `tsum`

of some junk value, rather than the limit of the finite sums from 1 to n, because it doesn't converge absolutely) but this shouldn't be an issue here.

#### Riccardo Brasca (Jan 26 2021 at 19:02):

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

#### Johan Commelin (Jan 26 2021 at 19:04):

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

#### Adam Topaz (Jan 26 2021 at 19:06):

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

#### Riccardo Brasca (Jan 26 2021 at 19:06):

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

#### Riccardo Brasca (Jan 26 2021 at 19:08):

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 (Jan 26 2021 at 19:08):

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

#### Heather Macbeth (Jan 26 2021 at 19:21):

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

#### Johan Commelin (Jan 26 2021 at 19:23):

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

#### Adam Topaz (Jan 26 2021 at 19:24):

#### Johan Commelin (Jan 26 2021 at 19:25):

But I guess `summable_iff_vanishing_norm`

gets us at least halfway to the statement we want.

#### Adam Topaz (Jan 26 2021 at 19:26):

#### Heather Macbeth (Jan 26 2021 at 19:28):

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

?

#### Johan Commelin (Jan 26 2021 at 19:30):

`res`

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

#### Johan Commelin (Jan 26 2021 at 19:31):

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

#### Heather Macbeth (Jan 26 2021 at 19:31):

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 (Jan 26 2021 at 19:31):

yep

#### Riccardo Brasca (Jan 26 2021 at 19:31):

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

#### Johan Commelin (Jan 26 2021 at 19:32):

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

#### Riccardo Brasca (Jan 26 2021 at 19:32):

Sorry, there is no $f$

#### Riccardo Brasca (Jan 26 2021 at 19:33):

The same is true for $d$

#### Heather Macbeth (Jan 26 2021 at 19:39):

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

#### Heather Macbeth (Jan 26 2021 at 19:39):

And docs#has_sum.norm_le_of_bounded would control its norm.

#### Sebastien Gouezel (Jan 26 2021 at 19:40):

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

#### Heather Macbeth (Jan 26 2021 at 19:40):

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

#### Riccardo Brasca (Jan 26 2021 at 19:53):

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

#### Patrick Massot (Jan 26 2021 at 20:04):

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 (Jan 26 2021 at 20:05):

I you need that argument I could formalize it.

#### Adam Topaz (Jan 26 2021 at 20:06):

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 (Jan 26 2021 at 20:06):

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

#### Patrick Massot (Jan 26 2021 at 20:08):

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

#### Adam Topaz (Jan 26 2021 at 20:08):

I see. I was envisioning formalizing the following statement:

```
import analysis.normed_space.basic
variables (A : Type*) [normed_group A] [complete_space A]
theorem foo {C : ℝ} (hC : 0 < C) (a : A) : ∃ x : ℕ → A,
has_sum x a ∧ ∀ i, ∥ x i ∥ ≤ C / 2^i := sorry
```

#### Adam Topaz (Jan 26 2021 at 20:09):

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

#### Patrick Massot (Jan 26 2021 at 20:09):

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

#### Peter Scholze (Jan 26 2021 at 20:09):

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

#### Peter Scholze (Jan 26 2021 at 20:10):

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

#### Peter Scholze (Jan 26 2021 at 20:10):

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 (Jan 26 2021 at 20:11):

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

#### Adam Topaz (Jan 26 2021 at 20:12):

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 (Jan 26 2021 at 20:12):

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

#### Peter Scholze (Jan 26 2021 at 20:12):

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

#### Peter Scholze (Jan 26 2021 at 20:16):

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

#### Adam Topaz (Jan 26 2021 at 20:18):

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

#### Peter Scholze (Jan 26 2021 at 20:20):

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

#### Riccardo Brasca (Jan 26 2021 at 20:21):

Adam Topaz said:

I see. I was envisioning formalizing the following statement:

`import analysis.normed_space.basic variables (A : Type*) [normed_group A] [complete_space A] theorem foo {C : ℝ} (hC : 0 < C) (a : A) : ∃ x : ℕ → A, has_sum x a ∧ ∀ i, ∥ x i ∥ ≤ C / 2^i := sorry`

It is enough to prove this for some positive `C`

if I am following the proof correctly, but the rest seems the correct statement

#### Adam Topaz (Jan 26 2021 at 20:22):

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

#### Riccardo Brasca (Jan 26 2021 at 20:22):

Ah, and `x i`

should be in the original group... so `A`

is not complete but `a`

is in the completion

#### Adam Topaz (Jan 26 2021 at 20:23):

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

#### Riccardo Brasca (Jan 26 2021 at 20:23):

I guess that in practice this will be OK since `x i`

will be constructed using a Cauchy sequence converging to `a`

#### Peter Scholze (Jan 26 2021 at 20:24):

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

#### Riccardo Brasca (Jan 26 2021 at 20:24):

For arbitrary `C`

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

#### Adam Topaz (Jan 26 2021 at 20:24):

:face_palm: yes of course

#### Patrick Massot (Jan 26 2021 at 20:25):

So this is what I wrote, right?

#### Peter Scholze (Jan 26 2021 at 20:25):

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

#### Patrick Massot (Jan 26 2021 at 20:27):

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

#### Peter Scholze (Jan 26 2021 at 20:28):

sure!

#### Adam Topaz (Jan 26 2021 at 20:29):

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 (Jan 26 2021 at 20:29):

Yes

#### Peter Scholze (Jan 26 2021 at 20:30):

I think you can take the norm of $x$

#### Riccardo Brasca (Jan 26 2021 at 20:30):

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

#### Riccardo Brasca (Jan 26 2021 at 20:30):

@Patrick Massot 's proof looks good to me

#### Patrick Massot (Jan 26 2021 at 20:32):

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

#### Peter Scholze (Jan 26 2021 at 20:36):

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 (Jan 26 2021 at 20:40):

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

#### Johan Commelin (Jan 26 2021 at 20:40):

can you filterize the statement?

#### Patrick Massot (Jan 26 2021 at 20:40):

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

#### Peter Scholze (Jan 26 2021 at 20:40):

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

#### Patrick Massot (Jan 26 2021 at 20:41):

Indeed Johan, that means filters.

#### Riccardo Brasca (Jan 26 2021 at 21:29):

@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 (Jan 26 2021 at 23:21):

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

#### Adam Topaz (Jan 26 2021 at 23:21):

#### Riccardo Brasca (Jan 27 2021 at 10:01):

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

#### Peter Scholze (Jan 27 2021 at 10:06):

Which change?

#### Peter Scholze (Jan 27 2021 at 10:07):

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

#### Peter Scholze (Jan 27 2021 at 10:07):

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

#### Riccardo Brasca (Jan 27 2021 at 10:07):

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

#### Peter Scholze (Jan 27 2021 at 10:09):

I think Johan Commelin is working on the pseudo-normed things; to be able to go cleanly from $\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 (Jan 27 2021 at 10:12):

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

#### Peter Scholze (Jan 27 2021 at 10:14):

This will not come up!

#### Peter Scholze (Jan 27 2021 at 10:14):

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

#### Riccardo Brasca (Jan 27 2021 at 10:15):

Even better!

#### Johan Commelin (Jan 27 2021 at 10:17):

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

#### Johan Commelin (Jan 27 2021 at 10:18):

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

#### Johan Commelin (Jan 27 2021 at 10:19):

@Riccardo Brasca If you search for `pseudo_normed_group`

in the repo, then you'll see that we already have it (-;

#### Johan Commelin (Jan 27 2021 at 10:20):

But we'll need to pack some special pseudo-normed groups into a category, and this has not been done yet. That category will serve as "input" for the construction that applies $\hat V$ and builds the system of complexes (of "ordinary" complete normed groups)

#### Riccardo Brasca (Jan 28 2021 at 12:41):

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

#### Peter Scholze (Jan 28 2021 at 12:46):

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

#### Adam Topaz (Jan 28 2021 at 13:49):

@Riccardo Brasca I started playing with it a couple of days ago. I can send you what I got so far in a few mins. Unfortunately, I won't have any time at all today for lean.

#### Riccardo Brasca (Jan 28 2021 at 13:53):

I would be happy to fill some sorry

#### Adam Topaz (Jan 28 2021 at 13:54):

@Riccardo Brasca :down:

long

#### Adam Topaz (Jan 28 2021 at 13:55):

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

#### Adam Topaz (Jan 28 2021 at 13:55):

I didn't get very far.

#### Adam Topaz (Jan 28 2021 at 13:58):

A few things to note:

- I was only focusing on the second paragraph of Peter's argument, so assuming everything is complete ahead of time.
- I'm not sure if the $\delta$ is needed. I put it there just to get started.
- I'm not sure if I chose the correct real numbers (like $k \cdot c$, etc.) in some places.
- 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 (Jan 28 2021 at 14:00):

Oh, and the `#check cauchy_seq_tendsto_of_complete`

at the top was just for myself to remember the name of this useful lemma :)

#### Riccardo Brasca (Jan 28 2021 at 14:02):

`d_res_commute`

is already there, it is called `d_res`

#### Adam Topaz (Jan 28 2021 at 14:03):

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

#### Riccardo Brasca (Jan 28 2021 at 14:03):

`library_search`

found it for me :)

#### Adam Topaz (Jan 28 2021 at 14:04):

I guess I was REALLY lazy then! :rofl:

#### Riccardo Brasca (Jan 28 2021 at 14:09):

Concerning the `i-1+1+1`

etc, in the proof the weak version I was able to completely avoid these problems : I never rewrote the indexes, so I had `C ... (i + 1 + 1 + 1)`

but this is virtually invisible since you can always write `_`

, Lean was very good at guessing and I let `i`

be the smallest one, to avoid subtraction. Also, it was useful to write `k^3*c`

as `k * (k * (k * c))`

, since the lemmas are written this way. Otherwise you end up using `congr`

a lot

#### Adam Topaz (Jan 28 2021 at 14:10):

This comes up from the argument since you first obtain some `y`

in `C.X _ i`

, but then you need to consider the sequence one index below, which puts you in `i-1`

, and then you apply `d`

which puts you back at `i-1+1`

.

#### Riccardo Brasca (Jan 28 2021 at 14:12):

Mmh, yeah, here it can be inevitable

#### Johan Commelin (Jan 28 2021 at 14:12):

There is `C.congr`

to help with these annoyances

#### Adam Topaz (Jan 28 2021 at 14:13):

Johan Commelin said:

There is

`C.congr`

to help with these annoyances

Good to know!

#### Riccardo Brasca (Jan 28 2021 at 14:13):

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

#### Riccardo Brasca (Jan 28 2021 at 15:49):

@Peter Scholze Zulip is not happy if I try to quote your message for some reason, so you have to find it, sorry...

Just to be sure to understand the math. You write "...$||\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 (Jan 28 2021 at 15:50):

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/normed.20snake.20lemma

I can at least put a link :)

#### Peter Scholze (Jan 28 2021 at 16:31):

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 (Jan 28 2021 at 17:03):

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

#### Riccardo Brasca (Jan 28 2021 at 19:09):

@Adam Topaz At the end I didn't had time to do anything except reading the argument. In any case I don't think $\delta$ is necessary.

#### Patrick Massot (Jan 28 2021 at 22:07):

Quick note: I haven't forget that I promised to formalize a lemma here, but I haven't found any time yet. I hope I'll do it tomorrow.

#### Riccardo Brasca (Jan 29 2021 at 13:07):

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 (Jan 29 2021 at 13:12):

thanks a lot for doing this!

#### Riccardo Brasca (Jan 29 2021 at 16:40):

I rewrote all Peter's argument in the stream, everything seems to be OK.

But now I forgot why we are doing this instead of following the current strategy in the pdf file (i.e. proving the preliminary observation and adapting the proof of the weak snake lemma to get a proof of the strong version): I thought this was to get better constants, but I have the impression are going in the opposite direction!

- The current (full proved) weak snake lemma says: quotient of weak $\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 (Jan 29 2021 at 17:09):

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

#### Peter Scholze (Jan 29 2021 at 20:37):

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

#### Peter Scholze (Jan 29 2021 at 20:39):

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 (Jan 29 2021 at 20:40):

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

#### Peter Scholze (Jan 29 2021 at 20:40):

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

#### Riccardo Brasca (Jan 29 2021 at 20:58):

What I propose is to forget this new notion of weak exactness that we introduced as a fix to the problems in the original proof of 9.10 and to keep your actual proof, unless you see other reasons to keep it. This amounts to prove your "preliminary observation" about the quotient norm and then doing the rest of the proof using this.

Proving the preliminary observation is for sure easier than proving the third and fourth points of my previous message (the argument are similar and definitely easy, there are no series, just sequences): I checked these with pen and paper, but almost nothing is done in Lean. Modifying the current proof of the weak snake lemma is not a lot work.

And this is not only laziness, I have the impression that the strategy using weak exactness gives worst bounds. Of course I know only a very little part of the paper, essentially just Proposition 9.10, so my opinion can very well be irrelevant :)

#### Patrick Massot (Jan 29 2021 at 21:06):

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

#### Peter Scholze (Jan 29 2021 at 21:07):

Well, I don't mind much either way, but here are the arguments for doing the weak version:

a) Until the very last step, you can assume that $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 (Jan 29 2021 at 21:13):

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

#### Riccardo Brasca (Jan 29 2021 at 21:29):

OK, I think I misunderstood the whole strategy: I thought you need in any case the strong snake lemma for completion (and the path weak snake lemma, then completions gives $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 (Jan 29 2021 at 21:30):

Exactly, everything is weak up until the very end

#### Peter Scholze (Jan 29 2021 at 21:30):

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

#### Riccardo Brasca (Jan 29 2021 at 21:46):

I will let someone that knows better than me the analysis part of mathlib decide how difficult it is to formalize the arguments of 4.15 and 4.16 of https://webusers.imj-prg.fr/~riccardo.brasca/files/blueprint.pdf

The file contains currently the best of the two approaches, and if we have proofs of 4.15 and 4.16 we can surely do the beginning of 4.18 very quickly (and I can take care of the rest). Note that the beginning of 4.15 (writing $x$ as a sum) has been done by Patrick, the rest is very elementary but with a lot of small calculations.

#### Patrick Massot (Jan 29 2021 at 21:50):

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

#### Riccardo Brasca (Jan 29 2021 at 22:02):

This is very possible! But I remember when I literally spent two hours to prove that $\{1, 3, 5, 7, 15, 21, 35 \}$ 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 (Jan 29 2021 at 22:03):

it has 7 tho

#### Riccardo Brasca (Jan 29 2021 at 22:04):

ROTF

#### Patrick Massot (Jan 29 2021 at 22:05):

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

#### Patrick Massot (Jan 29 2021 at 22:08):

It reminds me of a colloquium by Jean-Yves Welschinger about real enumerative geometry where he spent one hour explaining his job was to count geometric objects and then failed to draw five lines on the board (I don't remember whether he drew 4 or 6 lines).

#### Patrick Massot (Jan 29 2021 at 22:09):

Anyway, if you are sure those lemmas 4.15 and 4.16 are what you want and if you formalize the statements then I can probably handle the proofs at some point during the week.

#### Patrick Massot (Jan 29 2021 at 22:10):

But now I should go to bed.

#### Riccardo Brasca (Jan 29 2021 at 22:11):

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

#### Johan Commelin (Mar 13 2021 at 09:23):

The strictness assumption in 9.10 (normed snake) can be relaxed to norm-nonincreasing. I guess this is useful for our application in 9.6.

#### Johan Commelin (Mar 13 2021 at 14:04):

Hmm... we assume exactness at `M'`

in the statement of `weak_snake_lemma`

. But I think we should refactor this to say that kernel of `g`

is the topological closure of the range of `f`

.

#### Johan Commelin (Mar 15 2021 at 07:29):

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

#### Johan Commelin (Mar 15 2021 at 07:29):

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

#### Riccardo Brasca (Mar 15 2021 at 08:49):

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

#### Riccardo Brasca (Mar 15 2021 at 09:09):

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 (Mar 15 2021 at 09:12):

Nah, it's best to use the predicate, like we have now. Because in the application in 9.6 we don't get something that is definitionally the quotient. All the objects will be definitionally the quotient, but the system of complexes will probably not be.

#### Kevin Buzzard (Mar 15 2021 at 09:20):

@Riccardo Brasca we learnt this from the theory of localisation. If you define the field of fractions of an integral domain and then prove things about it, you can't deduce anything for the rational numbers because they're not literally equal to the field of fractions of the integers in the sense that they're not literally a built as a localisation.

#### Riccardo Brasca (Mar 15 2021 at 13:04):

@Johan Commelin The assumption in the normed snake lemma is already norm-nonincreasing, isn't it?

```
lemma weak_normed_snake {k k' k'' K K' K'' : ℝ≥0}
[hk : fact (1 ≤ k)] [hk' : fact (1 ≤ k')] [hk'' : fact (1 ≤ k'')]
{m : ℕ} {c₀ : ℝ≥0}
(hM : M.is_weak_bounded_exact k K (m+1) c₀)
(hM' : M'.is_weak_bounded_exact k' K' (m+1) c₀)
(hM'_adm : M'.admissible)
(hf : ∀ c i, (f.apply : M c i ⟶ M' c i).norm_noninc)
(Hf : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ m+1+1) (x : M (k'' * c) i),
∥(res x : M c i)∥ ≤ K'' * ∥f x∥)
(hg : ∀ c i, (g.apply : M' c i ⟶ N c i).ker = f.apply.range)
(hgquot : system_of_complexes.is_quotient g) :
N.is_weak_bounded_exact (k''*k*k') (K'*(K*K'' + 1)) m c₀ :=
```

#### Johan Commelin (Mar 15 2021 at 13:08):

Yes, I did that part

#### Johan Commelin (Mar 15 2021 at 13:08):

@Riccardo Brasca But we need another refactor, namely `hg`

should be weakened

#### Riccardo Brasca (Mar 15 2021 at 13:50):

OK, I had a look at it, and it is slightly longer than I thought: we need to prove Peter's "preliminary observation" (at the beginning of the proof of 9.10 in Analytic.pdf). This will modify some of the constants in the result (with something like `k^4`

if we use a single constant). If you're happy with this result I can work on it

#### Johan Commelin (Mar 15 2021 at 13:54):

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

#### Riccardo Brasca (Mar 15 2021 at 14:19):

Hmm, the preliminary observation seems to require completeness . If this is the versions of the snake lemma we need I don't see point of having the notion of weak exactness. (Note that proving the strong snake lemma modifying the proof of the weak one is not that much work.)

#### Riccardo Brasca (Mar 15 2021 at 14:20):

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

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

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

#### Peter Scholze (Mar 15 2021 at 14:21):

I didn't follow this discussion closely. It seemed to me that completeness shouldn't be needed, if one uses the weak notion of exactness

#### Peter Scholze (Mar 15 2021 at 14:22):

where do you now use completeness?

#### Peter Scholze (Mar 15 2021 at 14:22):

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

#### Johan Commelin (Mar 15 2021 at 14:23):

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

#### Peter Scholze (Mar 15 2021 at 14:24):

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

#### Peter Scholze (Mar 15 2021 at 14:24):

or do you mean assume completeness + strong exactness?

#### Johan Commelin (Mar 15 2021 at 14:24):

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 (Mar 15 2021 at 14:24):

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

is closed

#### Peter Scholze (Mar 15 2021 at 14:25):

wait, why should the image of f be closed?

#### Johan Commelin (Mar 15 2021 at 14:25):

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

#### Johan Commelin (Mar 15 2021 at 14:25):

right, we assume that it is, but in the proof of 9.6 we don't have that assumption. So there is a little hole there.

#### Peter Scholze (Mar 15 2021 at 14:25):

hmm wait

#### Peter Scholze (Mar 15 2021 at 14:26):

it's OK

#### Johan Commelin (Mar 15 2021 at 14:26):

Peter Scholze said:

or do you mean assume completeness + strong exactness?

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

#### Peter Scholze (Mar 15 2021 at 14:26):

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

#### Peter Scholze (Mar 15 2021 at 14:26):

Just take the quotient by the image

#### Johan Commelin (Mar 15 2021 at 14:26):

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

#### Peter Scholze (Mar 15 2021 at 14:26):

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

#### Peter Scholze (Mar 15 2021 at 14:26):

It is, I think

#### Johan Commelin (Mar 15 2021 at 14:27):

Ooh, in your generalised sense!

#### Johan Commelin (Mar 15 2021 at 14:27):

Wait, I'm confused...

#### Peter Scholze (Mar 15 2021 at 14:29):

What's the Lean definition of a normed group?

#### Johan Commelin (Mar 15 2021 at 14:29):

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

#### Peter Scholze (Mar 15 2021 at 14:29):

Yes

#### Johan Commelin (Mar 15 2021 at 14:29):

And lean assumes that axiom

#### Peter Scholze (Mar 15 2021 at 14:29):

Ah

#### Peter Scholze (Mar 15 2021 at 14:29):

But it doesn't assume completeness?

#### Johan Commelin (Mar 15 2021 at 14:29):

Nope

#### Johan Commelin (Mar 15 2021 at 14:29):

So separated, but not complete

#### Peter Scholze (Mar 15 2021 at 14:29):

Right

#### Peter Scholze (Mar 15 2021 at 14:30):

That's a weird convention then

#### Johan Commelin (Mar 15 2021 at 14:30):

```
/-- A normed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥` defines
a metric space structure. -/
class normed_group (α : Type*) extends has_norm α, add_comm_group α, metric_space α :=
(dist_eq : ∀ x y, dist x y = norm (x - y))
```

#### Johan Commelin (Mar 15 2021 at 14:30):

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

#### Peter Scholze (Mar 15 2021 at 14:31):

wait, a metric space also requires that?

#### Johan Commelin (Mar 15 2021 at 14:31):

Yes....

#### Peter Scholze (Mar 15 2021 at 14:31):

Weird... OK

#### Johan Commelin (Mar 15 2021 at 14:31):

```
/-- Metric space
Each metric space induces a canonical `uniform_space` and hence a canonical `topological_space`.
This is enforced in the type class definition, by extending the `uniform_space` structure. When
instantiating a `metric_space` structure, the uniformity fields are not necessary, they will be
filled in by default. In the same way, each metric space induces an emetric space structure.
It is included in the structure, but filled in by default.
-/
class metric_space (α : Type u) extends has_dist α : Type u :=
(dist_self : ∀ x : α, dist x x = 0)
(eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y)
(dist_comm : ∀ x y : α, dist x y = dist y x)
(dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
(edist : α → α → ℝ≥0∞ := λx y, ennreal.of_real (dist x y))
(edist_dist : ∀ x y : α, edist x y = ennreal.of_real (dist x y) . control_laws_tac)
(to_uniform_space : uniform_space α := uniform_space_of_dist dist dist_self dist_comm dist_triangle)
(uniformity_dist : 𝓤 α = ⨅ ε>0, 𝓟 {p:α×α | dist p.1 p.2 < ε} . control_laws_tac)
```

#### Peter Scholze (Mar 15 2021 at 14:31):

It seems that this is also the wikipedia definition

#### Johan Commelin (Mar 15 2021 at 14:31):

The second axiom

#### Peter Scholze (Mar 15 2021 at 14:32):

right

#### Johan Commelin (Mar 15 2021 at 14:32):

In Leiden they also taught me that axiom for metric spaces

#### Peter Scholze (Mar 15 2021 at 14:32):

It may very well be the standard

#### Johan Commelin (Mar 15 2021 at 14:33):

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

#### Riccardo Brasca (Mar 15 2021 at 14:33):

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

#### Peter Scholze (Mar 15 2021 at 14:33):

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

#### Johan Commelin (Mar 15 2021 at 14:34):

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

?

#### Riccardo Brasca (Mar 15 2021 at 14:34):

We can just call it `seminormed_group`

...

#### Johan Commelin (Mar 15 2021 at 14:34):

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

#### Riccardo Brasca (Mar 15 2021 at 14:35):

Just joking :sweat_smile:

#### Johan Commelin (Mar 15 2021 at 14:35):

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

#### Peter Scholze (Mar 15 2021 at 14:35):

Hmm, I guess so

#### Johan Commelin (Mar 15 2021 at 14:35):

And for the final application it doesn't matter either

#### Johan Commelin (Mar 15 2021 at 14:35):

So that might be the easy way out (-;

#### Peter Scholze (Mar 15 2021 at 14:36):

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

#### Peter Scholze (Mar 15 2021 at 14:37):

I think that would actually make the constants slightly worse there

#### Julian Külshammer (Mar 15 2021 at 14:40):

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

#### Sebastien Gouezel (Mar 15 2021 at 14:41):

I *really* don't think it is a good idea to change the metric space definition in mathlib, which is the standard one. Whenever you do analysis, having unique limits is extremely useful! (That's why in all analysis books the `L^p`

space is a space of equivalence classes of functions, for instance).

#### Johan Commelin (Mar 15 2021 at 14:42):

@Sebastien Gouezel But if we call them `pseudometric_space`

?

#### Johan Commelin (Mar 15 2021 at 14:42):

85% of the lemmas will still be about `metric_space`

, but some of the general facts can be proven for `pseudometric_space`

#### Sebastien Gouezel (Mar 15 2021 at 14:43):

Sure, why not. It's a little bit like non-separated topological groups: they show up sometimes, but whenever you want to do something serious, like extending a uniformly continuous function, you have to go to the separated quotient first.

#### Peter Scholze (Mar 15 2021 at 14:43):

OK, I think that should be the solution: Just also introduce `pseudometric_space`

and `seminormed_group`

and use these things instead

#### Johan Commelin (Mar 15 2021 at 14:43):

And similarly, we could then have `seminormed_group`

. (It seems that `pseudo_normed_group`

has recently be claimed...)

#### Johan Commelin (Mar 15 2021 at 14:45):

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

#### Johan Commelin (Mar 15 2021 at 14:47):

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

#### Peter Scholze (Mar 15 2021 at 14:49):

@Sebastien Gouezel OK, I definitely don't want to change the definition of `metric_space`

. It's just that from my experience in algebraic geometry, I always tend to explicitly think of separatedness as something that should not be included in the most primitive definition, only added later on top. This is probably an irrelevant consideration when doing analysis, but maybe a little relevant when setting up something like mathlib, so I think it would be good to include `pseudometric_space`

now.

#### Riccardo Brasca (Mar 15 2021 at 14:53):

But in any case for the snake lemma we cannot assume that `f`

has closed image, right? And for that I have the impression that completeness is needed... or not?

#### Sebastien Gouezel (Mar 15 2021 at 14:53):

It certainly can't hurt. And indeed I've already been longing for this class to be in mathlib several times (for instance to put a uniform structure on the space of integrable functions).

#### Johan Commelin (Mar 15 2021 at 14:53):

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

#### Peter Scholze (Mar 15 2021 at 14:53):

We can't assume that `f`

has closed image. But we shouldn't need it...

#### Johan Commelin (Mar 15 2021 at 14:54):

Because we can then drop `is_closed`

from the `instance`

of `seminormed_group`

for quotients

#### Damiano Testa (Mar 15 2021 at 14:56):

I like the distinction `metric`

vs `pseudo-metric`

. For a specific example, the Kobayashi pseudo-metric is usually referred to as a *pseudo*-metric, even though the title (but not the body) of the Wikipedia page says otherwise:

https://en.wikipedia.org/wiki/Kobayashi_metric

#### Riccardo Brasca (Mar 15 2021 at 14:57):

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

#### Riccardo Brasca (Mar 15 2021 at 14:58):

What is the general strategy? Introduce `pseudometric_space`

and check by hand what stay true in this generality?

#### Johan Commelin (Mar 15 2021 at 15:01):

One complication is whether we also want `pseudo_emetric_space`

...

#### Johan Commelin (Mar 15 2021 at 15:01):

(allowing $\infty$ as distance)

#### Johan Commelin (Mar 15 2021 at 15:02):

@Riccardo Brasca yes, that's the strategy that I would use. It might mean reorganizing a bunch of things into different sections, and maybe even split into different files

#### Peter Scholze (Mar 15 2021 at 15:04):

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

#### Johan Commelin (Mar 15 2021 at 15:05):

It's not relevant for this project, I agree. But if we dive into a refactor, we might want to do both in one go...

#### Julian Külshammer (Mar 15 2021 at 15:10):

A pseudo_emetric shows for example up in topological data analysis.

#### Peter Scholze (Mar 15 2021 at 15:11):

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

#### Riccardo Brasca (Mar 15 2021 at 15:21):

Apperently in mathlib these things are called docs#premetric_space

#### Johan Commelin (Mar 15 2021 at 15:22):

Ooh! So we have them already in some sense?

#### Johan Commelin (Mar 15 2021 at 15:22):

That means we only need to do the `seminormed_group`

stuff?

#### Riccardo Brasca (Mar 15 2021 at 15:23):

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

#### Johan Commelin (Mar 15 2021 at 15:24):

Should we call them `prenormed_group`

as well?

#### Johan Commelin (Mar 15 2021 at 15:24):

Because `seminormed_group`

sounds like it might have something to do with seminorms

#### Johan Commelin (Mar 15 2021 at 15:24):

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

#### Peter Scholze (Mar 15 2021 at 15:27):

Isn't this exactly a seminorm?

#### Riccardo Brasca (Mar 15 2021 at 15:27):

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

#### Peter Scholze (Mar 15 2021 at 15:28):

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

#### Johan Commelin (Mar 15 2021 at 15:28):

ooh, you are right. so `seminormed_group`

it is! :face_palm:

#### Sebastien Gouezel (Mar 15 2021 at 15:28):

Note that nothing is proved currently on `premetric_space`

, I only introduced it some time ago as a gadget to construct metric spaces by taking a suitable quotient. For instance, there is currently no uniform space structure on a premetric space.

#### Johan Commelin (Mar 15 2021 at 15:29):

We can rename `premetric_space`

#### Sebastien Gouezel (Mar 15 2021 at 15:30):

It will be a little bit strange to have `pseudometric_space`

and `seminormed_space`

, but hey, we all know that mathematics terminology is not always coherent :-)

#### Peter Scholze (Mar 15 2021 at 15:31):

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

#### Riccardo Brasca (Mar 15 2021 at 16:29):

I gave a little try to understand what is needed for the refactor about `pseudometric_space`

(or whatever name we choose), and I think I can do it. If I understand correctly how mathlib is set up, `emetric_space`

is more fundamental than `metric_space`

(this is clear looking at the imports), so I will start there

#### Johan Commelin (Mar 15 2021 at 16:30):

Are there `pre_emetric_space`

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

#### Riccardo Brasca (Mar 15 2021 at 16:34):

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

#### Riccardo Brasca (Mar 15 2021 at 20:31):

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

#### Johan Commelin (Mar 15 2021 at 20:40):

Thanks, I left 1 comment (-;

#### Johan Commelin (Apr 06 2021 at 13:32):

Hooray! `normed_group_hom`

in mathlib is now refactored to work for semi normed groups.

Major thanks to Riccardo for the 5 or 6 PRs that performed the refactor!

#### Riccardo Brasca (Apr 06 2021 at 13:34):

I have some time today to work on `semi_normed_group`

in the LTE! `leanproject upgrade-mathlib`

is all I have to do to ugrade mathlib? I am working in my branch

#### Johan Commelin (Apr 06 2021 at 13:37):

Yes, `leanproject up`

should get you started. But there might be unexpected breakage.

#### Johan Commelin (Apr 06 2021 at 13:37):

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

#### Johan Commelin (Apr 06 2021 at 13:38):

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

#### Johan Commelin (Apr 06 2021 at 13:39):

The oleans aren't available yet.

#### Riccardo Brasca (Apr 06 2021 at 13:39):

No problem :)

#### Johan Commelin (Apr 06 2021 at 13:55):

Now they are there, it seems

#### Riccardo Brasca (Apr 06 2021 at 13:58):

`leanproject up`

did its job. If I try to build the project I get a lot of errors, but I can work normally on `normed_group_quotient.lean`

#### Johan Commelin (Apr 06 2021 at 13:59):

I'll look at the other errors

#### Johan Commelin (Apr 06 2021 at 13:59):

Is your branch clean?

#### Johan Commelin (Apr 06 2021 at 14:00):

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

#### Riccardo Brasca (Apr 06 2021 at 14:01):

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

.

#### Riccardo Brasca (Apr 06 2021 at 14:02):

The first error is

```
/imjprgpool/home/brasca/lean/lean-liquid/_target/deps/mathlib/src/category_theory/abelian/additive_functor.lean:1:0: error: file '/imjprgpool/home/brasca/lean/lean-liquid/_target/deps/mathlib/src/category_theory/abelian/additive_functor.lean' not found in the search path
```

So it's probably my fault

#### Johan Commelin (Apr 06 2021 at 14:02):

No, I got the same.

#### Johan Commelin (Apr 06 2021 at 14:02):

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

#### Johan Commelin (Apr 06 2021 at 14:06):

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

#### Johan Commelin (Apr 06 2021 at 14:06):

But now the errors are about `NormedGroup`

and such

#### Johan Commelin (Apr 06 2021 at 14:06):

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

#### Riccardo Brasca (Apr 06 2021 at 14:26):

Yes, that looks like a real error caused by something about `normed_group_hom`

, that now accepts `semi_normed_group`

. I am playing with it to see if I can fix it without too much work... I am not very familiar to declaration like `def NormedGroup : Type (u+1) := bundled normed_group`

.

#### Johan Commelin (Apr 06 2021 at 14:27):

I think you should just generalize it to `semi_normed_group`

#### Johan Commelin (Apr 06 2021 at 14:27):

And see what breaks after that (-;

#### Riccardo Brasca (Apr 06 2021 at 16:51):

I started in the branch `semi_normed`

the refactor to include `semi_normed_group`

in the LTE. What I did is to generalize the files

`src/for_mathlib/normed_group`

`src/for_mathlib/normed_group_hom_equalizer`

, `src/for_mathlib/normed_group_hom`

and `src/for_mathlib/normed_group_quotient`

: no problem here.

Then I started working on `src/normed_group/NormedGroup`

: I essentially wrote `semi`

everywhere (but I didn't change the name of the category, even if this should be done) and erased the lemma `coker.exists_norm_le`

that is useless since now we take the algebraic quotient (without taking the closure).

Now Lean complains about other places where `NormedGroup`

is used, for example in `src/locally_constant/NormedGroup`

. I am not very familiar with the category theory part of mathlib, so it probably makes more sense if someone else look at this, at least to have a plan of what we have to do. For example, do we want locally constant functions with values in a `pseudo_metric_space`

? Do we need both the category `SemiNormedGroup`

and the category `NormedGroup`

?

#### Riccardo Brasca (Apr 06 2021 at 16:52):

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

#### Adam Topaz (Apr 06 2021 at 16:54):

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

#### Adam Topaz (Apr 06 2021 at 16:59):

Well, just looking very quickly, it seems that there is no seminormed_group instance on locally constant functors, and that's the source of the issue in `src/locally_constant/NormedGroup.lean`

#### Riccardo Brasca (Apr 06 2021 at 17:03):

Yes, the problem is for sure that one. What confuses me is that there is a `normed_group`

instance, and so also a `semi_normed_group`

instance. In any case the question is if we should generalize everything to `semi_normed_group`

or rather convince Lean that here everything is automatically a `semi_normed_group`

.

#### Johan Commelin (Apr 06 2021 at 17:04):

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

#### Johan Commelin (Apr 06 2021 at 17:04):

So `locally_constant/analysis.lean`

should be generalised.

#### Adam Topaz (Apr 06 2021 at 17:08):

looks like `locally_constant.pseudo_metric_space`

is missing

#### Johan Commelin (Apr 06 2021 at 17:10):

I pushed a fix

#### Riccardo Brasca (Apr 06 2021 at 17:10):

I just did it, `locally_constant/analysis.lean`

is now for `pseudo_metric_space`

.

#### Riccardo Brasca (Apr 06 2021 at 17:10):

But maybe we want to keep the results for `metric_space`

#### Johan Commelin (Apr 06 2021 at 17:11):

@Riccardo Brasca ooh, you might want to pull

#### Johan Commelin (Apr 06 2021 at 17:12):

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

#### Johan Commelin (Apr 06 2021 at 17:12):

This is hopefully in mathlib?

#### Adam Topaz (Apr 06 2021 at 17:14):

Is this true?

#### Riccardo Brasca (Apr 06 2021 at 17:14):

I thought about that, but `complete`

means `t1`

in mathlib

#### Riccardo Brasca (Apr 06 2021 at 17:14):

And maybe even in standard mathematics, I am not sure

#### Johan Commelin (Apr 06 2021 at 17:14):

But that is not a problem right?

#### Riccardo Brasca (Apr 06 2021 at 17:16):

It means that is probably even a `normed_group`

#### Johan Commelin (Apr 06 2021 at 17:17):

Right, I think that the completion of a `semi_normed_group`

is always a `normed_group`

.

#### Johan Commelin (Apr 06 2021 at 17:18):

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

#### Riccardo Brasca (Apr 06 2021 at 17:18):

Yes :expressionless:

#### Riccardo Brasca (Apr 06 2021 at 17:18):

I can do it very quickly

#### Riccardo Brasca (Apr 06 2021 at 17:24):

#### Johan Commelin (Apr 06 2021 at 17:26):

Wow! I expected a much larger diff.

#### Patrick Massot (Apr 06 2021 at 17:28):

Don't forget the backbone of all this is the general uniform space completion that doesn't see any difference between pseudo-norms and norms, it way more general.

#### Johan Commelin (Apr 06 2021 at 17:31):

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

?

#### Riccardo Brasca (Apr 06 2021 at 17:34):

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

#### Johan Commelin (Apr 06 2021 at 17:56):

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

#### Johan Commelin (Apr 06 2021 at 17:57):

`Completion.lift`

uses `is_closed_eq`

in its proof.

#### Johan Commelin (Apr 06 2021 at 17:57):

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

#### Adam Topaz (Apr 06 2021 at 17:58):

Is this pushed to the branch?

#### Johan Commelin (Apr 06 2021 at 17:58):

yes

#### Johan Commelin (Apr 06 2021 at 17:58):

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

#### Johan Commelin (Apr 06 2021 at 17:58):

Because clearly you can't lift `V -> W`

to the completion of `V`

for arbitrary `W`

.

#### Adam Topaz (Apr 06 2021 at 17:59):

Doesn't complete imply t2?

#### Johan Commelin (Apr 06 2021 at 18:00):

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

#### Johan Commelin (Apr 06 2021 at 18:00):

But mathlib doesn't seem to realize this

#### Adam Topaz (Apr 06 2021 at 18:00):

hmmm....

#### Riccardo Brasca (Apr 06 2021 at 18:02):

docs#uniform_space.completion says "Hausdorff completion of `α`

", so it should be `t2`

... I think

#### Johan Commelin (Apr 06 2021 at 18:02):

Idem dito, it can't find `[separated_space W]`

. So we are missing `complete_space => separated_space`

#### Johan Commelin (Apr 06 2021 at 18:04):

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

#### Johan Commelin (Apr 06 2021 at 18:04):

Pushed.

#### Riccardo Brasca (Apr 06 2021 at 18:05):

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

#### Riccardo Brasca (Apr 06 2021 at 18:06):

Hm, I see

#### Adam Topaz (Apr 06 2021 at 18:07):

Yeah, it's a bit silly.

#### Riccardo Brasca (Apr 06 2021 at 18:09):

Should we call `NormedGroup`

`SemiNormedGroup`

(and maybe recreate `NormedGroup`

)? This will break a lot of files of course, but it is more clear

#### Adam Topaz (Apr 06 2021 at 18:11):

#### Riccardo Brasca (Apr 06 2021 at 18:16):

The correct thing to do is the following I think: if `M`

and `N`

are `semi_normed_group`

(or `pseudo_metric_space`

, or whatever), and `f : M → N`

then the induced map `completion M → completion N`

is given by considering the natural map `i : N → completion N`

, so now `i ∘ f : M → completion N`

can be extendend.

#### Adam Topaz (Apr 06 2021 at 18:20):

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

#### Adam Topaz (Apr 06 2021 at 18:21):

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

?

#### Riccardo Brasca (Apr 06 2021 at 18:24):

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

#### Adam Topaz (Apr 06 2021 at 18:29):

Is this actually true for arbitrary uniform spaces?

#### Riccardo Brasca (Apr 06 2021 at 18:31):

docs#uniform_space.completion.separated_space seems to say this

#### Johan Commelin (Apr 06 2021 at 18:31):

I just pushed `fix rescale.normed_group`

#### Riccardo Brasca (Apr 06 2021 at 18:31):

If complete implies equal to the completion

#### Johan Commelin (Apr 06 2021 at 18:37):

It seems that there are 3 or 4 errors left

#### Riccardo Brasca (Apr 06 2021 at 18:39):

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

#### Johan Commelin (Apr 06 2021 at 18:42):

Another one is trickier.

```
lemma to_exact (hC : C.is_weak_bounded_exact k K m c₀) {δ : ℝ≥0} (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 (Apr 06 2021 at 18:44):

Which is used in

```
lemma strong_of_complete [hk : fact (1 ≤ k)] [hk' : fact (1 ≤ k')]
(hC : C.is_weak_bounded_exact k K m c₀)
(hC' : admissible C) [∀ c i, complete_space (C c i)] :
∀ δ > 0, C.is_bounded_exact (k^2) (K + δ) m c₀ :=
```

#### Johan Commelin (Apr 06 2021 at 18:45):

These proofs currently make actual use of `norm_eq_zero_iff`

and friends

#### Johan Commelin (Apr 06 2021 at 18:46):

@Riccardo Brasca But `exists_norm_le`

maybe also needs a bit of refactoring, right?

#### Riccardo Brasca (Apr 06 2021 at 18:47):

The lemma says

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

#### Riccardo Brasca (Apr 06 2021 at 18:47):

Now it is true even for `ε = 0`

, isn't it?

#### Riccardo Brasca (Apr 06 2021 at 18:48):

The `ε `

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

#### Johan Commelin (Apr 06 2021 at 18:48):

So the proof simplifies?

#### Riccardo Brasca (Apr 06 2021 at 18:50):

I mean that the statement is completely trivial, if `y₁`

and `y₂`

are equal in the cokernel the difference is in the image of `f`

, since we are taking the algebraic quotient

#### Riccardo Brasca (Apr 06 2021 at 18:53):

I have to stop now, sorry!

#### Johan Commelin (Apr 06 2021 at 18:58):

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

#### Johan Commelin (Apr 06 2021 at 19:10):

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

#### Johan Commelin (Apr 06 2021 at 19:11):

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

#### Johan Commelin (Apr 06 2021 at 19:11):

Besides that, this mathlib bump is finished.

#### Patrick Massot (Apr 06 2021 at 19:24):

Do you still have questions about completeness and separation?

#### Patrick Massot (Apr 06 2021 at 19:25):

Johan Commelin said:

Idem dito, it can't find

`[separated_space W]`

. So we are missing`complete_space => separated_space`

This implication is not correct (at least not with our definition of complete, which is also Bourbaki's definition of complete). However `completion X`

is always separated, even if `X`

isn't.

#### Patrick Massot (Apr 06 2021 at 19:26):

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

#### Johan Commelin (Apr 06 2021 at 19:41):

@Patrick Massot So `completion`

can do something nontrivial to a complete space?

#### Patrick Massot (Apr 06 2021 at 19:42):

No, it can make it smaller

#### Johan Commelin (Apr 06 2021 at 19:42):

In `strong_of_complete`

we are assuming that we have `complete_space`

and `semi_normed_group`

.

That should still imply `normed_group`

, because `t1`

implies `t2`

for topological groups.

#### Johan Commelin (Apr 06 2021 at 19:42):

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

#### Patrick Massot (Apr 06 2021 at 19:43):

Yes, t1 implies t2 for topological groups.

#### Patrick Massot (Apr 06 2021 at 19:45):

Is there code to fix? On which branch?

#### Johan Commelin (Apr 06 2021 at 19:48):

@Patrick Massot `semi_normed`

is the branch

#### Johan Commelin (Apr 06 2021 at 19:49):

I just checked: the final `sorry`

in `normed_spectral`

(9.6) just vanished completely :happy:

#### Patrick Massot (Apr 06 2021 at 19:50):

Is there anything to fix then?

#### Johan Commelin (Apr 06 2021 at 19:50):

Yes

#### Johan Commelin (Apr 06 2021 at 19:50):

`strong_of_complete`

is broken

#### Johan Commelin (Apr 06 2021 at 19:51):

Because it assumes that the objects are `normed_group`

s

#### Johan Commelin (Apr 06 2021 at 19:51):

And Lean doesn't know that `semi_normed_group`

+ `complete_space`

implies `normed_group`

.

#### Johan Commelin (Apr 06 2021 at 19:51):

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

#### Patrick Massot (Apr 06 2021 at 19:52):

This isn't true

#### Patrick Massot (Apr 06 2021 at 19:52):

I think you mean semi_normed_group + separated implies normed_group

#### Johan Commelin (Apr 06 2021 at 19:52):

But `complete_space`

implies `t1`

, right?

#### Patrick Massot (Apr 06 2021 at 19:53):

why?

#### Johan Commelin (Apr 06 2021 at 19:53):

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

#### Adam Topaz (Apr 06 2021 at 19:53):

Is it not true that a complete pseudo_metric_space is T2?

#### Adam Topaz (Apr 06 2021 at 19:54):

I agree about general uniform spaces btw

#### Patrick Massot (Apr 06 2021 at 19:56):

It is certainly true if you put separation in the definition of complete, but a priori I don't see why it would be automatic

#### Riccardo Brasca (Apr 06 2021 at 19:56):

Johan Commelin said:

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

I said that... I thought that the completion of a complete space was the same as the space :sweat_smile:

#### Johan Commelin (Apr 06 2021 at 19:56):

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

#### Johan Commelin (Apr 06 2021 at 19:57):

@Patrick Massot For me it's fine if we prove `strong_of_complete`

assuming `separated`

. Because we will only ever apply it to `completion foobar`

.

#### Johan Commelin (Apr 06 2021 at 19:57):

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

to `norm_eq_zero_iff`

.

#### Patrick Massot (Apr 06 2021 at 19:58):

The name `completion`

is maybe a bit unfortunate, but `separated_completion`

seemed too long.

#### Patrick Massot (Apr 06 2021 at 20:00):

And of course Bourbaki calls it completion only.

#### Patrick Massot (Apr 06 2021 at 20:01):

Assuming `semi_normed`

and `separated`

is a bit silly, this is equivalent to `normed_group`

, right?

#### Johan Commelin (Apr 06 2021 at 20:03):

Yes, but you are handed a `system_of_complexes`

, whose objects are by definition `semi_normed_group`

.

#### Johan Commelin (Apr 06 2021 at 20:03):

If `normed_group`

was a mixin on top of `semi_normed_group`

, there wouldn't be a problem. But of course that would be a gigantic refactor, and it's not even clear if it is desirable from a UX point of view.

#### Patrick Massot (Apr 06 2021 at 20:05):

I see

#### Johan Commelin (Apr 06 2021 at 20:07):

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

#### Patrick Massot (Apr 06 2021 at 20:07):

`cauchy_seq_of_le_geometric`

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

#### Johan Commelin (Apr 06 2021 at 20:09):

Maybe we can write a `def normed_group_of_separated`

and lift the `semi_normed_group`

structure to a `normed_group`

manually?

#### Johan Commelin (Apr 06 2021 at 20:09):

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

#### Patrick Massot (Apr 06 2021 at 20:10):

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

#### Patrick Massot (Apr 06 2021 at 20:10):

So maybe we should be lazy

#### Patrick Massot (Apr 06 2021 at 20:11):

Do we already have a def upgrading a pseudo normed group to a normed group using a proof of norm x = 0 implies x = 0?

#### Johan Commelin (Apr 06 2021 at 20:12):

pseudo normed groups don't even have a `has_norm`

at the moment. (And note that there can be elements with norm $\infty$).

#### Johan Commelin (Apr 06 2021 at 20:12):

Or did you mean `semi_normed_group`

?

#### Johan Commelin (Apr 06 2021 at 20:12):

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

#### Patrick Massot (Apr 06 2021 at 20:15):

Yes, I meant semi normed group

#### Riccardo Brasca (Apr 06 2021 at 20:18):

I don't remember writing it, but maybe it is more or less already there. The difference between `semi_normed_group`

and `normed_group`

is that the first extends `pseudo_metric_space`

, the latter `metric_space`

#### Riccardo Brasca (Apr 06 2021 at 20:18):

And `metric_space`

extends `pseudo_metric_space`

#### Patrick Massot (Apr 06 2021 at 20:29):

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

`lemma `