## Stream: condensed mathematics

### Topic: bounded exactness

#### 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 > 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 (Jan 30 2021 at 09:29):

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

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

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

#### Johan Commelin (Jan 30 2021 at 10:29):

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

#### Patrick Massot (Jan 30 2021 at 10:43):

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

#### Patrick Massot (Jan 30 2021 at 10:44):

Or maybe k isn't a natural number.

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

#### Peter Scholze (Jan 30 2021 at 13:38):

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 (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 $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 (Feb 01 2021 at 09:59):

@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 (Feb 01 2021 at 10:00):

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

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

#### Peter Scholze (Feb 05 2021 at 11:19):

I think that's still relevant!

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

#### Riccardo Brasca (Feb 05 2021 at 21:02):

I am looking at it

#### 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 $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 (Feb 05 2021 at 21:05):

Is "closed element" standard terminology?

#### Patrick Massot (Feb 05 2021 at 21:06):

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

#### Patrick Massot (Feb 05 2021 at 21:06):

Closed differential form is certainly a standard terminology.

Ah, sure

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

Looks good to me

#### Kevin Buzzard (Feb 05 2021 at 21:16):

Would "cocycle" and "coboundary" be better?

Probably

#### Patrick Massot (Feb 05 2021 at 21:20):

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

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

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

#### Patrick Massot (Feb 06 2021 at 17:02):

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

#### Patrick Massot (Feb 06 2021 at 17:06):

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

#### Patrick Massot (Feb 06 2021 at 17:10):

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

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

#### Johan Commelin (Feb 06 2021 at 17:34):

@Patrick Massot thanks a lot for this refactor!

#### Johan Commelin (Feb 06 2021 at 17:35):

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

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

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

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

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

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

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

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

#### Kevin Buzzard (Feb 08 2021 at 15:09):

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

#### Johan Commelin (Feb 08 2021 at 15:12):

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

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

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

#### Adam Topaz (Feb 08 2021 at 15:15):

Then just restate things in terms of D.

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

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

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

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

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

#### Johan Commelin (Feb 08 2021 at 16:03):

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

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


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

#### Patrick Massot (Feb 08 2021 at 16:55):

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

Ah okay.

#### Patrick Massot (Feb 08 2021 at 16:55):

We need a more powerful proof search.

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

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

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


#### Adam Topaz (Feb 08 2021 at 16:59):

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

#### Patrick Massot (Feb 08 2021 at 17:00):

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

Oh :)

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


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

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

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

#### Peter Scholze (Feb 08 2021 at 20:01):

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

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

#### Adam Topaz (Feb 08 2021 at 20:12):

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

#### Adam Topaz (Feb 08 2021 at 20:12):

(It's true for nat)

#### Mario Carneiro (Feb 08 2021 at 20:13):

I think the associativity part might cause a problem over int

#### Peter Scholze (Feb 08 2021 at 20:13):

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

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


#### Mario Carneiro (Feb 08 2021 at 20:14):

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

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

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

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

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

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

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

#### Johan Commelin (Feb 08 2021 at 20:19):

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 (Feb 08 2021 at 20:19):

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

Aha, I see!

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

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

#### Peter Scholze (Feb 08 2021 at 20:20):

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

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

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

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

#### Johan Commelin (Feb 08 2021 at 20:22):

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

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

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

#### Mario Carneiro (Feb 08 2021 at 20:22):

aka "$\Sigma$ = :rainbow: "

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

#### 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∥


#### Mario Carneiro (Feb 08 2021 at 20:24):

what are the types of res, d and congr

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

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

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

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

#### Adam Topaz (Feb 23 2021 at 18:41):

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

#### Adam Topaz (Feb 23 2021 at 18:42):

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

#### Johan Commelin (Feb 23 2021 at 18:51):

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

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

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

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

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

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

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

Ah we want it as an additive functor!

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

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

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

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

I like these observations.

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

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