Zulip Chat Archive

Stream: condensed mathematics

Topic: bounded exactness


view this post on Zulip Johan Commelin (Jan 30 2021 at 06:41):

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>0k > 0 and cc0c \ge c'_0. After that, the text refers to xCkcix \in C_{kc}^i. Do we want kcc0kc \ge c'_0?

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

view this post on Zulip Riccardo Brasca (Jan 30 2021 at 09:29):

We need restriction from kckc to cc, don't we? So I have the impression that k1k \geq 1 is necessary

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

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

view this post on Zulip Johan Commelin (Jan 30 2021 at 10:29):

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

view this post on Zulip Patrick Massot (Jan 30 2021 at 10:43):

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

view this post on Zulip Patrick Massot (Jan 30 2021 at 10:44):

Or maybe k isn't a natural number.

view this post on Zulip Patrick Massot (Jan 30 2021 at 10:45):

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

view this post on Zulip Peter Scholze (Jan 30 2021 at 13:38):

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

view this post on Zulip Patrick Massot (Feb 01 2021 at 08:16):

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 kk in the definition of weak exactness. Currently kk 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 kk then probably we should track both uses of kk independently.

view this post on Zulip Peter Scholze (Feb 01 2021 at 09:59):

@Patrick Massot You are absolutely right, kk 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.

view this post on Zulip Peter Scholze (Feb 01 2021 at 10:00):

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

view this post on Zulip Patrick Massot (Feb 05 2021 at 11:14):

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?

view this post on Zulip Peter Scholze (Feb 05 2021 at 11:19):

I think that's still relevant!

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:00):

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?

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 21:02):

I am looking at it

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:03):

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

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

Is "closed element" standard terminology?

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:06):

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

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:06):

Closed differential form is certainly a standard terminology.

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 21:07):

Ah, sure

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:07):

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

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

Looks good to me

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 21:16):

Would "cocycle" and "coboundary" be better?

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:16):

Probably

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:20):

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

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:22):

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

view this post on Zulip Riccardo Brasca (Feb 05 2021 at 21:22):

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

view this post on Zulip Patrick Massot (Feb 06 2021 at 17:02):

I pushed the Zeeman effect refactor. It splits the role of kk 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).

view this post on Zulip Patrick Massot (Feb 06 2021 at 17:04):

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₀

view this post on Zulip Patrick Massot (Feb 06 2021 at 17:05):

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.

view this post on Zulip Patrick Massot (Feb 06 2021 at 17:06):

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

view this post on Zulip Patrick Massot (Feb 06 2021 at 17:10):

Technical note: the coercion that allows to write x : C c i for xCcix \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.

view this post on Zulip Patrick Massot (Feb 06 2021 at 17:11):

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

view this post on Zulip Patrick Massot (Feb 06 2021 at 17:14):

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

view this post on Zulip Johan Commelin (Feb 06 2021 at 17:34):

@Patrick Massot thanks a lot for this refactor!

view this post on Zulip Johan Commelin (Feb 06 2021 at 17:35):

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

view this post on Zulip Riccardo Brasca (Feb 08 2021 at 14:52):

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.

view this post on Zulip Johan Commelin (Feb 08 2021 at 14:59):

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.

view this post on Zulip Bhavik Mehta (Feb 08 2021 at 15:02):

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

view this post on Zulip Riccardo Brasca (Feb 08 2021 at 15:05):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 15:08):

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.

view this post on Zulip Johan Commelin (Feb 08 2021 at 15:08):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 15:08):

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

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 15:09):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 15:12):

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

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 15:13):

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.

view this post on Zulip Adam Topaz (Feb 08 2021 at 15:15):

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.

view this post on Zulip Adam Topaz (Feb 08 2021 at 15:15):

Then just restate things in terms of D.

view this post on Zulip Johan Commelin (Feb 08 2021 at 15:16):

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

view this post on Zulip Riccardo Brasca (Feb 08 2021 at 15:39):

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.

view this post on Zulip Johan Commelin (Feb 08 2021 at 15:41):

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

view this post on Zulip Riccardo Brasca (Feb 08 2021 at 15:41):

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

view this post on Zulip Sebastien Gouezel (Feb 08 2021 at 16:02):

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?

view this post on Zulip Johan Commelin (Feb 08 2021 at 16:03):

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

view this post on Zulip Patrick Massot (Feb 08 2021 at 16:22):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 16:49):

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

view this post on Zulip Patrick Massot (Feb 08 2021 at 16:55):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 16:55):

Ah okay.

view this post on Zulip Patrick Massot (Feb 08 2021 at 16:55):

We need a more powerful proof search.

view this post on Zulip Patrick Massot (Feb 08 2021 at 16:56):

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?

view this post on Zulip Patrick Massot (Feb 08 2021 at 16:57):

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.

view this post on Zulip Adam Topaz (Feb 08 2021 at 16:57):

So adding an instance like the following is not enough?

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 16:59):

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

view this post on Zulip Patrick Massot (Feb 08 2021 at 17:00):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 17:01):

Oh :)

view this post on Zulip Adam Topaz (Feb 08 2021 at 17:36):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 17:37):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 17:37):

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

view this post on Zulip Patrick Massot (Feb 08 2021 at 17:39):

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.

view this post on Zulip Peter Scholze (Feb 08 2021 at 20:01):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 20:12):

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.

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:12):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 20:12):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 20:12):

(It's true for nat)

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:13):

I think the associativity part might cause a problem over int

view this post on Zulip Peter Scholze (Feb 08 2021 at 20:13):

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

view this post on Zulip Adam Topaz (Feb 08 2021 at 20:13):

Right:

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:14):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:14):

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

view this post on Zulip Peter Scholze (Feb 08 2021 at 20:16):

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?

view this post on Zulip Adam Topaz (Feb 08 2021 at 20:17):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:17):

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

view this post on Zulip Peter Scholze (Feb 08 2021 at 20:18):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:18):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:19):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:19):

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

view this post on Zulip Peter Scholze (Feb 08 2021 at 20:19):

Aha, I see!

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:19):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:20):

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

view this post on Zulip Peter Scholze (Feb 08 2021 at 20:20):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:21):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:21):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:21):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:22):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:22):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:22):

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.

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:22):

aka "Σ\Sigma = :rainbow: "

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:23):

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

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

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:24):

what are the types of res, d and congr

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

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:26):

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.

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:27):

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.

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:27):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:28):

you mean in hy?

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:28):

yeah

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:29):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:29):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:29):

don't use rfl

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:29):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:30):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:30):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:31):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:31):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:31):

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,

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:32):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:32):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:32):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:33):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:33):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:34):

at y?

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:34):

at everything

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:35):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:35):

yes, so I think we need that cleanup tactic.

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:36):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:37):

It is my lunch break :grinning_face_with_smiling_eyes:

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:37):

I pushed these experiments to wip_dtt_d_magic of the LTE repo

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:37):

Mario Carneiro said:

It is my lunch break :grinning_face_with_smiling_eyes:

I know, hence my question :laughing:

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:37):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:38):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:38):

no, this is int

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:38):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:38):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:39):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:39):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:39):

As long as they are all in some normal form

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:39):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:40):

sure, if that is easier (-;

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:40):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:40):

then you call the cleanup tactic on the result

view this post on Zulip Patrick Massot (Feb 08 2021 at 20:40):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:41):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:41):

yes

view this post on Zulip Patrick Massot (Feb 08 2021 at 20:41):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:41):

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

view this post on Zulip Heather Macbeth (Feb 08 2021 at 20:41):

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.

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:41):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:41):

because rw "doesn't work under binders"

view this post on Zulip Patrick Massot (Feb 08 2021 at 20:43):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 20:43):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:49):

@Mario Carneiro you are a genius!

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:49):

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

view this post on Zulip Johan Commelin (Feb 08 2021 at 20:49):

Works like a charm :tada: :octopus:

view this post on Zulip Peter Scholze (Feb 08 2021 at 20:55):

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

view this post on Zulip Patrick Massot (Feb 08 2021 at 21:03):

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.

view this post on Zulip Patrick Massot (Feb 08 2021 at 21:04):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 21:05):

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

view this post on Zulip Johan Commelin (Feb 11 2021 at 06:05):

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.

view this post on Zulip Johan Commelin (Feb 11 2021 at 16:00):

Done

view this post on Zulip Patrick Massot (Feb 23 2021 at 18:00):

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

view this post on Zulip Patrick Massot (Feb 23 2021 at 18:02):

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.

view this post on Zulip Patrick Massot (Feb 23 2021 at 18:04):

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

view this post on Zulip Patrick Massot (Feb 23 2021 at 18:08):

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 KK by if K > 0 then K else 1. And the formal statement that I wrote a couple of weeks ago missed the completeness assumption...

view this post on Zulip Patrick Massot (Feb 23 2021 at 18:10):

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

view this post on Zulip Patrick Massot (Feb 23 2021 at 18:14):

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.

view this post on Zulip Sebastien Gouezel (Feb 23 2021 at 18:30):

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?

view this post on Zulip Adam Topaz (Feb 23 2021 at 18:41):

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

view this post on Zulip Adam Topaz (Feb 23 2021 at 18:42):

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

view this post on Zulip Adam Topaz (Feb 23 2021 at 18:48):

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.

view this post on Zulip Johan Commelin (Feb 23 2021 at 18:51):

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

view this post on Zulip Johan Commelin (Feb 23 2021 at 18:52):

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

view this post on Zulip Peter Scholze (Feb 23 2021 at 19:35):

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

view this post on Zulip Sebastien Gouezel (Feb 23 2021 at 20:14):

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\N-indexed complexes you don't need to define things in a specific way at i = 0.

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

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

view this post on Zulip Adam Topaz (Feb 23 2021 at 20:24):

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

view this post on Zulip Adam Topaz (Feb 23 2021 at 20:24):

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

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

Ah we want it as an additive functor!

view this post on Zulip Adam Topaz (Feb 23 2021 at 20:27):

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

view this post on Zulip Patrick Massot (Feb 23 2021 at 20:47):

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.

view this post on Zulip Mario Carneiro (Feb 23 2021 at 21:24):

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.

view this post on Zulip Johan Commelin (Feb 23 2021 at 21:27):

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\N-indexed complexes you don't need to define things in a specific way at i = 0.

I like these observations.

view this post on Zulip Johan Commelin (Feb 23 2021 at 21:28):

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

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

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


Last updated: May 09 2021 at 16:20 UTC