Dual snake lemma

Stream: condensed mathematics

[Riccardo Brasca]

Can someone (AKA @Peter Scholze ) give me a little hint for the math proof of the dual snake lemma? The precise statement I am trying to prove is

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

lemma weak_normed_snake_dual {k k' K K' r₁ r₂ : ℝ≥0}
  [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)
  (hg : ∀ c i (x : M c i), ∥g x∥ ≤ r₁ * ∥x∥)
  (Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ m+1+1) (y : M' c i),
    ∃ (x : M c i), g x = y ∧ ∥x∥ ≤ r₂ * ∥y∥)
  (hg : ∀ c i, (f.apply : N c i ⟶ M c i).range = g.apply.ker)
  (hfker : system_of_complexes.is_kernel f) :
  N.is_weak_bounded_exact (k * k') (K' * (K + 1)) m c₀

(with the constants at the end that will be changed).

So we have $g^\bullet \colon M^\bullet \to M'^\bullet$, of controlled norm and surjective, with $N^\bullet$ the system of kernels (let's ignore all the $c$, $kc$ and so on, so no restriction). We want to prove that $N^\bullet$ is blah blah exact. Let $n \in N^i$, so $n\in M^i$ and I can use exactness of $M^\bullet$ to produce $y \in M^{i-1}$. I guess we need to look at what happens to $z = g(y)$. My idea was to use exactness of $M'$ to produce $z_1 \in M'^{i-2}$ and lift it to $y_1 \in M^{i-2}$. The standard snake lemma tells me to look at $y - d(y_1)$, that is in the kernel of $g$ and so it lies in $N^{i-1}$. But now this is not true anymore and I don't see how to produce an element in the kernel of $g$... thank's!!

[Peter Scholze]

Why is it not in the kernel of $g$? I'd have expected that this is true, at least after a further restriction?

[Riccardo Brasca]

Well, the image by $g$ is $z-d(z_1)$. By construction of $z_1$ we can control its norm using the norm of $d(z)$ (again I am ignoring restrictions). Now the norm of $d(z)$ is related to the norm of $d(y)$, but I don't see why anything of these things should be $0$.

[Peter Scholze]

Didn't you choose $z_1$ so that $z=d(z_1)$?

[Peter Scholze]

I have the feeling we really need to put all the $c$'s in to resolve this

[Riccardo Brasca]

Let me write all the details

[Riccardo Brasca]

Let $n_{k^2c} \in N^i_{k^2c}$, so $n_{k^2c}\in M^i_{k^2c}$ and I can use exactness of $M^\bullet$ to produce $y_{kc} \in M^{i-1}$ such that $||n_{kc}-d(y_{kc})|| \leq K || d(n_{k^2c})|| + \varepsilon$. Let $z_{kc} = g(y_{kc})$. By exactness of $M'$ we can find $z_{1,c} \in M'^{i-2}_c$ such that $||z_{c}-d(z_{1,c})|| \leq K' || d(z_{kc})|| + \varepsilon$. We can lift it to $y_{1,c} \in M^{i-2}_c$. Let consider $y_{c}-d(y_{1,c})$. Its image by $g$ is $z_{c}-d(z_{1,c})$ that satisfies $||z_{c}-d(z_{1,c})|| \leq K' || d(z_{kc})|| + \varepsilon$. Let $y'_c \in M^{i-1}_c$ be a lift of $z_{c}-d(z_{1,c})$ with norm smaller than $r_2||z_{c}-d(z_{1,c})||$. By construction $y_{c}-d(y_{1,c})-y'_c \in N^{i-1}$. We need to control $||n_c - d( y_{c}-d(y_{1,c})-y'_c )|| = ||n_c - d( y_{c}-y'_c )||$

[Peter Scholze]

Ah!! You are using weak exactness here! Actually, we only need the lemma in a situation where everything is complete, and anyways we know strong exactness

[Peter Scholze]

I'd guess one should also be able to prove it with weak exactness... let me try to do it on paper, but feel free to write up the version with strong exactness

[Riccardo Brasca]

OK, this eliminates the epsilon, but still I have $||z_{c}-d(z_{1,c})|| \leq K' || d(z_{kc})||$. Is $d(z_{kc})=0$?

[Riccardo Brasca]

Hmm, maybe trivially yes

[Peter Scholze]

Ah sorry I was starting with $n_{k^2c}$ in the kernel of $d$, in which case this would be trivially zero

[Peter Scholze]

OK, let me try to write down an actual argument...

[Peter Scholze]

maybe even for weak exactness (for consistency's sake)

[Peter Scholze]

By the way, if you have some $y$ such that $g(y)$ is small, as opposed to exactly $0$, you can always modify it by changing by a small lift of $g(y)$: This shows that there is some $y'$ close to $y$ with $g(y')=0$.

[Peter Scholze]

So coming back to the above, one ought to be able to prove that $z_c-d(z_{1,c})$ has norm bounded in terms of the norm of $d(n_{k^2c})$. Together with what I said in my previous message, this should be enough to conclude.

[Riccardo Brasca]

Ah yes, this looks promising. Let me check

[Peter Scholze]

How does it look?

[Riccardo Brasca]

So far I am here

Let $n_{k^2c} \in N^i_{k^2c}$, so $n_{k^2c}\in M^i_{k^2c}$ and I can use exactness of $M^\bullet$ to produce $y_{kc} \in M^{i-1}$ such that $||n_{kc}-d(y_{kc})|| \leq K || d(n_{k^2c})|| + \varepsilon$. Let $z_{kc} = g(y_{kc})$. By exactness of $M'$ we can find $z_{1,c} \in M'^{i-2}_c$ such that $||z_{c}-d(z_{1,c})|| \leq K' || d(z_{kc})|| + \varepsilon$. We can lift $z_{1,c}$ to $y_{1,c} \in M^{i-2}_c$. Let consider $y_{c}-d(y_{1,c})$, whose image by $g$ is $z_{c}-d(z_{1,c})$. Let $y'_c \in M^{i-1}_c$ be a lift of $z_{c}-d(z_{1,c})$ with norm smaller than $r_2||z_{c}-d(z_{1,c})||$. By construction $y_{c}-d(y_{1,c})-y'_c \in N^{i-1}$. We need to control
$||n_c - d( y_{c}-d(y_{1,c})-y'_c )|| \leq \\ || n_c - d( y_{c})|| + ||d( y'_c )|| \leq \\ || n_c - d( y_{c})|| + || y'_c || \leq \\ || n_c - d( y_{c})|| + r_2||z_{c}-d(z_{1,c})|| \leq \\ || n_c - d( y_{c})|| + r_2(K'|| d(z_{kc})|| + \varepsilon) \leq \\ ||n_{kc}-d(y_{kc})|| + r_2(K'|| d(z_{kc})|| + \varepsilon) \leq \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'|| d(z_{kc})|| + \varepsilon) = \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'|| d(g(y_{kc}))|| + \varepsilon) = \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'|| g(d(y_{kc}))|| + \varepsilon) = \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'|| g(n_{kc} - d(y_{kc}))|| + \varepsilon)$.

Now I don't see immediatly how to go from the norm of $y_{kc}$ to the norm of $d(n_{k^2c})$, but I was having lunch, and I didn't check the computations.

[Peter Scholze]

I think you need to be more careful with the estimate of $||d(z_{kc})||$: Use rather $d(z_{kc})=d(g(y_{kc})) = g(d(y_{kc})) = g(d(y_{kc})-n_{kc})$ and the estimate on $||n_{kc}-d(y_{kc})||$.

[Riccardo Brasca]

OK, so we have
$||n_c - d( y_{c}-d(y_{1,c})-y'_c )|| \leq \\ || n_c - d( y_{c})|| + ||d( y'_c )|| \leq \\ || n_c - d( y_{c})|| + || y'_c || \leq \\ || n_c - d( y_{c})|| + r_2||z_{c}-d(z_{1,c})|| \leq \\ || n_c - d( y_{c})|| + r_2(K'|| d(z_{kc})|| + \varepsilon) \leq \\ ||n_{kc}-d(y_{kc})|| + r_2(K'|| d(z_{kc})|| + \varepsilon) \leq \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'|| d(z_{kc})|| + \varepsilon) = \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'|| d(g(y_{kc}))|| + \varepsilon) = \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'|| g(d(y_{kc}))|| + \varepsilon) = \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'|| g(n_{kc} - d(y_{kc}))|| + \varepsilon) \leq \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'r_1|| n_{kc} - d(y_{kc})|| + \varepsilon) \leq \\ K || d(n_{k^2c})|| + \varepsilon + r_2(K'r_1K || d(n_{k^2c})|| + \varepsilon) = \\ || d(n_{k^2c})||(K + r_2r_1KK') + \varepsilon(1+r_2)$.

[Peter Scholze]

That's what we wanted, right?

[Riccardo Brasca]

Yes, this proves

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

lemma weak_normed_snake_dual {k k' K K' r₁ r₂ : ℝ≥0}
  [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)
  (hg : ∀ c i (x : M c i), ∥g x∥ ≤ r₁ * ∥x∥)
  (Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ m+1+1) (y : M' c i),
    ∃ (x : M c i), g x = y ∧ ∥x∥ ≤ r₂ * ∥y∥)
  (hg : ∀ c i, (f.apply : N c i ⟶ M c i).range = g.apply.ker)
  (hfker : system_of_complexes.is_kernel f) :
  N.is_weak_bounded_exact (k * k') (K + r₁ * r₂ * K * K') m c₀

I am 99% sure there will be no Lean problems (same for the strong version if we need it).

[Johan Commelin]

Wow! That went pretty fast! I remember that the original snake lemma took a bit more work

[Kevin Buzzard]

you mean the thing you proved as your first lean project ever in about 2018?

[Johan Commelin]

No, I meant the one in LTE

[Johan Commelin]

The original normed snake

[Kevin Buzzard]

Oh OK :-) I could imagine that Riccardo now was faster than you in 2018 :-)

[Johan Commelin]

What I proved in 2018 was the five lemma, and it also took some time (-;

[Riccardo Brasca]

Well, I have the math proof, not yet the Lean proof...

[Riccardo Brasca]

I will try to do it today

[Riccardo Brasca]

And the "subspace norm" is easier than the quotient norm...

[Riccardo Brasca]

@Johan Commelin With the new complexes, what is the strategy to deal with the following situation?

Let $M^\bullet$ a complex that is bla bla exact and $i \leq m$. I have $x \in M^i$, and I use exactness to build an element $y \in M^{i-1}$. Now I want to consider $x + d(y)$, where the $d$ is the one given in the definition of exactness (I mean, with i and j). If $i=0$ then $y \in M^0$, but $d(y)$ is still in $M^1$. Should I do a by_cases and avoid the addition if $i=0$? (This is going to work since anyway $y=0$ if $i=0$)

[Riccardo Brasca]

(deleted)

[Adam Topaz]

You can use the X_prev construction which gives the zero object if there is no previous object

[Riccardo Brasca]

I don't think I can chose, $y$ is given by

def is_bounded_exact
  (k K : ℝ≥0) (m : ℕ) [hk : fact (1 ≤ k)] (c₀ : ℝ≥0) : Prop :=
∀ c (hc : fact (c₀ ≤ c)) i (hi : i ≤ m) (x : C (k * c) i),
∃ (i₀ j : ℕ) (hi₀ : i₀ = i - 1) (hj : i + 1 = j)
  (y : C c i₀), ∥res x - C.d _ _ y∥ ≤ K * ∥C.d i j x∥

So it will be in $M^0$ if $i=0$. But C.d _ _ y = 0 in this case, since C.d 0 0 = 0,

[Adam Topaz]

I see... So to really use the new complexes API, I think this definition might need to be changed

[Johan Commelin]

I don't know what's best given the new complexes.

[Johan Commelin]

But my idea was indeed that you would get something in degree 0-1 = 0 and then use that C.d 0 0 = 0. So all should be well.

[Riccardo Brasca]

Ah wait, now I can write d _ _ y instead of just d y, and with the correct _ this should work

[Riccardo Brasca]

Hmm, it doesn't work: I really want to consider d i' i'+1 y, that is given by the exactness condition, and the idea is to add x to this. I guess that a by_cases will work :grimacing:

[Johan Commelin]

@Riccardo Brasca You can do cases i instead of by_cases.

[Johan Commelin]

That might save you nasty rewrites.

[Riccardo Brasca]

Yes, but then I will have i.succ everywhere... I will see

[Riccardo Brasca]

In any case the beginning of the proof is here
https://github.com/leanprover-community/lean-liquid/blob/normed_snake_dual/src/normed_snale_dual.lean

There are a lot of sorry in the calc bloc, but they should be easy

[Johan Commelin]

Riccardo Brasca said:

Yes, but then I will have i.succ everywhere... I will see

I hope dsimp only [nat.succ_eq_add_one] will fix that.

[Johan Commelin]

But by_cases is also an option, and then subst.

[Riccardo Brasca]

I only need i ≠ 0 to rewrite i' + 1 = i (here i' = i - 1) inside a differential. I was afraid of "motive is not type correct", but it worked

[Johan Commelin]

@Riccardo Brasca You've got snale in your file name :stuck_out_tongue_wink: :snail:

[Johan Commelin]

By the way, I think I've got the complexes ready to which we want to apply this lemma.
We want to prove that the complex on the left ("the kernel") is

((thm95.double_complex BD.data c_ r r' V Λ M (N c' r r' m)).col j).is_weak_bounded_exact (k₁ m) (K₁ m) m (c₀ m Λ)

But the constants (k₁ m) (K₁ m) still have to be defined, and we can basically make them whatever we want/need (-;

[Johan Commelin]

The need to be "large" in some sense. But we can give them a nice definitional shape if that is convenient.

[Riccardo Brasca]

Feel free to merge into master the branch normed_snake_dual, the statement should be correct.

[Riccardo Brasca]

Also the structure of the proof is there, I am killing all the mini sorry in the calc bloc to check that I didn't made stupid mistakes on paper

[Riccardo Brasca]

normed_snake_dual is now in master. The file contain 10 sorry at the moment.

The first one, in admissible_of_kernel said that a system of complexes, isomorphic to the kernel of a morphism of system of complexes with admissible domain, is admissible. This is obvious since we can compute the norm after applying the morphism. Is this a special case of something already there?

The next 8 sorry are trivial, 0 < 37+ε ^ 37 if 0 < ε.

The last one is the only one not completely easy: it is the theorem in the case i=0. The same proof does not literally apply, but indeed it should be easier. I will do it tomorrow, trying to avoid code duplication as much as possible.

[Riccardo Brasca]

Also, the giant calc should be golfed, there are lines, whose proof is rfl, that I don't understand why I need them.

[David Michael Roberts]

If we had a proof of the snail lemma for free that would be impressive https://doi.org/10.1016/j.jpaa.2016.06.001

[Riccardo Brasca]

Also the sorry corresponding to i=0 is now reduced to an (easy) inequality in ℝ. I pushed this to the branch normed_snake_dual, I will put it in master tomorrow.

[Johan Commelin]

Thanks @Riccardo Brasca, that's great work!

[Johan Commelin]

I don't think admissible_of_kernel follows from something that we already have.

[Riccardo Brasca]

Now all the sorry are completely trivial. I have some teaching stuff to do today, but I will finish it before the weekend.

[Riccardo Brasca]

BTW, to use lemmas like normed_group_hom.map_sub I had to change f m to f.apply m (here f : M ⟶ N is a morphism of system of complexes and m: M c i for some c and i). This is just a rfl or a change, but avoiding it would golf the proof a little bit. Am I missing something obvious here? library_search does not find a lemma saying exactly that.

[Johan Commelin]

Nah, I don't think we have such lemmas yet.

[Riccardo Brasca]

OK, I will add it. What is a good name? system_of_complexes.hom_apply?

[Johan Commelin]

Sounds good to me

[Riccardo Brasca]

weak_normed_snake_dual is sorry free (but still to be golfed).

[Riccardo Brasca]

Do we need the strong version?

[Johan Commelin]

@Riccardo Brasca Great! I don't think we need the strong version.

[Johan Commelin]

Thanks so much for doing this!

[Johan Commelin]

I realize that I was maybe a bit to fast with suggesting to abstract away r1 and r2 into constants.
How hard do you think it would be to replace the assumption

(Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ a + 1 + 1) (y : P c i),
    ∃ (x : N c i), g x = y ∧ ∥x∥ ≤ r₂ * ∥y∥)

with

(Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ a + 1 + 1) (\eps : \nnreal) (h\eps : 0 < \eps) (y : P c i),
    ∃ (x : N c i), g x = y ∧ ∥x∥ ≤ (r₂ + \eps) * ∥y∥)

[Peter Scholze]

I guess we don't need the strong version (although for this part of the argument, I think it wouldn't matter -- all argument should directly give the strong version here, and the constants would also be the same. But in the end we are just trying to get input into 9.6, and there only weak exactness is required).

[Riccardo Brasca]

What constant do you need? Now the result is that the kernel is K + r₁ * r₂ * K * K'-exact, with r₂ arbitrary. If ε is big then it will change the constant for sure.

[Johan Commelin]

Hmm... the point is that 9.2 gives us this "forall \eps > 0, the norm is bounded by r_2 + \eps"

[Johan Commelin]

For some r_2

[Johan Commelin]

Well, to be more precise: "forall \eps > 0, there exists a y such that ... , ..., the norm is bounded by r2 + \eps"

[Johan Commelin]

So in the proof of dual snake you can choose y such that \eps is as small as you want it to be

[Riccardo Brasca]

I see. This gives

(Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ a + 1 + 1) (y : P c i),
    ∃ (x : N c i), g x = y ∧ ∥x∥ ≤ (r₂ + 1) * ∥y∥)

So we automatically get K + r₁ * (r₂ + 1) * K * K'-exactness. If we want K + r₁ * r₂ * K * K'-exactness I have to check the proof, but I think it's OK.

[Riccardo Brasca]

(deleted)

[Johan Commelin]

Sounds good!

[Riccardo Brasca]

If we need the strong version I have proved it (it took 10 minutes, the same exact proof works, much easier then the cokernel case)

[Johan Commelin]

@Riccardo Brasca with the + \eps in the assumption?

[Riccardo Brasca]

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

lemma normed_snake_dual {k k' K K' r₁ r₂ : ℝ≥0}
  [hk : fact (1 ≤ k)] [hk' : fact (1 ≤ k')]
  {a : ℕ} {c₀ : ℝ≥0}
  (hN : N.is_bounded_exact k K (a + 1) c₀)
  (hP : P.is_bounded_exact k' K' (a + 1) c₀)
  (hN_adm : N.admissible)
  (hgnorm : ∀ c i (x : N c i), ∥g x∥ ≤ r₁ * ∥x∥)
  (Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ a + 1 + 1) (y : P c i),
    ∃ (x : N c i), g x = y ∧ ∥x∥ ≤ r₂ * ∥y∥)
  (hg : ∀ c i, (f.apply : M c i ⟶ N c i).range = g.apply.ker)
  (hfiso : ∀ c i, @isometry (M c i) (N c i) _ _ f.apply) :
  M.is_bounded_exact (k * k') (K + r₁ * r₂ * K * K') a c₀ :=

[Riccardo Brasca]

Is the same as the weak one. If you are ready to lose something in the constant at the end just use you assumption with ε and you will get M.is_bounded_exact (k * k') (K + r₁ * (r₂ + 1) * K * K') a c₀

[Riccardo Brasca]

If we really need M.is_bounded_exact (k * k') (K + r₁ * r₂ * K * K') a c₀ no problem, I will think about it

[Johan Commelin]

I don't think it's an urgent problem. But it is of course nice to optimize the constants.

[Johan Commelin]

(Now I need to run. I'll be gone for an hour or two. Ciao.)

[Riccardo Brasca]

My impression is that we can (easily ) prove that a system of complexes that is K + ε- weak exact for all 0 < ε is K- weak exact, so taking a sufficiently small ε in your Hg we would get K + r₁ * r₂ * K * K'-weak exactness.

[Riccardo Brasca]

For strong exactness, we can obtain K + r₁ * r₂ * K * K' + ε-exactness, but to get rid of the ε we have to modify the proof (I don't think K+ε-exactness implies K-exactness in general).

[Peter Scholze]

Yeah, I think in the strong version, with Johan's hypothesis, one will lose some $\epsilon$ in the conclusion.

[Peter Scholze]

Don't worry about any of this; we're having doubly-exponential growth at least in other parts of the argument...

[Riccardo Brasca]

I've golfed the proof a little bit and pushed to master. Now normed_snake_dual contains complete proofs of the dual weak snake lemma and of the dual strong snake lemma. The file is quite slow, but I guess we just use it and forget about it. (If we want to improve the speed, there are lemmas (proved by ring) that are used in both proof and that can be proved only once)