bounded exactness

Stream: condensed mathematics

[Johan Commelin]

In a long list of remarks on the blueprint (sent in a PM, I've fixed almost all of them), Kevin raised the following question. In the definition of (weak) bounded exactness, we have $k > 0$ and $c \ge c'_0$. After that, the text refers to $x \in C_{kc}^i$. Do we want $kc \ge c'_0$?

For the normed snake lemma, the definition as is, certainly worked fine.

[Riccardo Brasca]

We need restriction from $kc$ to $c$, don't we? So I have the impression that $k \geq 1$ is necessary

[Johan Commelin]

Ooh, you are right. We actually have that in the Lean repo.

[Johan Commelin]

https://github.com/PeterScholze/Analytic/pull/2

[Patrick Massot]

Johan, aren't you forgetting docs#nat.succ_le_of_lt?

[Patrick Massot]

Or maybe k isn't a natural number.

[Patrick Massot]

Oh, yes k is a norm constraint, not a graduation one, forget about that. I should have read the context instead of relying only on notations...

[Peter Scholze]

Yes sorry, $k\geq 1$ always. One sometimes forgets to mention this when in fact $k\gg 100000$ is implicit in your head ;-)

[Patrick Massot]

I've thought a bit about the weak exactness lemmas yesterday night. I'm pretty confident the first lemma will be not so bad, there are clear sublemmas to extract there. However, before pressing on, I feel like we should discuss whether we really want to keep a single $k$ in the definition of weak exactness. Currently $k$ is used both a the restriction depth factor and the norm bound. This is a bit confusing to me. When I first read that definition I only remembered that it was a definition about a subtle relation between restriction depth and norm bounds. Now I feel this is completely artificial. And if we are interested in explicit bounds on $k$ then probably we should track both uses of $k$ independently.

[Peter Scholze]

@Patrick Massot You are absolutely right, $k$ plays two roles that have nothing to do with each other. I was just too lazy and didn't want to have yet another variable.

[Peter Scholze]

It definitely makes sense to turn it into two variables, it will also improve estimates

[Patrick Massot]

I'll have time this afternoon to tackle these lemmas relating weak exactness and exactness for complexes of complete normed groups. Is this still relevant or were there changes that made them obsolete?

[Peter Scholze]

I think that's still relevant!

[Patrick Massot]

I didn't have time for Lean code in the end, but I did went through the LaTeX code. Riccardo, could you have a look at the beginning of the newly created Section 4 of blueprint.pdf up to the bottom of Page 7?

[Riccardo Brasca]

I am looking at it

[Patrick Massot]

Recent changes to the blueprint:

• Gather all normed homological algebra in a dedicated Section 4 instead of splitting it between the main text and an appendix (which was simply following the structure of the lecture notes where it made sense to hide technical stuff).
• Split off the two uses of $k$ in the definition of (weak)-exactness
• State two extra small technical lemmas split off the proof of our previous pair of technical lemma (I can see some fractal appearing there)
• Simplify notations in the normed homological algebra stuff.
• Slightly rephrase the first two technical proofs so that we don't choose magic sequences of positive real numbers upfront.

[Riccardo Brasca]

Is "closed element" standard terminology?

[Patrick Massot]

I'm only pretending to know complexes that are not the de Rham complex maybe?

[Patrick Massot]

Closed differential form is certainly a standard terminology.

[Riccardo Brasca]

Ah, sure

[Patrick Massot]

Anyway, the fact that you asked means we should avoid this terminology. There are enough unusual things going on here.

[Riccardo Brasca]

Looks good to me

[Kevin Buzzard]

Would "cocycle" and "coboundary" be better?

[Patrick Massot]

Probably

[Patrick Massot]

I still find it weird that you are happy to use "exact" but not "closed".

[Patrick Massot]

Anyway, I'll try to Lean that soon. Hopefully those little reformulation will make it slightly easier (at least it's less frightening).

[Riccardo Brasca]

Probably because exact is less used, so my mind only find one "instance". Closed relates to closed subspaces (that were relevant for the story of weak exactness) and complete... but this is just how my brain works

[Patrick Massot]

I pushed the Zeeman effect refactor. It splits the role of $k$ in the bounded exactness definitions into a depth factor and norm bound. The new definitions are:

def is_bdd_exact_for_bdd_degree_above_idx
  (k K : ℝ≥0) (m : ℤ) [hk : fact (1 ≤ k)] (c₀ : ℝ≥0) : Prop :=
∀ c ≥ c₀, ∀ i < m,
∀ x : C (k * c) (i+1),
∃ y : C c i, ∥res x - d y∥ ≤ K * ∥d x∥

def is_weak_bdd_exact_for_bdd_degree_above_idx
  (k K : ℝ≥0) (m : ℤ) [hk : fact (1 ≤ k)] (c₀ : ℝ≥0) : Prop :=
∀ c ≥ c₀, ∀ i < m,
∀ x : C (k * c) (i+1),
∀ ε > 0, ∃ y : C c i, ∥res x - d y∥ ≤ K * ∥d x∥ + ε

Along the way, note also how new coercions to functions and smarter implicit arguments allow to write things like x : C (k * c) (i+1) or ∥res x - d y∥ ≤ K * ∥d x∥ (Peter, this is part of what Lean's elaborator can do, no need for decorations here).

[Patrick Massot]

The normed snake lemma (weak bounded exactness version) becomes:

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_bdd_exact_for_bdd_degree_above_idx k K m c₀)
  (hM' : M'.is_weak_bdd_exact_for_bdd_degree_above_idx k' K' m c₀)
  (hM'_adm : M'.admissible)
  (hf : ∀ c i, is_strict (f.apply : M c i ⟶ M' c i))
  (Hf : ∀ (c : ℝ≥0) (i : ℤ) (hi : i ≤ m + 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_bdd_exact_for_bdd_degree_above_idx (k''*k*k') (K'*(K*K'' + 1)) (m - 1) c₀

[Patrick Massot]

Note that I also took the opportunity to stop assuming the restriction depth factor for both systems of complexes and f, and same for the norm bounds.

[Patrick Massot]

It doesn't cost anything anyway since separating both uses of $k$ means that we don't have to align constants anymore.

[Patrick Massot]

Technical note: the coercion that allows to write x : C c i for $x \in C^i_c$ is completely smooth. The coercion from morphisms of system of complexes to functions is less efficient. It works great when applying a morphism to an element. But the elaborator doesn't understand (f : M c i ⟶ M' c i). That's why f.apply still appears in the statement above, and this causing some pain in the proof.

[Patrick Massot]

One could argue that writing f.apply everywhere is less painful. This would be easy to revert (although I wasn't careful enough to have a commit containing only that move...).

[Patrick Massot]

Important note: the statement of Proposition 9.6 now has a random constant. It hasn't been updated.

[Johan Commelin]

@Patrick Massot thanks a lot for this refactor!

[Johan Commelin]

(Today I learned about the Zeeman effect :laughing:)

[Riccardo Brasca]

Is someone (and I mean @Patrick Massot ) working on lemmas like system_of_complexes.controlled_y? If not I think I can prove it during the week.

[Johan Commelin]

Yes, Patrick has been looking at this. But he also hit some DTT troubles. We need a principled solution to the following issue: if x : C c i and you want to say that x is in the image of d, then you get some y : C c (i - 1) such that d y = x. Except that this doesn't typecheck, because d y : C c (i - 1 + 1).
And i - 1 + 1 is not defeq to i. This is of course a very annoying stupidity. But we'll need to find a smooth solution, or otherwise we'll have a lot of very painful hours ahead of us, and the resulting code will be awful to read.

[Bhavik Mehta]

Does the eq_to_hom sort of idea work here? Specifically, does it work to make a morphism C c i -> C c j given i = j, and insert it in the equality? I think this idea has been successful in abstract categories, perhaps it's appropriate here as well

[Riccardo Brasca]

We already have system_of_complexes.congr that does that. It has been written by Johan, so I guess he sees some troubles in using it a lot

[Adam Topaz]

Just thinking out loud here: What if we redefine complexes so that the d is defined on the whole complex at once, not on the individual graded components? This is the usual thing we do on paper, where dis defined on the direct sum of the graded components.

[Johan Commelin]

@Bhavik Mehta it doesn't make the code pleasant to look at. Once you start chasing elements through diagrams, you don't want to constantly tell Lean that eq_to_hom commutes with foo, bar, and quux.

[Adam Topaz]

I know that these complexes were defined elsewhere (in mathlib), so this would be a significant change.

[Kevin Buzzard]

Why not just take the direct sum of all the objects?

[Johan Commelin]

And endow it with the sup norm? Maybe it works... we'll have to experiment

[Kevin Buzzard]

The fix which Mario sometimes advertises is the sigma type,i.e. the disjoint union of the objects. But because these things are groups, the direct sum seems more natural.

[Adam Topaz]

Or you can have the best of both worlds: Define a new thing, called D or something, on the sigma type (or direct sum, whatever), and add an axiom that it agrees with d on the graded components.

[Adam Topaz]

Then just restate things in terms of D.

[Johan Commelin]

Currently, my idea was to have d take to arguments i j and mover from C c i to C c j. It should automatically infer a proof that j = i + 1. However, auto_params don't play well with bundled functions, I just discovered. See the question in #general

[Riccardo Brasca]

We can maybe have two version, one like the current one and one like the one you want, but where we write the proof that j = i + 1 by hand, so most of the time we use the normal one, and when needed we use the other one.

[Johan Commelin]

I think the direct-sum idea is also interesting, but I would like to see some code to know what it would really look like

[Riccardo Brasca]

Mmm, I see that then we will have to chose which one to use in the definition of exact, that is probably not a good thing

[Sebastien Gouezel]

Would something like d {i} {j} (h : j = i + 1 . my_tactic) (x : C i) : C j := ... be fine, where my_tactic would try refl and j = j - 1 + 1 and so on (where the "and so on" would not need to be able to treat everything, only what comes up in practice)? Or is it the problem you mention in the other thread that prevents this from working?

[Johan Commelin]

Right, but then we no longer have a bundled morphism...

[Patrick Massot]

I apologize for the secret work shared only in private messages with Johan. This is a bad habit inherited from the perfectoid project when we were only three contributors. Indeed I started to work on those lemmas and hit issues with dependent types. The following is a piece of not quite working code for people who want to play with those issues:

import data.real.nnreal

open_locale nnreal

structure mock_complex :=
(obj : ℝ≥0 → ℤ → Type)
(differential : ∀ c i, obj c i → obj c (i+1))
(restriction : ∀ c' c i, c ≤ c' → obj c' i → obj c i)
(restriction_func : ∀ c c' c'' i (h : c ≤ c') (h' : c' ≤ c'') (x : obj c'' i),
  restriction c' c i h (restriction c'' c' i h' x) = restriction c'' c i (h.trans h') x)
(commute : ∀ c c' i (h : c ≤ c') (x : obj c' i),
  differential c i (restriction c' c i h x) = restriction c' c (i+1) h (differential c' i x))

instance : has_coe_to_fun mock_complex :=
⟨λ C, ℝ≥0 → ℤ → Type, λ C, C.obj ⟩

section
open tactic

example {c c' c'' : ℝ≥0} (h : c ≤ c') (h' : c' ≤ c'') : c ≤ c'' :=
begin
  rw ← nnreal.coe_le_coe at *,
  linarith,
end

lemma stupid_one {c k : ℝ≥0} (h : 1 ≤ k) : c ≤ k*c:=
begin
  conv_lhs { rw ← one_mul c },
  exact mul_le_mul_right' h c
end

lemma stupid_two {c k : ℝ≥0} (h : 1 ≤ k) : c ≤ k^2*c:=
begin
  rw [pow_two, mul_assoc],
  have : c ≤ k*c := stupid_one h,
  conv_lhs { rw ← one_mul c },
  apply mul_le_mul ; try { assumption } ; exact nnreal.zero_le_coe
end

lemma stupid_three {c k : ℝ≥0} (h : 1 ≤ k) : k*c ≤ k^2*c:=
begin
  rw [pow_two, mul_assoc],
  exact stupid_one h,
end

meta def magic : tactic unit :=
do (assumption <|>
   `[rw ← nnreal.coe_le_coe at *, linarith]) <|>
   `[simp [stupid_one, stupid_two, stupid_three, *]] <|>
   target >>= trace

end

def res {C : mock_complex} {c c' : ℝ≥0} {i : ℤ} (x : C c' i) (hc : c ≤ c' . magic) : C c i :=
C.restriction c' c i hc x

def d {C : mock_complex} {c : ℝ≥0} {i : ℤ} (x : C c i) : C c (i+1) :=
C.differential c i x

lemma d_res {C : mock_complex} {c c' : ℝ≥0} {i : ℤ} (x : C c' i) (hc : c ≤ c') :
  d (res x) = res (d x) :=
by apply C.commute

lemma res_res {C : mock_complex} {c c' c'' : ℝ≥0} {i : ℤ} (x : C c'' i) (h : c ≤ c') (h' : c' ≤ c'') :
  res (res  x) = res x :=
by apply C.restriction_func

lemma res_res_mul {C : mock_complex} {c k : ℝ≥0} {i : ℤ} (x : C (k^2*c) i) (h : 1 ≤ k) :
  @res C c (k*c) i (res x : C (k*c) i) (by simp [stupid_one, stupid_two, stupid_three, *]) = res x :=
by apply C.restriction_func

[Adam Topaz]

If we're playing with these auto param tricks, why not just play the [fact (j = i + 1)] game again?

[Patrick Massot]

We tried this game already. It doesn't seem to be powerful enough.

[Adam Topaz]

Ah okay.

[Patrick Massot]

We need a more powerful proof search.

[Patrick Massot]

In principle the auto parameter trick is allowed to run any tactic you want. I write "in principle" because there are issues. Part of the issue is with implicit vs explicit but the main one is elaboration order: at which stage of the elaboration does the tactic kicks in?

[Patrick Massot]

In the case that doesn't work at the very end of the above snippet, the tactic gets c \le ?m_1 as its goal, and obviously this is not very promising.

[Adam Topaz]

So adding an instance like the following is not enough?

instance {i j : ℤ} [h : fact (j = i + 1)] : fact (j-1 = i) := sorry

[Adam Topaz]

I'm getting no errors with the code snippet above. Am I supposed to?

[Patrick Massot]

You'll get an error if you replace the last statement by something readable.

[Adam Topaz]

Oh :)

[Adam Topaz]

This is slightly more readable, IMO:

import data.real.nnreal

open_locale nnreal

structure mock_complex :=
(obj : ℝ≥0 → ℤ → Type)
(differential : ∀ c i, obj c i → obj c (i+1))
(restriction : ∀ c' c i, c ≤ c' → obj c' i → obj c i)
(restriction_func : ∀ c c' c'' i (h : c ≤ c') (h' : c' ≤ c'') (x : obj c'' i),
  restriction c' c i h (restriction c'' c' i h' x) = restriction c'' c i (h.trans h') x)
(commute : ∀ c c' i (h : c ≤ c') (x : obj c' i),
  differential c i (restriction c' c i h x) = restriction c' c (i+1) h (differential c' i x))

instance : has_coe_to_fun mock_complex :=
⟨λ C, ℝ≥0 → ℤ → Type, λ C, C.obj ⟩

section
open tactic

example {c c' c'' : ℝ≥0} (h : c ≤ c') (h' : c' ≤ c'') : c ≤ c'' :=
begin
  rw ← nnreal.coe_le_coe at *,
  linarith,
end

lemma stupid_one {c k : ℝ≥0} (h : 1 ≤ k) : c ≤ k*c:=
begin
  conv_lhs { rw ← one_mul c },
  exact mul_le_mul_right' h c
end

lemma stupid_two {c k : ℝ≥0} (h : 1 ≤ k) : c ≤ k^2*c:=
begin
  rw [pow_two, mul_assoc],
  have : c ≤ k*c := stupid_one h,
  conv_lhs { rw ← one_mul c },
  apply mul_le_mul ; try { assumption } ; exact nnreal.zero_le_coe
end

lemma stupid_three {c k : ℝ≥0} (h : 1 ≤ k) : k*c ≤ k^2*c:=
begin
  rw [pow_two, mul_assoc],
  exact stupid_one h,
end

meta def magic : tactic unit :=
do (assumption <|>
   `[rw ← nnreal.coe_le_coe at *, linarith]) <|>
   `[simp [stupid_one, stupid_two, stupid_three, *]] <|>
   target >>= trace

end

def res {C : mock_complex} {c c' : ℝ≥0} {i : ℤ} (x : C c' i) (hc : c ≤ c' . magic) : C c i :=
C.restriction c' c i hc x

def res' {C : mock_complex} (c : ℝ≥0) {c' : ℝ≥0} {i : ℤ} (x : C c' i) (hc : c ≤ c' . magic) : C c i :=
C.restriction c' c i hc x

def res'' {C : mock_complex} (c c' : ℝ≥0) {i : ℤ} (x : C c' i) (hc : c ≤ c' . magic) : C c i :=
C.restriction c' c i hc x

def d {C : mock_complex} {c : ℝ≥0} {i : ℤ} (x : C c i) : C c (i+1) :=
C.differential c i x

lemma d_res {C : mock_complex} {c c' : ℝ≥0} {i : ℤ} (x : C c' i) (hc : c ≤ c') :
  d (res x) = res (d x) :=
by apply C.commute

lemma res_res {C : mock_complex} {c c' c'' : ℝ≥0} {i : ℤ} (x : C c'' i) (h : c ≤ c') (h' : c' ≤ c'') :
  res (res  x) = res x :=
by apply C.restriction_func

lemma res_res_mul {C : mock_complex} {c k : ℝ≥0} {i : ℤ} (x : C (k^2*c) i) (h : 1 ≤ k) :
  res'' c (k * c) (res x) = res x :=
by apply C.restriction_func

[Adam Topaz]

But of course the user should know that res' and res'' are just res with more variables being made explicit.

[Adam Topaz]

I tried using res' for the last lemma as well, but I (obviously...) ran into the same metavariable issue that @Patrick Massot mentioned.

[Patrick Massot]

Yes, this issue is independent of what variables are made explicit. On paper Peter explicits both c and c'. In Lean it would be fair to explicit the one that cannot be inferred by looking at the type of x. But we could also put type annotations when needed. This is orthogonal to the issue at hand.

[Peter Scholze]

Is it possible to explain (to a layperson like me) why $i-1+1$ causes such problems? Would $i+1+1$ vs. $i+2$ also cause such issues?

[Adam Topaz]

The issue is that we're working with dependent types C i which depend on i. We then have some term x : C i, and we want to view it as a term of type C (i-1+1). But i-1+1 is not definitionally equal to i, so C i and C (i-1+1) are not "the same" by definition. You can do what essentially amounts to rewriting along the equality i - 1 + 1 = i, but then you have to carry around the fact that you did this rewriting and it gets messy and annoying very quickly.

[Mario Carneiro]

At least for nat, i+1+1 is defeq to i+2 so you are okay there

[Adam Topaz]

That's not the case for integers, is it?

[Adam Topaz]

(It's true for nat)

[Mario Carneiro]

I think the associativity part might cause a problem over int

[Peter Scholze]

But I guess $1+i$ and $i+1$ are not "defeq", even in nat?

[Adam Topaz]

Right:

example {i : ℤ} : i + 2 = i + (1 + 1) := rfl -- works
example {i : ℤ} : i + 2 = i + 1 + 1 := rfl -- fails

[Mario Carneiro]

no, defeq doesn't have most equalities you would want

[Mario Carneiro]

so it's best practice to structure things such that you don't need to rely on what is and isn't defeq

[Peter Scholze]

but this certainly sounds like the kind of thing that ought to be automatable (is that a word?). What is the problem with writing a tactic taking care of such issues?

[Adam Topaz]

That's more-or-less what @Patrick Massot and @Johan Commelin were trying to do in the code above.

[Johan Commelin]

For me the problem is that I'm still not good enough at writing robust tactics :see_no_evil:

[Peter Scholze]

OK, but it should be standard practice to have a dependent type over integers, and this issue should always come up then, it seems? So I would have expected that's the kind of thing somebody has already written a tactic for

[Johan Commelin]

But once we (Patrick, Adam, me) can write down a precise description of what the tactic should do, then there are enough people around here that can help us out

[Johan Commelin]

Unfortunately it isn't there yet. We regularly consider things like $\R^n$, where in principle the same problem occurs. But usually there are "easy" solutions.

[Johan Commelin]

I think homological algebra is the first place where this bites you hard.

[Peter Scholze]

Aha, I see!

[Johan Commelin]

And we've done a little bit of homological algebra before. But nothing as serious as chasing elements through complexes of normed groups.

[Mario Carneiro]

Part of the issue is that even with the best tactics you can't hide this from the user, once you have a dependent type over integers the issues already become apparent, and a tactic can't actually make things defeq in order to make the desired statements typecheck

[Peter Scholze]

I know, that's serious business! :stuck_out_tongue:

[Johan Commelin]

@Mario Carneiro Is that really true? I think there must be ways to make it almost transparent.

[Johan Commelin]

What we need is a sort of renormalize tactic, that will put all the indices in some normal form.

[Mario Carneiro]

You have to insert a cast to apply a non-definitional equality, and the user has to see and manipulate this

[Johan Commelin]

So x : C (k * c) (i - 1 + 1) gets replaced with x : C (k * c) i

[Mario Carneiro]

maybe if the tactic pulled everything back into a nondependent type this could be made more ergonomic

[Johan Commelin]

Mario Carneiro said:

You have to insert a cast to apply a non-definitional equality, and the user has to see and manipulate this

No, I claim that we can hide this behind an api.

[Mario Carneiro]

aka "$\Sigma$ = :rainbow: "

[Mario Carneiro]

I'm still not there yet on what exactly the automation task is that a hypothetical renormalize tactic would do

[Johan Commelin]

Here's a final part of a goal (I've turned on all implicit arguments):

hy :
  ∥⇑(@res C (k * c) c (i - 1 + 1 + 1) _) (@congr C (k * c) (k * c) (i + 1) (i - 1 + 1 + 1) x _ _) -
        ⇑(@d C c (i - 1 + 1) (i - 1 + 1 + 1) _) y∥ ≤
    ↑K * ∥⇑(@d C (k * c) (i + 1) (i - 1 + 1 + 1 + 1) _) x∥
⊢ ∥⇑(@res C (k * c) c (i + 1) _) x - ⇑(@d C c (i - 1 + 1) (i + 1) _) y∥ ≤
    ↑K * ∥⇑(@d C (k * c) (i + 1) (i + 1 + 1) _) x∥

[Mario Carneiro]

what are the types of res, d and congr

[Johan Commelin]

But until that point, everything is taken care of by an api.

def congr {C : system_of_complexes} {c c' : ℝ≥0} {i i' : ℤ}
  (x : C c i) (hc : c = c' . magic) (hi : i = i' . magic') :
  C c' i' :=
congr_hom _ hc hi x

/-- `C.d` is the differential `C c i ⟶ C c (i+1)` for a system of complexes `C`. -/
def d {C : system_of_complexes} {c : ℝ≥0} {i j : ℤ} [hj : fact (j = i + 1)] :
  C c i ⟶ C c j :=
(C.obj $ op c).d i ≫ congr_hom _ rfl hj.symm

def res {C : system_of_complexes} {c' c : ℝ≥0} {i : ℤ} [h : fact (c ≤ c')] :
  C c' i ⟶ C c i :=
(C.map (hom_of_le h).op).f i

[Johan Commelin]

This means that in statements like

def is_bdd_exact_for_bdd_degree_above_idx
  (k K : ℝ≥0) (m : ℤ) [hk : fact (1 ≤ k)] (c₀ : ℝ≥0) : Prop :=
∀ c ≥ c₀, ∀ i < m,
∀ x : C (k * c) (i+1),
∃ y : C c i, ∥res x - d y∥ ≤ K * ∥(d x : C _ (i+1+1))∥

The res x and d y help each other to figure out the indices.

[Johan Commelin]

Probably, with the Lean4 elaborator, we could make things even better. But Lean4 doesn't have mathlib :sad: So we can't transition to that before summer.

[Mario Carneiro]

Okay, these look good; but then why is i-1+1+1 an index in your goal?

[Johan Commelin]

you mean in hy?

[Mario Carneiro]

yeah

[Mario Carneiro]

I would keep all indices in the C c i to natural things like i+1, i, i-1 etc

[Johan Commelin]

cases H c hc (i-1) (by linarith) (congr x rfl) with y hy,
gives me
y : ↥(⇑C c (i - 1 + 1)),

[Mario Carneiro]

don't use rfl

[Mario Carneiro]

congr x (_ : i-1+1+1=i+1) or so

[Johan Commelin]

nope, that rfl is taking care of k * c = k * c.

[Johan Commelin]

I don't know why the auto_param doesn't kick in. The elaboration order isn't optimal there.

[Johan Commelin]

But I guess your point is that we should help lean with the second auto_param anyway.

[Mario Carneiro]

There is a type ascription you could put on something, but not knowing the types of things it's hard to say exactly what

[Johan Commelin]

Well... here is H

H :
  ∀ (c : ℝ≥0),
    c ≥ c₀ →
    ∀ (i : ℤ),
      i < m - 1 →
      ∀ (x : ↥(⇑C (k * c) (i + 1 + 1))),
        ∃ (y : ↥(⇑C c (i + 1))),
          ∥⇑(@res C (k * c) c (i + 1 + 1) _) x - ⇑(@d C c (i + 1) (i + 1 + 1) _) y∥ ≤
            ↑K * ∥⇑(@d C (k * c) (i + 1 + 1) (i + 1 + 1 + 1) _) x∥,

[Johan Commelin]

And as you can see, it talks about i + 1 in the type of y, but then we feed it i - 1 as argument to H

[Johan Commelin]

So you are bound to get a y : C _ (i - 1 + 1)

[Mario Carneiro]

Does the auto_param try to reduce i+1+1 to i+2 (without being told the termi+2)?

[Johan Commelin]

That auto_param only tries refl, assumption, ring because I don't know how to do better

[Mario Carneiro]

simp with lemmas like i + a + b = i + (a + b) and then norm_num might work

[Johan Commelin]

at y?

[Mario Carneiro]

at everything

[Mario Carneiro]

I mean I guess it's fine to have these terms around for a little while but they should be cleaned up, either by a cleanup tactic that you call when things are getting out of hand or in the magic auto_params

[Johan Commelin]

yes, so I think we need that cleanup tactic.

[Johan Commelin]

Is this the kind of thing that you write in your lunch break?

[Mario Carneiro]

It is my lunch break :grinning_face_with_smiling_eyes:

[Johan Commelin]

I pushed these experiments to wip_dtt_d_magic of the LTE repo

[Johan Commelin]

Mario Carneiro said:

It is my lunch break :grinning_face_with_smiling_eyes:

I know, hence my question :laughing:

[Mario Carneiro]

I think that it's possible for a carefully crafted rw to simplify away all instances of i+1+1 to i+2 in H

[Johan Commelin]

But that's not the issue, right? Those are defeq anyway.

[Mario Carneiro]

no, this is int

[Johan Commelin]

We need a cleanup tactic that replaces y : C _ (i - 1 + 1) by y : C _ i

[Mario Carneiro]

but that doesn't particularly matter, I can say the same about other int expressions

[Mario Carneiro]

but I'm talking specifically about H, where everything is still bound. Once you put it in your context with cases it gets harder

[Johan Commelin]

Aha, I see. Well, I don't care about having all expressions be of the form i-1-1-1 or i +1+1+1+1+1

[Johan Commelin]

As long as they are all in some normal form

[Mario Carneiro]

I was thinking more like i+2, i+1, i, i-1

[Johan Commelin]

sure, if that is easier (-;

[Johan Commelin]

But what can you do in H, if it talks about i + 1, and then you feed it i := i' - 1.

[Mario Carneiro]

then you call the cleanup tactic on the result

[Patrick Massot]

I think we need to work more on my baby version before getting Mario's help

[Johan Commelin]

Aah, you mean I first specialize to H (i' - 1), then clean up, then do cases?

[Mario Carneiro]

yes

[Patrick Massot]

In particular that version doesn't depend on anything from the project (or even from the category theory part of mathlib).

[Mario Carneiro]

actually H is too bound atm, it is best if i is free but x and y are not

[Heather Macbeth]

We need a normalization for expressions which are elements the ring of integer polynomials in i, i', j, etc, modulo a certain number of polynomial identities.

[Johan Commelin]

@Patrick Massot But we need to upgrade it slightly to use bundled functions.

[Mario Carneiro]

because rw "doesn't work under binders"

[Patrick Massot]

Yes, we need to upgrade it, that's why I wrote: we need to work more before asking for specific help.

[Mario Carneiro]

but like @Patrick Massot says, I'm very close to suggesting that you make a standalone version of this problem that I can hack on

[Johan Commelin]

@Mario Carneiro you are a genius!

[Johan Commelin]

lemma is_bdd_exact_for_bdd_degree_above_idx_of_shift  {k K : ℝ≥0} {m : ℤ} [hk : fact (1 ≤ k)] {c₀ : ℝ≥0}
  (H : ∀ c ≥ c₀, ∀ i < m - 1, ∀ x : C (k * c) (i + 1 + 1),
   ∃ y : C c (i + 1), ∥res x - d y∥ ≤ K * ∥(d x : C _ (i+1+1+1))∥) :
   C.is_bdd_exact_for_bdd_degree_above_idx k K m c₀ :=
begin
  intros c hc i hi x,
  specialize H c hc (i-1) (by linarith),
  rw [sub_add_cancel] at H,
  exact H x,
end

[Johan Commelin]

Works like a charm :tada: :octopus:

[Peter Scholze]

It's been great fun reading along, thanks for the explanations!

[Patrick Massot]

Peter Scholze said:

It's been great fun reading along, thanks for the explanations!

As you can see, we're not yet at a stage where such a software can be used while ignoring ugly implementations details that have no mathematical content at all. But we'll get there eventually.

[Patrick Massot]

It's nice that this lemma works but I'm a bit worried that we get tempted to use it to push back the moment where the issue will have to be solved for real (and then we'll have to redo thousands of lines of code).

[Mario Carneiro]

I don't think we know what the solution looks like yet though. We need a decent amount of test code before we can see what works

[Johan Commelin]

What do people think of renaming is_bdd_exact_for_bdd_degree_above_idx to is_bounded_exact (and similarly for weak exactness). I think it helps with readability, and it should be clear that the other conditions are implied.

[Johan Commelin]

Done

[Patrick Massot]

I stopped working on this for a while because I was hoping that DTT issues with complexes would improve. But this doesn't seem to be coming soon, so I pushed in our broken setup and proved complete weakly bounded exact complexes are bounded exact: https://github.com/leanprover-community/lean-liquid/commit/fefeb5e9cb7ea2edb55371882e944f4a1e774586

[Patrick Massot]

I'd very interested in seeing a tactic, or at least a user guide, simplifying the endless stream of stupid inequalities. Clearly we don't have a usable tool there yet.

[Patrick Massot]

The proof is 110 lines long and most of it should be completely automatic.

[Patrick Massot]

Also for the record: the blueprint proof is not correct because we don't ask that $K$ is positive (actually we don't even ask that it's nonnegative, whereas it could well be negative if all the normed groups involved are trivial). So I had to replace some $K$ by if K > 0 then K else 1. And the formal statement that I wrote a couple of weeks ago missed the completeness assumption...

[Patrick Massot]

Oh, and I almost forgot: the blueprint was also missing an argument invoking https://github.com/leanprover-community/lean-liquid/blob/fefeb5e9cb7ea2edb55371882e944f4a1e774586/src/system_of_complexes/basic.lean#L211-L213

[Patrick Massot]

For those who did not follow: this proof is not in the lecture notes, it was sketched by Peter as a little tactical change in the main proofs and details were (almost) filled in by Riccardo and myself.

[Sebastien Gouezel]

I didn't follow the discussion on complexes closely, but I was pretty convinced by a suggestion by Johan, if I remember correctly. Which was: define a group morphism d' i j for all i j, which is equal to 0 if j is not i + 1, and to the usual d followed by a cast if j = i+1. Possibly with variations in which the i could be implicit when you apply it to x : C i. Did it turn out to be not so practical?

[Adam Topaz]

If I recall correctly this approach didn't really improve anything.

[Adam Topaz]

Same goes for the approach where you define it as a functor from $\mathbb{Z}$ (with the poset structure) to abelian groups satisfying some condition.

[Adam Topaz]

It seems the moral of this story is that one should think of complexes as functors from some indexing category, and equality in this index category just like any other isomorphism, and hope that automation will eventually save the day.

[Johan Commelin]

I think the proposal that Sebastian is talking about hasn't really been tried yet.

[Johan Commelin]

At least I haven't properly tested it... but I have been to distracted by other things lately :expressionless:

[Peter Scholze]

@Patrick Massot I'm glad this implication worked out! Now I'm eagerly waiting for the next trouble ya'll find :-)

[Sebastien Gouezel]

Sebastien Gouezel said:

I didn't follow the discussion on complexes closely, but I was pretty convinced by a suggestion by Johan, if I remember correctly. Which was: define a group morphism d' i j for all i j, which is equal to 0 if j is not i + 1, and to the usual d followed by a cast if j = i+1. Possibly with variations in which the i could be implicit when you apply it to x : C i. Did it turn out to be not so practical?

There's something I like with this proposition: in degree i, you can define the closed guys as (d' i (i+1)).ker, and the exact guys as (d' (i-1) i).range, and then the cohomology as their quotient, without having ever to check that (i-1) + 1 = i. And in fact it also works in degree i = 0, where this equality fails because of nat subtraction (but still (d' (0-1) 0).range is the zero submodule, so everything is fine). This means that for $\N$-indexed complexes you don't need to define things in a specific way at i = 0.

[Riccardo Brasca]

Is there something subtle in the definition of completion of a system of complexes I am missing? It is a sorry at the moment, but we have completion of normed groups, so it seems easy to write

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/fd2e905e64fad39a0650f3cea374f55357842a45/src/system_of_complexes/completion.lean#L17

[Adam Topaz]

I have a mathlib PR open with additive functors. I'll merge this branch of LTE into master once that gets into mathlib.

[Riccardo Brasca]

Ah we want it as an additive functor!

[Adam Topaz]

Yeah, the completion is an additive functor. And you can pushforward a complex with respect to an additive functor.

[Patrick Massot]

Indeed we already know how to complete a normed group, but it's nicer if we can say directly the completion of a complex is a complex.

[Mario Carneiro]

By the way, I would be interested to try to restructure one of the proofs in this area to see if I can spot some tricks to make working with complexes easier. It will be easiest for this if the theorem is already formalized, so that it's really a refactoring job and I don't have to learn too much of the prerequisites. Let me know if you have a good theorem or collection of theorems to try this on.

[Johan Commelin]

Sebastien Gouezel said:

Sebastien Gouezel said:

I didn't follow the discussion on complexes closely, but I was pretty convinced by a suggestion by Johan, if I remember correctly. Which was: define a group morphism d' i j for all i j, which is equal to 0 if j is not i + 1, and to the usual d followed by a cast if j = i+1. Possibly with variations in which the i could be implicit when you apply it to x : C i. Did it turn out to be not so practical?

There's something I like with this proposition: in degree i, you can define the closed guys as (d' i (i+1)).ker, and the exact guys as (d' (i-1) i).range, and then the cohomology as their quotient, without having ever to check that (i-1) + 1 = i. And in fact it also works in degree i = 0, where this equality fails because of nat subtraction (but still (d' (0-1) 0).range is the zero submodule, so everything is fine). This means that for $\N$-indexed complexes you don't need to define things in a specific way at i = 0.

I like these observations.

[Johan Commelin]

@Mario Carneiro thanks! I'm sure we have several complete proofs scattered around on some branches. We can put those together in one file for you to play with.

[Adam Topaz]

Another small mathlib PR with the pushforward of a complex w.r.t. an additive functor. This should get rid of the additive_functor.lean file in the additive branch of lean-liquid. #6403