Stream: condensed mathematics

Topic: spectral 9.6

Johan Commelin (Jan 25 2021 at 21:17):

I think we're almost ready to state 9.6.

• We should finish the definition of system_of_double_complexes.{row,col}.
• Define a new structure that records the 3 assumptions.
• Write a statement.

Johan Commelin (Jan 25 2021 at 21:17):

@Riccardo Brasca do you think it's worth it to also prove a weak version here? Or should we just go for complete directly?

Riccardo Brasca (Jan 25 2021 at 21:26):

I don't know, but I have the impression that the the proofs are essentially the same, especially once we have written down what happens taking completions

Riccardo Brasca (Jan 25 2021 at 21:30):

We should check all the details very carefully, but if, as I suspect, it is not that difficult to prove that for a complete M we have that weak_blah_blah implies blah_blah for a slightly different constant, then in the statement we can assume the strong property and prove the weak one

Riccardo Brasca (Jan 25 2021 at 21:31):

But in any case modifying one version into the other seems easy

Riccardo Brasca (Jan 25 2021 at 21:34):

In the main theorem everything is complete, right?

yup

Riccardo Brasca (Jan 25 2021 at 21:43):

The only place where this $\ldots + \varepsilon$ appears and we cannot ignore it taking completions is in the quotient norm (even for complete spaces is there). In that case to pass from the weak version to the strong one we need to change k, this is what happens for the snake lemma. If there are no quotient involved and everything is complete (maybe even without this assumption) we can go directly with the strong version I think

Riccardo Brasca (Jan 25 2021 at 21:44):

I just suggest for everybody starting formalizing the proof to carefully check on paper that there are no surprises. If that is the case the person working on the proof can change the statement, this should be essentially zero work

Riccardo Brasca (Jan 25 2021 at 21:45):

If I understand correctly it doesn't matter too much if in the main result we have k-exact or k^37+1-exact

Johan Commelin (Jan 25 2021 at 21:48):

Right, it doesn't really matter. Apart from trying to optimize the constants (-;

Johan Commelin (Feb 05 2021 at 09:51):

Is anyone working towards this?

Johan Commelin (Feb 05 2021 at 09:52):

I think we have all the ingredients

Peter Scholze (Feb 05 2021 at 10:23):

I'd be interested in this! Make sure to put all the quantifiers in the right order :-)

Johan Commelin (Feb 05 2021 at 18:14):

I've made the file system_of_double_complexes sorry-free. But there are still some useful simp-lemmas missing about how objects of C.col and C.row are just objects of the system of double complexes C.
Anyway, we should now have everything in place for a sorry-free statement of 9.6.

Floris van Doorn (Feb 05 2021 at 21:26):

I redefined C.col and C.row in a less ad-hoc way, and gave the simp lemmas.

Floris van Doorn (Feb 05 2021 at 21:39):

In Proposition 9.6, the normed abelian groups are indexed by c ≥ c₀. In our single/double complexes we index it by c ≥ 0. Do we just have the convention in the formalization that c₀ = 0?

Riccardo Brasca (Feb 05 2021 at 21:45):

I think that the idea is that you can always set everything equal to 0 if c < c₀ (the same is true if i < 0)

Riccardo Brasca (Feb 05 2021 at 21:46):

If for example you look at the definition of is_bdd_exact_for_bdd_degree_above_idx there is ∀ c ≥ c₀, so the terms for smaller c are irrelevant for this property

Floris van Doorn (Feb 05 2021 at 21:49):

Ah, I see. Thanks.

Floris van Doorn (Feb 05 2021 at 22:58):

Here is a stab at the statement of Proposition 9.6:

/-- Proposition 9.6 in [Analytic] -/
theorem analytic_9_6 (m : ℕ) (k : ℝ≥0) [fact (1 ≤ k)] :
∃ (ε : ℝ) (hε : ε > 0) (k₀ : ℝ≥0) [fact (1 ≤ k₀)],
∀ (M : system_of_double_complexes) (k' ≥ k₀) (c₀ : ℝ≥0) (H : ℝ≥0) (hH : 0 < H)
(cond1 : ∀ j ≤ m, (M.col j).is_bdd_exact_for_bdd_degree_above_idx k (m+1) c₀)
(cond2 : ∀ i ≤ m + 1, (M.row i).is_bdd_exact_for_bdd_degree_above_idx k m c₀)
(h : ∀ q [fact (q ≤ m)] (c) [fact (c₀ ≤ c)], M.X (k' * c) 0 (q+1) ⟶ M.X c 1 q)
(cond3a :
(∀ q [fact (q ≤ m)] (c) [fact (c₀ ≤ c)] (x : M.X (k' * c) 0 (q+1)), ​∥ h q c x ∥ ≤ H * ∥ x ∥))
(cond3b :
(∀ q [fact (q + 1 ≤ m)] (c) [fact (c₀ ≤ c)] (x : M.X (k' * (k' * c)) 0 (q+1)) (u1 u2 : units ℤ)
[fact (c ≤ k' * (k' * c))] [fact (k' * c ≤ k' * (k' * c))] [fact (c₀ ≤ k' * c)] [fact (q ≤ m)], -- these facts follow from previous ones
​∥ M.res (M.d x) + (u1 : ℤ) • h (q+1) (k' * c) (M.d' x) + (u2 : ℤ) • M.d' (h q (k' * c) x)∥ ≤
ε * ∥ (res M x : M.X c 0 (q+1)) ∥))
[fact (1 ≤ max (k' * k') (2 * k₀ * H))], -- (follows)
​(M.row 0).is_bdd_exact_for_bdd_degree_above_idx (max (k' * k') (2 * k₀ * H)) (m+1) c₀ :=
sorry


This is assuming that all of the following are correct:

• k, k₀ ≥ 1
• The c₀ is quantified at the same time as M.
• the first displayed equation in (3) holds for (it says) $x \in M_c^{0,q+1}$. This has a typo: the $c$ should be $k'c$.
• (9.2) holds (only) for q ≥ 1.
• (9.2) is 4 inequalities, for each ± a choice of either + or -.
• The "first row" in the conclusion is row 0.

Peter Scholze (Feb 05 2021 at 23:39):

Thanks! Let me confirm each point:
Floris van Doorn said:

This is assuming that all of the following are correct:

• k, k₀ ≥ 1
• The c₀ is quantified at the same time as M.
• the first displayed equation in (3) holds for (it says) $x \in M_c^{0,q+1}$. This has a typo: the $c$ should be $k'c$.
• (9.2) holds (only) for q ≥ 1.
• (9.2) is 4 inequalities, for each ± a choice of either + or -.
• The "first row" in the conclusion is row 0.
• Yes
• Yes
• Yes, that's a typo. Please a commit request in the GitHub! (https://github.com/PeterScholze/Analytic)
• No, it should hold also for $q=0$, in which case $h^{q-1}=0$.
• The statement holds for any choice of signs, and I wasn't sure which one is the one needed later (as homotopies sometimes acquire signs?)
• Yes, it's row 0.

Johan Commelin (Feb 06 2021 at 03:44):

@Floris van Doorn Note that since we index the complexes by $\Z$, but in all applications $X = 0$ if $i < 0$. So the condition $h^{-1} = 0$ is automatic in those cases.

Johan Commelin (Feb 06 2021 at 03:51):

Thanks for refactoring row and col.

Johan Commelin (Feb 06 2021 at 04:02):

What do you think of recording all the conditions in a structure spectral_conditions?

Johan Commelin (Feb 06 2021 at 04:43):

@Floris van Doorn I generalised some of the facts, so now a bunch of -- follows could be removed.

Johan Commelin (Feb 06 2021 at 04:46):

About the signs and u1 u2 : units \Z, I guess that in practice it might be more convenient to just record 4 conditions...
This is one benefit of putting all the conditions in a structure, because we can then have a constructor using units (if that is easier for verifying the condition), but we can project 4 conditions out of it, which might be easier to use when we apply the conditions in the proof.

Johan Commelin (Feb 06 2021 at 05:10):

Ok, I made that change. The names are not very pleasant: cond3bpp, cond3bpm, etc...

Johan Commelin (Feb 06 2021 at 05:14):

But before we launch into the proof, I guess we need to do two things:

1. State this in terms of weak exactness. (We might want to keep the version for strong exactness, but it needs to assume all objects are complete)
2. Refactor the exactness conditions to split k into two constants, because it is used in two ways. This will probably simplify calculations in the proofs (also for the proof of normed snake). Patrick was planning on doing this refactor.

Floris van Doorn (Feb 06 2021 at 07:00):

Thanks for the improvements @Johan Commelin.

Indexing complexes by all of $\mathbb{Z}$ makes sense. I just fixed so $h$ is also defined for $q<0$. I expect we will also need to add assumptions to various theorems stating that $M^{p,q}=0$ if $p<0$ or $q<0$, but that should be fine.

About u1 u2 : units \Z, I wasn't sure if that was the most convenient way to do it. Maybe 4 conditions is easier. However, when we apply the Proposition and have to check the 4 cases, maybe we can prove them all at the same time with this formulation.

Johan Commelin (Feb 06 2021 at 07:19):

Right... so now you get both. You only need to check cond3b, but you can use cond3bpm (and 3 other variants)

Johan Commelin (Feb 15 2021 at 10:21):

@Riccardo Brasca did you already work on the quotient of normed groups somewhere?

Johan Commelin (Feb 15 2021 at 10:21):

Because we'll need that for the proof of 9.6

Riccardo Brasca (Feb 15 2021 at 12:40):

In src/for_mathlib/normed_group_hom.lean there is the definition is_quotient and two basic results (the norm of the image in the quotient is smaller than the original norm and for all $\varepsilon$ there is ...). Do we need something more complicated?

Riccardo Brasca (Feb 15 2021 at 12:41):

We also have some basic result for system of complexes (like the quotient of admissible is admissible)

Johan Commelin (Feb 15 2021 at 12:44):

We will need the construction of a quotient, for the proof of 9.6

Riccardo Brasca (Feb 15 2021 at 13:26):

I see. There is no construction at the moment, but I can start working on it right now. We want something like def quotient (f : normed_group_hom M N) : normed_group that gives the quotient of N by the image of f, right? Plus the basic API of course

Maybe...

Johan Commelin (Feb 15 2021 at 13:32):

@Riccardo Brasca I can also imagine that something like

instance (s : add_subgroup M) : normed_group s.quotient := _


would be what we want

Johan Commelin (Feb 15 2021 at 13:32):

You already defined the range of a normed group hom, right?

Yes

Riccardo Brasca (Feb 15 2021 at 13:34):

BTW the only mathematical lemma to prove is that the "quotient norm" defined using the sup is actually a norm

Riccardo Brasca (Feb 15 2021 at 13:53):

Is the following the correct way of doing this? Given(s : add_subgroup M), I define on s.quotient an instance of has_norm, then I define def quotient.core(f : normed_group_hom M N) : normed_group.core (meaning that the norm has the requires properties) and finally I use normed_group.of_core to produce the required normed_group.

Johan Commelin (Feb 15 2021 at 13:55):

It's probably fine

Johan Commelin (Feb 15 2021 at 13:56):

But if s.quotient already gets a quotient metric (or topology) then this gives diamonds

Johan Commelin (Feb 15 2021 at 13:56):

So then you would have to prove that all those quotient structures are compatible in the proof fields of normed_group

Sebastien Gouezel (Feb 15 2021 at 13:59):

Just chiming in with my analyst's hat on, but if you quotient by a subgroup which is not closed, then the norm on the quotient is not a norm because there are nonzero vectors with zero norm. Adding an assumption [complete_space s] should save the day.

Johan Commelin (Feb 15 2021 at 14:00):

Yes, thanks for reminding me of that

Riccardo Brasca (Feb 15 2021 at 14:00):

@Sebastien Gouezel yes, of course!

Riccardo Brasca (Feb 15 2021 at 14:03):

There are no quotients of metric spaces in mathlib, and indeed instance test (s : add_subgroup M) : metric_space (quotient s) := by apply_instance doesn't work. But quotient s has an instance of topological_space. I don't know if this is a problem

Johan Commelin (Feb 15 2021 at 14:04):

We will probably be fine... but it won't be the mathlib way of doing things.

Johan Commelin (Feb 15 2021 at 14:04):

We only need the construction in a special place, where we really use it as normed_group. So it will find the right instance path, I guess.

Sebastien Gouezel (Feb 15 2021 at 14:25):

It would be really more mathliby to do things properly, i.e., check that you also get the quotient topology. @Patrick Massot , do we already have the quotient uniform structure on the quotient by a subgroup? (I am afraid of diamonds here between the uniform structure coming from the topological group structure on a quotient group, and the quotient uniform structure coming from the uniform structure on the original group, so to do this the right way it should be done by someone knowing very well this part of the library).

Johan Commelin (Feb 15 2021 at 14:27):

That diamond is one that causes many headaches. I think Patrick has mentioned several times during perfectoid project that we should refactor that part of the library... but it seems like a painful one

Riccardo Brasca (Feb 15 2021 at 20:33):

I just pushed the beginning of the construction of the quotient, in particular there is

instance quotient_normed_group (s : add_subgroup M) [complete_space M] [complete_space s] :
normed_group (quotient s)


Riccardo Brasca (Feb 15 2021 at 20:35):

There is one sorry, the fact that ∥x∥ = 0 → 0, that is not completely trivial I think (but not that difficult, it is the only statement that is not mathematically clear)

Riccardo Brasca (Feb 15 2021 at 20:37):

Ah, we will of course need that the natural projection is a normed group hom!

Riccardo Brasca (Feb 15 2021 at 20:38):

I think I'll stop for today, but if someone is interested please go ahead. We can also probably refactor is_quotient a little bit using the new definition

Riccardo Brasca (Feb 16 2021 at 14:34):

I've added a little API to quotients of normed groups. We still have to prove that ∥x∥ = 0 → x = 0, but this should be easy using what is already proved. I have to get familiar with Cauchy sequences in Lean but I can do it, I think.
There is a little duplicate code, since we have essentially two notion of quotients: the first one is the normed group structure on quotient S for S : add_subgroup M and the second one is the structure is_quotient (f : normed_group_hom M N), that essentially says that N is isomorphic to the quotient by the completion of the image of f. I proved that the morphism M → (quotient S) satisfies is_quotient but not the other implication. Do we need it?

Johan Commelin (Feb 16 2021 at 14:43):

I think that the direction that you proved is the important one.

Johan Commelin (Feb 16 2021 at 14:44):

We should do everything in terms of is_quotient. But sometimes you need to construct the target of the morphism f for which you need is_quotient f. That is the role that quotient plays.

Riccardo Brasca (Feb 16 2021 at 14:47):

I agree. The unfortunate thing is that we need some results that were proved for is_quotient to prove that the quotient norm is actually a norm. In practice I them before being able to state that the natural morphism satisfies is_quotient and I had to prove them directly for the quotient norm. But this is just an aesthetic problem

Kevin Buzzard (Feb 16 2021 at 14:50):

I guess the way to deal with the |z|=0 question is to show that the elements of norm 0 are precisely the closure of the subgroup you're quotienting out by.

Riccardo Brasca (Feb 16 2021 at 14:56):

The math proof is easy: if $||x|| = 0$ with lifting $m \in M$, then for all $n > 0$ there is $s_n\in S$ such that $||m + s_n|| < 1/n$. The sequence $(s_n)$ is Cauchy and so it converges to $s \in S$ (since $S$ is supposed complete). We get $||m - s|| = 0$ so $m = s \in S$ and $x=0$.

Kevin Buzzard (Feb 16 2021 at 14:59):

Right -- I'm just saying that a more general statement is that |x-bar| = 0 iff x is in the closure of S.

Heather Macbeth (Feb 16 2021 at 16:30):

If you need it, I added the submodule structure on the closure of a subspace fairly recently (for similar arguments about orthogonal projection): docs#submodule.topological_closure

Heather Macbeth (Feb 16 2021 at 16:30):

Actually I guess you need (if anything) the corresponding result for subgroups.

Riccardo Brasca (Feb 16 2021 at 21:42):

The construction of the norm on quotient S is now sorry free. Note that the proof of norm_zero_eq_zero, that is the above statement, can surely be golfed a lot: it's the first time I write a proof concerning limits, so in practice I translated all the statements from "filters language" to "$\varepsilon$ language" and then I messed around with $\varepsilon/2$ and so on.

More interestingly, the assumption that S is completed is written as (S : add_subgroup M) [complete_space S]: another option is (S : add_subgroup M) [is_complete (S : set M)]. The first one seems more natural, but in the proof I wanted to use cauchy_seq_tendsto_of_is_complete, so (S : set M) appears in the proof. I can modify this quickly if the second option is better.

Johan Commelin (Feb 17 2021 at 06:14):

@Riccardo Brasca great work, thanks a lot!

Johan Commelin (Feb 17 2021 at 06:15):

This seems like a natural moment to start thinking about how for_mathlib/normed_group_hom.lean should move to mathlib. @Sebastien Gouezel @Heather Macbeth I would love to have feedback from you, because I'm far from an expert and just blundering my way into functional analysis. For example: should we rename this to bounded_hom or does this deserve the name normed_group_hom?

Kevin Buzzard (Feb 28 2021 at 16:48):

In system_of_complexes.double we have

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


Looks fine, right? And then almost immediately afterwards we have

@[simp] lemma res_comp_res (h₁ : fact (c₂ ≤ c₁)) (h₂ : fact (c₃ ≤ c₂)) :
@res C _ _ p q h₁ ≫ @res C _ _ p q h₂  = @res C _ _ p q (le_trans h₂ h₁) := ...

@[simp] lemma res_res (h₁ : fact (c₂ ≤ c₁)) (h₂ : fact (c₃ ≤ c₂)) (x : C.X c₁ p q) :
@res C _ _ p q h₂ (@res C _ _ p q h₁ x) = @res C _ _ p q (le_trans h₂ h₁) x := ...


with all this @ _ nonsense. Until about a week ago I regarded this as a fact of life. But Mario's comment here was as much news to me as it was to Bryan. @Mario Carneiro what is going on here? Should p and q be explicit in the definition of res? What is the rule?

Kevin Buzzard (Feb 28 2021 at 16:52):

Same question for

/-- C.d is the differential C.X c p q ⟶ C.X c (p+1) q for a system of double complexes C. -/
def d {c : ℝ≥0} {p q : ℤ} :
C.X c p q ⟶ C.X c (p+1) q :=
((C.obj $op c).d p).f q lemma d_comp_res (h : fact (c₂ ≤ c₁)) : @d C c₁ p q ≫ @res C _ _ _ _ h = @res C _ _ p q _ ≫ @d C c₂ p q := ...  Bhavik Mehta (Feb 28 2021 at 17:00): I think the situation in res compared to in that PR is different, right? There, the rule for lemmas is that f can be implicit because it's implied by the later explicit hypothesis for hf; but here there's no such later hypothesis. So I think the usual rule applies for res, that Lean can't figure out what p and q should be, so either make them implicit and use @ or make them explicit (and I'd instinctively do the latter) Kevin Buzzard (Feb 28 2021 at 17:05): The PR is talking about a def. The file in lean-liquid is littered with @s. Mario Carneiro (Feb 28 2021 at 17:06): @Kevin Buzzard The rule is different for partial functions specifically because the proof arguments are elided in printing, so it's hard to see what things like congr will do. In this example it depends on whether that hom is to be considered a function or not Mario Carneiro (Feb 28 2021 at 17:07): If it's usually left unapplied then I would keep the other arguments explicit Bhavik Mehta (Feb 28 2021 at 17:09): Kevin Buzzard said: The PR is talking about a def. The file in lean-liquid is littered with @s. Sure - but I'm saying that Mario's comment is about an argument which is implied by another; but in your case there is no later argument which implies what p or q are Mario Carneiro (Feb 28 2021 at 17:10): if it's a function, then the later argument would be C.X c' p q Mario Carneiro (Feb 28 2021 at 17:11): but as long as this is manipulated using categorical notation like ≫ then it's not really a function, it's just an object that looks kind of like a function (and in particular is not the subject of a coe_fn instance with another argument) Patrick Massot (Feb 28 2021 at 18:06): I asked the same question as soon as I saw this file, but indeed those res and d functions are always applied in the following files, so it makes sense to keep things like this, at least until we need other aspects. Kevin Buzzard (Mar 01 2021 at 13:47): Dumb question: In the docstring for system_of_double_complexes it says Implementation detail: cochain_complex assumes that the complex is indexed by ℤ, whereas we are interested in complexes indexed by ℕ. We therefore set all objects indexed by negative integers to 0, in our use case.  Where is the assumption in the statement of 9.6 that all objects indexed by negative integers are 0? I'm starting on a proof of 9.6 and I can't find it :-/ Johan Commelin (Mar 01 2021 at 13:55): hah, good point... breen_deligne.package.system returns a system for which all objects in negative degrees are 0. Johan Commelin (Mar 01 2021 at 13:55): But of course some of the theorems might need to assume this. Johan Commelin (Mar 01 2021 at 13:55): By the way, it might be easier to assume that d i = 0 for negative i Johan Commelin (Mar 01 2021 at 13:56): Because that's an equality of terms, instead of some isom in a category. Johan Commelin (Mar 01 2021 at 13:57): Note that for the proof of normed_snake we don't need any nonzeroness assumptions Riccardo Brasca (Mar 01 2021 at 13:57): In the paper all complexes are indexed by nonnegative integer, aren't they? 9.6 says "$M_c^{p,q}, p,q \geq 0$..." Kevin Buzzard (Mar 01 2021 at 13:57): but d i = 0 doesn't imply $M_{i,j}=0$ right? Are you saying that I have to modify the statement of 9.6 that we have? Johan Commelin (Mar 01 2021 at 13:58): yes, you might need to modify the conclusion (I didn't check) to say that you only prove something about nonneg indices Kevin Buzzard (Mar 01 2021 at 13:58): Yes Riccardo, the issue is that we have what we are claiming is a formalisation of the statement of 9.6 in the repo and it doesn't contain this assumption. I totally agree that it's true! Kevin Buzzard (Mar 01 2021 at 13:59): For some reason, our complexes are indexed over the integers (in fact I'm pleased they are because we have to deal with subtraction and you all know what I think about nat subtraction) Kevin Buzzard (Mar 01 2021 at 14:01): Johan, these is_bounded_exact hypotheses and conclusion are everywhere. I need to modify a lot more than the conclusion, right? It's not just the assertion that we're only proving something about non-negative indices (which would imply that the M_{i,j} could be non-trivial for i or j<0 but we don't prove anything about them). Are you saying that I should not be putting in the blanket assumption M_{i,j}=0 for i or j < 0 but should be doing something else? Johan Commelin (Mar 01 2021 at 14:04): Hmm, I thought that claiming we only prove something for p,q >= 0 would suffice Johan Commelin (Mar 01 2021 at 14:04): Why are you worried that this isn't enough? Sebastien Gouezel (Mar 01 2021 at 14:05): It's really easy for me to say nonsense, because I haven't tried to play the game. But is there really no way to have complexes indexed by $\N$? I can see many settings in math where the complex is genuinely indexed by $\N$ (de Rham cohomology, group cohomology, homotopy groups and so on), where having to extend all these definitions to negative indices will feel like totally weird. Johan Commelin (Mar 01 2021 at 14:05): ooh, you mean that is_bounded_exact doesn't make that assumption? Johan Commelin (Mar 01 2021 at 14:06): @Sebastien Gouezel I agree, and I think Scott has been experimenting with a new definition that generalises both concepts Johan Commelin (Mar 01 2021 at 14:06): The current PR on connective chain complexes just redefines nat-indexed complexes, but I'm not in favour of having two definitions if we can get away with one. Johan Commelin (Mar 01 2021 at 14:07): @Kevin Buzzard if assuming M_{i.j} = 0 works, then that's fine. But I'm worried that it isn't practical Johan Commelin (Mar 01 2021 at 14:07): Because of DTT issues Kevin Buzzard (Mar 01 2021 at 14:08): Johan Commelin said: ooh, you mean that is_bounded_exact doesn't make that assumption? Yes exactly: def is_bounded_exact (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∥  I could also change this. Kevin Buzzard (Mar 01 2021 at 14:09): OK so here is a mathematics question: is $i=-1$ OK in that definition? Kevin Buzzard (Mar 01 2021 at 14:12): From my reading of the proof of 9.6, $i=-1$ is OK because this is exactly what is being proved in the $m=0$ case. I will comment that like Sebastien all the complexes I see in the mathematics I've done have been nat-graded, and all the double complexes I've dealt with have been first quadrant ones, but I have certainly seen seminars where this was not the case. Riccardo Brasca (Mar 01 2021 at 14:17): Does 9.6 really requires $M_c^{p,q} = 0$ for negative indexes? For the snake lemma the exact same proof worked in general. Here we probably need to modify a little bit the hypothesis, something like "for $j \leq m$" instead of "for $j = 0,\ldots, m$..." etc, but I have the impression that, if we want to keep $\mathbb{Z}$-graded complexes, this is the most natural think to do Kevin Buzzard (Mar 01 2021 at 14:18): The answer to that question depends on your interpretation of what it means to be <=k exact in degrees <= m for c>=c0. There is an issue at 0. Kevin Buzzard (Mar 01 2021 at 14:21): Our i is Peter's i+1 but Peter allows i=0 so we need to allow i=-1. That's all. Kevin Buzzard (Mar 01 2021 at 14:22): We made some shift so we didn't have to do a subtraction, but this shift is pointless because it's integer subtraction. Kevin Buzzard (Mar 01 2021 at 14:23): Another issue is that we have changed <=k-exact to <=(k,K)-exact and have failed to correctly translate the statement of the theorem -- we have a spurious K about which we know nothing and our goal involves proving |a|<=K*|b| which is clearly impossible right now. Riccardo Brasca (Mar 01 2021 at 14:26): I didn't check, so maybe this is completely false, but I mean using the current definition of is_bounded_exact. My understanding is that Peter wrote "which is defined to be 0 when $i= 0$" just because, strictly speaking, $C^{i-1}_c$ doesn't make sense for him and that in the final application this will automatic for us since we will apply the general results to a particular case that have $0$ in negative degrees. But I don't know if all the proofs works in general Kevin Buzzard (Mar 01 2021 at 14:28): I need to think about this a little more, but right now our conclusion of 9.6 is  (M.row 0).is_bounded_exact (max (k' * k') (2 * k₀ * H)) K (m+1) c₀ :=  and I believe that the "max" is a consequence of the Scholze packing trick where one constant is used to do two jobs. Instead of (max A B) K it should be A B, and some but not all of the things called k' or k_0 should change to K's. Kevin Buzzard (Mar 01 2021 at 14:31): Riccardo you are right that the proofs might work in general. This hadn't occurred to me. Johan Commelin (Mar 01 2021 at 14:31): @Riccardo Brasca I think we need some assumptions here, contrary to normed_snake, because we want to do an induction, so we need a base case. Johan Commelin (Mar 01 2021 at 14:32): @Kevin Buzzard I don't think the indices are different between Analytic.pdf and the source code. We only shift a temporary index. Johan Commelin (Mar 01 2021 at 14:33): Like, the complexes have their objects in the same spot, but then we talk about C (i + 1) for i = 0,1,2, m-1 instead of C i for i = 1,...,m Riccardo Brasca (Mar 01 2021 at 14:33): @Johan Commelin sure, something should be changed here to start the induction. What I am saying is that, if this not too difficult, we can just find the correct assumption that makes the proof working and that is obviously satisfied if all the negative terms are $0$. Johan Commelin (Mar 01 2021 at 14:34): yes, that's also what I was hoping to do by assuming d i = 0 for negative i Johan Commelin (Mar 01 2021 at 14:34): But I don't know whether that's strong enough Kevin Buzzard (Mar 01 2021 at 14:35): Unfortunately I need to go to meetings now and I am not sure I'll have time to look at this again until after my next lecture on Thursday afternoon. But I'm happy to keep working on it then. Johan Commelin (Mar 01 2021 at 14:38): I guess we could change is_bounded_exact to ignore negative i Johan Commelin (Mar 01 2021 at 14:38): Or i < -1, if we need the -1 case Kevin Buzzard (Mar 01 2021 at 14:40): Because we have randomly changed i to i-1 (for no obvious reason as far as I can see, i is an integer) we need the -1 case. Adam Topaz (Mar 01 2021 at 14:41): One reason for why one might want Z-indexed complexes is because you might want to use the shift functors. Kevin Buzzard (Mar 01 2021 at 14:41): We could change it back and then ask for i : nat, we would still have (i : int) - 1 but we can just use 0. Johan Commelin (Mar 01 2021 at 14:42): Kevin Buzzard said: Because we have randomly changed i to i-1 (for no obvious reason as far as I can see, i is an integer) we need the -1 case. well, this is simply because of the well known DTT issues right? Until we fix the definition of d, the statement will not type check if you use i - 1. Kevin Buzzard (Mar 01 2021 at 14:42): On the balance of things I think int is better, or else you'll always be dealing with i=0 special cases. A long exact sequence of cohomology groups will start H^0(A)->H^0(B)... instead of 0=H^{-1}(C)->H^0(A)->... Patrick Massot (Mar 01 2021 at 14:47): Kevin Buzzard said: I need to think about this a little more, but right now our conclusion of 9.6 is  (M.row 0).is_bounded_exact (max (k' * k') (2 * k₀ * H)) K (m+1) c₀ :=  and I believe that the "max" is a consequence of the Scholze packing trick where one constant is used to do two jobs. Instead of (max A B) K it should be A B, and some but not all of the things called k' or k_0 should change to K's. Yes, this is clear. And we won't know the correct constants before carefully proving the theorem. Kevin Buzzard (Mar 01 2021 at 14:47): Well we won't be proving the theorem as it currently stands :-) Johan Commelin (Mar 01 2021 at 14:47): It would be nice if we could just start formalising it, and fix the conclusion along the way Kevin Buzzard (Mar 01 2021 at 14:48): Yes I agree! I just hadn't realised that this was the game we were playing :-) Johan Commelin (Mar 01 2021 at 14:48): Would it make sense to add assumptions that things are is_bounded_exact for certain negative m to the assumptions? Johan Commelin (Mar 01 2021 at 14:48): That might make the whole thing provable again Kevin Buzzard (Mar 01 2021 at 14:49): The issue right now is that the constants are all wrong Kevin Buzzard (Mar 01 2021 at 14:49): I mean literally wrong Kevin Buzzard (Mar 01 2021 at 14:50): Riccardo has pointed out that it might be the case that actually the proof works even if we don't assume the M_ij are zero for i,j<0 because the proof we have in the document for -1<=(our ) i might just work in general Kevin Buzzard (Mar 01 2021 at 14:51): The issue right now is that we have an input K which is not assumed to be k unlike in the paper, and an output K which is supposed to be a completely different number Kevin Buzzard (Mar 01 2021 at 14:51): I can fix this, I just need to write a two hour workshop first Johan Commelin (Mar 01 2021 at 14:52): Sure, provable modulo constants :rofl: Damiano Testa (Mar 01 2021 at 14:57): Just a comment, though I have only superficially followed the evolution of this branch. I have actually used (co-)homology in degree -1, in the context of simplicial complexes. In that case, especially reduced homology, is much easier to work with, but it does assign a generator to one of the "empty" simplicial complexes. This is actually important, since it allows induction arguments to start one step earlier than you would think reasonable and all proofs are much simpler. In general, even when complexes and (co-)homology have "positive" degrees, I always find it convenient to be able to "lean onto the boundary" of where the cohomology groups are interesting and begin inductions at a stage where they are zero (or almost zero), and then have fewer duplicate arguments. I hope that this makes some amount of sense! Johan Commelin (Mar 01 2021 at 15:09): I'm going to make m an integer in that file Johan Commelin (Mar 01 2021 at 15:22): Maybe we want the \eps to be an nnreal, and use nnnorm instead of norms, to stay in the nonnegative world. Adam Topaz (Mar 01 2021 at 16:17): Johan Commelin said: Sure, provable modulo constants :rofl: Can this be formalized with filters? Johan Commelin (Mar 02 2021 at 06:43): Johan Commelin said: I'm going to make m an integer in that file In the end I haven't done this yet. Johan Commelin (Mar 02 2021 at 06:49): My current feeling is that it should be sufficient to add the assumptions that the d-edges that enter the first quadrant are all 0 + the assumption that row 0 is bounded exact in degree $\le -1$. Johan Commelin (Mar 02 2021 at 07:04): I moved everything about 9.6 to normed_spectral.lean Johan Commelin (Mar 02 2021 at 12:14): I think we need to be very careful with how we phrase 9.6. Johan Commelin (Mar 02 2021 at 12:15): Because, when working with nat, $\forall i \le m - 1$ is an empty condition when $m = 0$, in ordinary maths. But in lean it isn't... Johan Commelin (Mar 02 2021 at 12:15): On the other hand, $\forall i < m$, would work... Johan Commelin (Mar 02 2021 at 12:15): These sort of annoyances will have to be sorted out (-; Johan Commelin (Mar 02 2021 at 19:53): Update: • m is now an integer • hence the off-by-one-shift could be undone, I did this • half of the case m = 0 is now proven Johan Commelin (Mar 03 2021 at 11:01): For the inductive step, we'll need to fold up systems of complexes. A helpful ingredient would be to know that NormedGroup has cokernels (and that they satisfy the is_quotient predicate that @Riccardo Brasca defined). Johan Commelin (Mar 03 2021 at 11:04): After that, we need a functor that takes a cochain complex (of objects in a category with zero morphisms and cokernels), and that sends C to the complex fold : C1 / C0 ---> C2 ---> C3 ---> ...  Johan Commelin (Mar 03 2021 at 11:05): As long as we do not have nat-indexed complexes, I suggest that we just discard all the objects indexed by negative indices Johan Commelin (Mar 03 2021 at 11:07): Once fold is defined, we should have system_of_complexes.fold, and prove that fold C is bounded exact in degrees \le m-1 iff C is bounded exact in degrees \le m (under suitable assumptions, such as d : C_{-1} -> C_0 = 0, and C is bounded exact in degrees \le -1) Johan Commelin (Mar 03 2021 at 11:08): Idem for weak exactness Johan Commelin (Mar 03 2021 at 11:09): Once that is done, we want system_of_double_complexes.fold which applies the fold above to all of its rows. With that construction under our belt, the inductive step in the proof of 9.6 should be easy. Julian Külshammer (Mar 03 2021 at 11:32): Probably a difference in terminology, but I would call the fold operation soft_truncation at 1. Johan Commelin (Mar 03 2021 at 11:44): @Julian Külshammer ok, that's a useful tip! Johan Commelin (Mar 03 2021 at 11:45): Does that include the shift? Or would soft_truncation place C1/C0 in degree 1? Julian Külshammer (Mar 03 2021 at 11:47): This does not include the shift, so there is a slight difference, right. Johan Commelin (Mar 03 2021 at 11:49): Well, I guess we could factor it into those two steps, that doesn't hurt. Johan Commelin (Mar 03 2021 at 11:49): After all, we already have the shift functor. Johan Commelin (Mar 03 2021 at 11:50): And presumably soft_truncation would take i as argument, and truncate at degree i, instead of only at 0. Johan Commelin (Mar 03 2021 at 11:51): On the other hand, for i = 0, it can very nicely be defined using the equation compiler. Julian Külshammer (Mar 03 2021 at 11:58): With this you don't seem to be far from defining the standard t-structure https://en.m.wikipedia.org/wiki/T-structure Johan Commelin (Mar 03 2021 at 12:12): Hah, that would actually be quite nice, if we could get to that definition. Johan Commelin (Mar 03 2021 at 12:38): Hmm, here we quotient by the image of C0, instead of the kernel of C1 -> C2 (which is what is usually done with the truncation functors). The two only agree if the complex is exact at C1. Julian Külshammer (Mar 03 2021 at 13:09): You are right, I also noticed in the meantime. Johan Commelin (Mar 03 2021 at 13:13): maybe we can still call this soft_truncation' Riccardo Brasca (Mar 03 2021 at 13:34): Johan Commelin said: For the inductive step, we'll need to fold up systems of complexes. A helpful ingredient would be to know that NormedGroup has cokernels (and that they satisfy the is_quotient predicate that Riccardo Brasca defined). Do you mean we need a universal property? The current situation is the following: we can take the quotient by a complete subspace, it automatically gets a normed_group instance and satisfies is_quotient. I think we have the completion of a subspace inside a complete group, so getting the quotient in general should be not too difficult. I don't what is the situation in the big group is not complete (I mean, I don't even know the mathematics). Johan Commelin (Mar 03 2021 at 13:35): @Riccardo Brasca hmm, good point... my sketch was a bit too naive Johan Commelin (Mar 03 2021 at 13:35): Because we aren't working in the category CompleteNormedGroup Johan Commelin (Mar 03 2021 at 13:35): And I don't think we should define it... sounds like we don't need the trouble Johan Commelin (Mar 03 2021 at 13:36): What we need is this soft_truncation' functor. And maybe we can just define it directly using your quotient stuff. We don't have to go through the cokernel api provided by category_theory/ Johan Commelin (Mar 03 2021 at 13:37): @Riccardo Brasca btw, I moved the quotient stuff to for_mathlib/normed_group_quotient.lean because the rest of normed_group_hom.lean is currently being PRd to mathlib Johan Commelin (Mar 03 2021 at 13:37): Did you define some sort of lift? Johan Commelin (Mar 03 2021 at 13:38): We'll need some sort of universal property to define soft_truncation' Riccardo Brasca (Mar 03 2021 at 13:39): I didn't define some lift but getting the linear map is immediate, since the quotient is the group quotient. For continuity... let me think one minute Johan Commelin (Mar 03 2021 at 13:40): you only need boundedness Riccardo Brasca (Mar 03 2021 at 13:45): OK, boundedness of the lift is trivial (I thought that boundedness and continuity were equivalent... for normed space they are...) Riccardo Brasca (Mar 03 2021 at 13:45): I don't have time this afternoon, but I can write it later today Johan Commelin (Mar 03 2021 at 13:50): boundedness implies continuity, but I have no idea whether the converse is true in this setting Riccardo Brasca (Mar 03 2021 at 14:06): Now I have the impression that a small modification the proof that the seminorm on $X/Y$ is actually a norm only requires $Y$ to be closed in $X$ (now the assumption is completeness), without assuming that $X$ is complete. The kernel of a continuous map is always closed, so maybe have cokernel without too much troubles Riccardo Brasca (Mar 03 2021 at 14:13): Even better, the proof of this more general fact seems easier than the current proof :sweat_smile: Johan Commelin (Mar 03 2021 at 14:30): Nice... that seems to be a general pattern (-; Johan Commelin (Mar 10 2021 at 20:26): @Peter Scholze I'm confused about the base case of the normed spectral sequence 9.6. Peter Scholze (Mar 10 2021 at 20:26): OK... Johan Commelin (Mar 10 2021 at 20:26): Part of the confusion might be because now k is split into two constants k and K, but I don't think that's everything. Johan Commelin (Mar 10 2021 at 20:26): I seem to be getting K * (H + 1/2) Johan Commelin (Mar 10 2021 at 20:27): Instead of 2 * K * H Peter Scholze (Mar 10 2021 at 20:27): oh, ok, that's not too bad then :-) Peter Scholze (Mar 10 2021 at 20:28): Hmm, is this in Lean or on paper? Johan Commelin (Mar 10 2021 at 20:28): it's not completely in Lean yet. Peter Scholze (Mar 10 2021 at 20:29): Because if it's on paper, I would think you do the wrong manipulation Peter Scholze (Mar 10 2021 at 20:29): You need to subtract the term $k\epsilon ||x_c||_{M_c^{0,0}}$ Peter Scholze (Mar 10 2021 at 20:30): I guess that's now $K\epsilon||x_c||_{M_c^{0,0}}$, but never mind Johan Commelin (Mar 10 2021 at 20:30): Ooh, I wasn't planning on doing that :oops: Johan Commelin (Mar 10 2021 at 20:30): I see... then I need to think about the correct manipulation again Johan Commelin (Mar 10 2021 at 20:33): I thought $\|d^{0,0}_{k'c}(x_{k'c})\| \le \|d^{0,0}_{k'c}(x_{k'c}) - h^0_{k^{'2}c}(d^{'0,0}_{k^{'2}c}(x))\| + \|h^0_{k^{'2}c}(d^{'0,0}_{k^{'2}c}(x))\|$ Johan Commelin (Mar 10 2021 at 20:33): Is that one of the manipulations that you had in mind? Peter Scholze (Mar 10 2021 at 20:33): That sounds too complicated Peter Scholze (Mar 10 2021 at 20:34): Do you agree with second displayed inequality on page 61? Johan Commelin (Mar 10 2021 at 20:34): I'm stuck on the second $\le$ in that display Johan Commelin (Mar 10 2021 at 20:35): Well, I managed to prove it using the beast I posted above Peter Scholze (Mar 10 2021 at 20:35): Ah, yes, sorry, I guess this uses what you've written Johan Commelin (Mar 10 2021 at 20:36): Ok, and then you need to pass from the final part of that 2nd display to the conclusion Johan Commelin (Mar 10 2021 at 20:36): And I thought this would just reuse the final display on p60 Peter Scholze (Mar 10 2021 at 20:36): Yes. But if you set $\epsilon=\tfrac 1{2k}$, then the first summand on the right is half of the term on the left Peter Scholze (Mar 10 2021 at 20:37): So you can subtract, leaving half of the left-hand side, so multiplying by $2$ gives what I claim Johan Commelin (Mar 10 2021 at 20:37): ooh, of course :face_palm: Johan Commelin (Mar 10 2021 at 20:37): gotcha, you're not just chaining them Peter Scholze (Mar 10 2021 at 20:37): Yeah, it's a confusing part! Usually you never do that thing Peter Scholze (Mar 10 2021 at 20:37): I should have maybe made that more explicit Peter Scholze (Mar 10 2021 at 20:38): This argument actually feels "wrong" to me, but I think it works Johan Commelin (Mar 10 2021 at 20:39): Ok, this also means that I canceled K too early Johan Commelin (Mar 10 2021 at 21:24): @Peter Scholze thanks for getting me unstuck there! The base case is now sorry-free in lean Kevin Buzzard (Mar 11 2021 at 07:08): In some sense that felt like most of the work -- the inductive step follows from something else, right? Johan Commelin (Mar 11 2021 at 12:47): If we define shift to swap signs, then it isn't clear to me why shift C is weak bounded exact if C is. Johan Commelin (Mar 11 2021 at 12:48): I end up with goals like (∃ (y : ↥(⇑(shift.obj C) c i')), ∥⇑res x - (⇑-C.d (i' + 1) (i + 1)) y∥ ≤ ↑K * ∥(⇑-C.d (i + 1) (i + 1 + 1)) x∥ + ε) ↔ ∃ (y : ↥(⇑C c (i' + 1))), ∥⇑res x - ⇑(C.d (i' + 1) (i + 1)) y∥ ≤ ↑K * ∥⇑(C.d (i + 1) (i + 1 + 1)) x∥ + ε  Johan Commelin (Mar 11 2021 at 12:49): This isn't very readable, but the problem is that on one side we have res x - - C.d _ _y and on the other side we have only one -. Peter Scholze (Mar 11 2021 at 12:57): I can't parse what's written, but how can there be a problem here? Maybe just change the sign of y again, or so? Johan Commelin (Mar 11 2021 at 13:01): Lol, I need to take a break I guess (-; :face_palm: Johan Commelin (Mar 11 2021 at 13:01): You are completely right Kevin Buzzard (Mar 14 2021 at 18:43): OK so I am working on 9.6. At some point in the proof we need to take the entire double complex $M^{p,q}$ and shift it all one to the left, giving us a new complex $N^{p,q}$ with the "0th column" $N^{p,0}$ defined as $M^{p,1}/M^{p,0}$ with its quotient norm. The claim (as I understand it) is that if $M$ satisfies all the conditions in the statement of 9.6 for $m$ then (with possibly different constants) $N$ satisfies all the conditions for $m-1$. The one I'm stuck on is condition (3), the case $q=0$ (using Scholze's notation), and I need to verify equation (9.2). Again sticking to notation in the paper and forgetting all c's and k's, I need to verify that for all $x$ in $N^{0,0}$, $|L(x)| \leq\epsilon|res(x)|$. Here $L$ is an abelian group hom (a sum of three homs actually, two of them with $\pm$ signs) from $N^{0,0} :=M^{0,1}/M^{0,0}$ to $N^{1,0} := M^{1,1}/M^{1,0}$ induced by some $L' : M^{0,1}\to M^{1,1}$, and the fact that $M$ satisfies the conditions of 9.6 tells us that $|L'(\tilde{x})| \leq\epsilon|res(\tilde{x})|$ for all $\tilde{x}$ in $M^{0,1}$. But because the quotient map is not an isometry I don't see how to now conclude that (9.2) is true for $N$ in the $q=0$ case. Kevin Buzzard (Mar 14 2021 at 19:13): Aah! As well as $L'$ I also have $L'' : M^{0,0}\to M^{1,0}$ with $|L''(y)|\leq\epsilon|res(y)|$ for all $y\in M^{0,0}$. Am I supposed to be using this somehow? This is condition (3) when $q=0$ for $M$; the $L'$ in the previous post was coming from $q=1$ for $M$. Peter Scholze (Mar 14 2021 at 21:31): This sounds exactly like the annoyance we already had in 9.10... if the issue persists, I'll think about it tomorrow Kevin Buzzard (Mar 14 2021 at 23:59): I can't use $L''$ because I don't know any relation between $h^0_{k'c}$ and $h^1_{k'c}$ (for $M$). I had assumed that to define $h^0$ for $N$ I just used $h^1_{k'c}$ for $M$. But now I realise that in fact maybe $L'$ doesn't even reduce to $L$ the way I thought things worked because in the $N$ world there is no $d'^{1,q-1}_{k'c}$ term when $d=0$ but in the $M$ world you have $q=1$ so there's an extra term -- oh but it's in the image of $M^{1,0}$ so makes no difference. To summarise, my worry is if $x\in M^{0,1}$ is close to the image of $M^{0,0}$, because then in the $N$ world the norm of $x$ on the right hand side might suddenly drop after you take the quotient, breaking the inquality. If we could say something like "x in M^{0,1} close to M^{0,0} implies L(x) in M^{1,1} close to something in M^{1,0}" we might be OK, but I don't seem to have any control over the $h^1:M^{0,2}\to M^{1,1}$ term. Johan Commelin (Mar 15 2021 at 06:08): I agree that the issue seems similar to what we saw in 9.10. In this case, I don't see that the issue goes away by assuming that everything is complete. Johan Commelin (Mar 15 2021 at 06:09): But it might certainly be the case that we are just chaining some inequalities in the wrong order again. Peter Scholze (Mar 15 2021 at 09:20): @Kevin Buzzard Ah, I think you caught something here; I think it's even a bit more subtle than in 9.10. I'm quite sure that the constants will change more than I claimed so far. Let me try to analyze what's happening, and get back to you Peter Scholze (Mar 15 2021 at 10:01): OK, I'm getting myself seriously confused here. It may take a moment. Peter Scholze (Mar 15 2021 at 10:14): Ah, I think I see! One has to phrase (9.2) better. Namely, what's inside the absolute value on the left-hand side defines a map of complexes $M_{k'^2c}^{0,\bullet}\to M_{k'c}^{1,\bullet}$. One has to ask that this map factors as a composite of the restriction $M_{k'^2c}^{0,\bullet}\to M_c^{0,\bullet}$ and a map of complexes $M_c^{0,\bullet}\to M_{k'c}^{1,\bullet}$ that is (in each degree) of norm $\leq\epsilon$. Peter Scholze (Mar 15 2021 at 10:14): (Actually, maybe it's not necessary that this is a map of complexes?) Peter Scholze (Mar 15 2021 at 10:14): In any case, this stronger condition is verified when 9.6 is applied in the proof of 9.5. Peter Scholze (Mar 15 2021 at 10:15): I'll try to rewrite the file to incorporate the change (and in the process check more carefully whether this ought to work) Peter Scholze (Mar 15 2021 at 10:16): OK, it should be map of complexes, but anyway it is. Johan Commelin (Mar 15 2021 at 10:17): Great! Let's see if this fixes it Peter Scholze (Mar 15 2021 at 10:18): Well, let's wait for a moment... Peter Scholze (Mar 15 2021 at 10:49): OK, I think this works :cold_sweat: New version of Analytic.pdf is on my homepage Johan Commelin (Mar 15 2021 at 11:04): @Peter Scholze So now the $\pm$ signs are gone. That is intentional, right? (I didn't check the proof of 9.5 yet) Peter Scholze (Mar 15 2021 at 11:08): Yes; I checked again how homotopies work, and apparently they shouldn't introduce minus signs there Johan Commelin (Mar 15 2021 at 13:55): @Peter Scholze I can confirm that lean thinks the problem with 9.6 is now solved :grinning: Johan Commelin (Mar 15 2021 at 13:56): There are two sorrys left. One related to the normed snake lemma, the other some annoying inequality involving cokernels. But both seem perfectly doable. Peter Scholze (Mar 15 2021 at 14:04): Ah, that's great to hear :-)! Peter Scholze (Mar 15 2021 at 14:09): I did get a little worried this morning; in the previous formulation, there was no way to get the induction to work (even if one was willing to change the constants). Johan Commelin (Mar 15 2021 at 14:19): In the previous proof, I had some half-assed attempt at setting up that $\delta$ in an ad-hoc fashion. But that wouldn't have worked, because it was too local. Johan Commelin (Mar 15 2021 at 14:20): Your current solution works great (the proofs even became shorter) because it's just a princpled approach directly at the start of the list of assumptions Johan Commelin (Mar 15 2021 at 14:20): Instead of hidden deep inside a subproof Johan Commelin (Mar 15 2021 at 18:20): I didn't check this formally, but I don't think I used in the proofs that $\delta$ is a map of complexes. Peter Scholze (Mar 15 2021 at 19:26): I think one uses it when implicitly arguing that $\delta(\tilde{x})$ maps to $\delta(x)$ in the notation of the manuscript Johan Commelin (Mar 15 2021 at 19:52): Hah, you are right! But in the Lean proof that was hidden away quite well. It's maybe a bit of an evil proof... Johan Commelin (Mar 15 2021 at 19:53): Because it doesn't make this explicit Johan Commelin (Mar 15 2021 at 19:53): Well, I guess it's about the same level of explicit as the proof in the PDF Johan Commelin (Mar 15 2021 at 19:54): In fact, I guess it's used in the definition of $\delta^{0,0}$ for the truncated double complex. Peter Scholze (Mar 15 2021 at 20:05): That's right Peter Scholze (Mar 15 2021 at 20:05): Well it's great if Lean is able to figure this out itself Johan Commelin (Mar 15 2021 at 20:41): The other outstanding sorry for 9.6 is now also filled in. So after the generalization to seminormed_group, all of 9.6 should be done. Peter Scholze (Mar 15 2021 at 20:43): OK, I feel like this is going in a good direction :-) Peter Scholze (Mar 15 2021 at 20:44): How much have you digested the proof of 9.5? Do you already have a feeling for how difficult it will be to formalize it? Johan Commelin (Mar 15 2021 at 20:49): To be honest, I'm feeling quite confident about it. I think I understand the global structure well. The part that I haven't looked at yet is the last bit of the proof where "condition 3" is checked. Johan Commelin (Mar 15 2021 at 20:49): The most hairy part will probably be 8.19 Johan Commelin (Mar 15 2021 at 20:51): And the moving back end forth between $\mathrm{Hom}(\Lambda'^{(m)}, M)$ and $\mathrm{Hom}(\Lambda', M)^{m/...}$ Johan Commelin (Mar 15 2021 at 20:51): Because that certainly is not going to be a defeq. Johan Commelin (Mar 15 2021 at 20:53): So we can construct the Cech conerve of $\Lambda \to \Lambda'$ and then construct the system of double complexes. But when we take columns of that, we need to build an isom to the Cech nerve of $\mathrm{Hom}(\Lambda', M) \to \mathrm{Hom}(\Lambda, M)$. Johan Commelin (Mar 15 2021 at 20:53): Or at least, we need to show that the columns are hypercovers. Johan Commelin (Mar 15 2021 at 20:53): But I think we should just dive in. We hit a wall, and then we learn. Johan Commelin (Mar 15 2021 at 20:54): We wrote 3 iterations of (co)chain complexes in two weeks time, and every version was better than the previous. Johan Commelin (Mar 15 2021 at 20:56): Johan Commelin said: To be honest, I'm feeling quite confident about it. I think I understand the global structure well. The part that I haven't looked at yet is the last bit of the proof where "condition 3" is checked. Of course there will be several inequalities where I will get hopelessly stuck because I didn't understand the details... but I'm sure we'll get past them, as we did in the past. Peter Scholze (Mar 15 2021 at 20:58): OK, that sounds great! :-) Johan Commelin (Mar 15 2021 at 20:58): Also, even though I am now starting to see the big picture... I have no idea how you ever came up with layer upon layer upon layer of induction arguments, inequality estimates, and generalizations into completely "ad hoc" directions that give you flexibility later on to make a step forward. Johan Commelin (Mar 15 2021 at 20:58): Chapeau! Peter Scholze (Mar 15 2021 at 20:59): Well, as I wrote in my e-mail, I was banging my head for a whole year against this problem, and almost got crazy over it Johan Commelin (Mar 15 2021 at 20:59): Yes, I can totally believe that Peter Scholze (Mar 15 2021 at 20:59): Especially because I always had at least 33% of me believing I was going in an insane direction Johan Commelin (Mar 15 2021 at 21:00): One thing that I want to try to do is build a definition that records all of the data needed to run the proof of 9.5. Peter Scholze (Mar 15 2021 at 21:01): Hmm OK; which parts do you want to generalize? Johan Commelin (Mar 15 2021 at 21:01): Such an abstraction usually helps in guiding lean in the right direction, and keeping things fast Johan Commelin (Mar 15 2021 at 21:01): Ideally Mbar r' S, and maybe even the construction of the system of complexes. Peter Scholze (Mar 15 2021 at 21:02): Aha. Well you need that Lemma 9.8 is true for this Johan Commelin (Mar 15 2021 at 21:02): So it would be something like: given a functor System : ProFinFiltPseuNormGrpWithTinv -> SystemOfComplexes that satisfies some homotopy condition... Johan Commelin (Mar 15 2021 at 21:02): Yes, so 9.8 will become an axiom Peter Scholze (Mar 15 2021 at 21:03): Hmm, but maybe more than that... Johan Commelin (Mar 15 2021 at 21:03): And then you build $\Lambda'^{(\bullet)}$, and use that to construct the system of double complexes. Johan Commelin (Mar 15 2021 at 21:03): Then you require as axiom that the columns are hypercovers. Peter Scholze (Mar 15 2021 at 21:03): Ah Johan Commelin (Mar 15 2021 at 21:03): And also admissibility becomes an axiom. Johan Commelin (Mar 15 2021 at 21:04): But I haven't thought much further beyond that. Peter Scholze (Mar 15 2021 at 21:04): Hmm... OK... I'm slightly afraid there'll be lots of axioms Johan Commelin (Mar 15 2021 at 21:04): 9.2 has to enter the picture as well. Peter Scholze (Mar 15 2021 at 21:04): Right Johan Commelin (Mar 15 2021 at 21:04): Yes, but Lean doesn't care about having a list of 25 axioms. Peter Scholze (Mar 15 2021 at 21:05): Sure... I think I can see your point, it may also help in digesting this proof to analyze it in this way Johan Commelin (Mar 15 2021 at 21:06): Just to illustrate: here is the output of #print linear_ordered_comm_ring Johan Commelin (Mar 15 2021 at 21:07): @[class, protect_proj list.nil.{0} name] structure linear_ordered_comm_ring : Type u → Type u fields: linear_ordered_comm_ring.add : Π {α : Type u} [c : linear_ordered_comm_ring α], α → α → α linear_ordered_comm_ring.add_assoc : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b c_1 : α), a + b + c_1 = a + (b + c_1) linear_ordered_comm_ring.zero : Π {α : Type u} [c : linear_ordered_comm_ring α], α linear_ordered_comm_ring.zero_add : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a : α), 0 + a = a linear_ordered_comm_ring.add_zero : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a : α), a + 0 = a linear_ordered_comm_ring.neg : Π {α : Type u} [c : linear_ordered_comm_ring α], α → α linear_ordered_comm_ring.sub : Π {α : Type u} [c : linear_ordered_comm_ring α], α → α → α linear_ordered_comm_ring.sub_eq_add_neg : ∀ {α : Type u} [c : linear_ordered_comm_ring α], auto_param (∀ (a b : α), a - b = a + -b) (name.mk_string "try_refl_tac" name.anonymous) linear_ordered_comm_ring.add_left_neg : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a : α), -a + a = 0 linear_ordered_comm_ring.add_comm : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b : α), a + b = b + a linear_ordered_comm_ring.mul : Π {α : Type u} [c : linear_ordered_comm_ring α], α → α → α linear_ordered_comm_ring.mul_assoc : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b c_1 : α), a * b * c_1 = a * (b * c_1) linear_ordered_comm_ring.one : Π {α : Type u} [c : linear_ordered_comm_ring α], α linear_ordered_comm_ring.one_mul : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a : α), 1 * a = a linear_ordered_comm_ring.mul_one : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a : α), a * 1 = a linear_ordered_comm_ring.left_distrib : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b c_1 : α), a * (b + c_1) = a * b + a * c_1 linear_ordered_comm_ring.right_distrib : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1 linear_ordered_comm_ring.le : Π {α : Type u} [c : linear_ordered_comm_ring α], α → α → Prop linear_ordered_comm_ring.lt : Π {α : Type u} [c : linear_ordered_comm_ring α], α → α → Prop linear_ordered_comm_ring.le_refl : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a : α), a ≤ a linear_ordered_comm_ring.le_trans : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1 linear_ordered_comm_ring.lt_iff_le_not_le : ∀ {α : Type u} [c : linear_ordered_comm_ring α], auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous) linear_ordered_comm_ring.le_antisymm : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b : α), a ≤ b → b ≤ a → a = b linear_ordered_comm_ring.add_le_add_left : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b linear_ordered_comm_ring.zero_le_one : ∀ {α : Type u} [c : linear_ordered_comm_ring α], 0 ≤ 1 linear_ordered_comm_ring.mul_pos : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b : α), 0 < a → 0 < b → 0 < a * b linear_ordered_comm_ring.le_total : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b : α), a ≤ b ∨ b ≤ a linear_ordered_comm_ring.decidable_le : Π {α : Type u} [c : linear_ordered_comm_ring α], decidable_rel has_le.le linear_ordered_comm_ring.decidable_eq : Π {α : Type u} [c : linear_ordered_comm_ring α], decidable_eq α linear_ordered_comm_ring.decidable_lt : Π {α : Type u} [c : linear_ordered_comm_ring α], decidable_rel has_lt.lt linear_ordered_comm_ring.exists_pair_ne : ∀ {α : Type u} [c : linear_ordered_comm_ring α], ∃ (x y : α), x ≠ y linear_ordered_comm_ring.mul_comm : ∀ {α : Type u} [c : linear_ordered_comm_ring α] (a b : α), a * b = b * a  Peter Scholze (Mar 15 2021 at 21:07): Bah Johan Commelin (Mar 15 2021 at 21:07): Of course those are auto-generated from other definitions lower in the hierarchy. But still, this is how lean thinks of linear ordered commutative rings under the hood. Peter Scholze (Mar 15 2021 at 21:08): Fun! :octopus: Johan Commelin (Mar 15 2021 at 21:08): With 9.6 we already did something like this, on a smaller scale. (And you do it in the pdf as well, in some sense.) Peter Scholze (Mar 15 2021 at 21:08): What do you mean? Johan Commelin (Mar 15 2021 at 21:09): /-- The assumptions on M in Proposition 9.6 bundled into a structure. -/ structure normed_spectral_conditions (M : system_of_double_complexes.{u}) (m : ℕ) (k K k' ε : ℝ≥0) [fact (1 ≤ k)] [fact (1 ≤ k')] (c₀ H : ℝ≥0) [fact (0 < H)] := (col_exact : ∀ j ≤ m, (M.col j).is_weak_bounded_exact k K m c₀) (row_exact : 0 < m → ∀ i ≤ m + 1, (M.row i).is_weak_bounded_exact k K (m-1) c₀) (h : Π (q : ℕ) {q' : ℕ} {c}, M.X (k' * c) 0 q' ⟶ M.X c 1 q) (h_bound_by : ∀ (q q' : ℕ) (hq : q ≤ m) (hq' : q+1 = q') (c) [fact (c₀ ≤ c)], (h q : M.X (k' * c) 0 q' ⟶ M.X c 1 q).bound_by H) -- δ only needs to be a map of complexes in degrees ≤ m; we might need to weaken this (δ : Π (c : ℝ≥0), (M.row 0).obj (op$ c) ⟶ (M.row 1).obj (op \$ k' * c))
(hδ : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (q : ℕ) (hq : q ≤ m) (x : M.X (k' * (k' * c)) 0 q),
(δ c).f q (M.res x) = M.res (M.d 0 1 x) + h q (M.d' q (q+1) x) + M.d' (q-1) q (h (q-1) x))
(δ_bound_by : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (q : ℕ) (hq : q ≤ m), ((δ c).f q).bound_by ε)
-- ergonomics: we bundle this assumption, instead of passing it around separately


Johan Commelin (Mar 15 2021 at 21:09):

This is the a definition before the statement of the lemma

Johan Commelin (Mar 15 2021 at 21:09):

/-- Proposition 9.6 in [Analytic] -/
theorem normed_spectral (m : ℕ) (c₀ H : ℝ≥0) [fact (0 < H)]
(M : system_of_double_complexes.{u}) (k K k' : ℝ≥0)
[fact (1 ≤ k)] [hK : fact (1 ≤ K)] [fact (k₀ m k ≤ k')] [fact (1 ≤ k')]
(cond : M.normed_spectral_conditions m k K k' (ε m K) c₀ H) :
(M.row 0).is_weak_bounded_exact (k' * k') (2 * K₀ m K * H) m c₀ :=


Johan Commelin (Mar 15 2021 at 21:10):

For completeness:

noncomputable
def ε : Π (m : ℕ) (K : ℝ≥0), ℝ≥0
| 0     K := (2 * K)⁻¹
| (m+1) K := ε m (K * (K * K + 1))

noncomputable
def k₀ : Π (m : ℕ) (k : ℝ≥0), ℝ≥0
| 0     k := k
| (m+1) k := k₀ m (k * k * k)

noncomputable
def K₀ : Π (m : ℕ) (K : ℝ≥0), ℝ≥0
| 0     K := K
| (m+1) K := K₀ m (K * (K * K + 1))


Peter Scholze (Mar 15 2021 at 21:11):

Ah! I just wanted to complain that I don't see the "exists $\epsilon$ and $k'$"

Peter Scholze (Mar 15 2021 at 21:12):

So this is how Lean will be able to compute all desired constants at the end

Yep

Cool!

Peter Scholze (Mar 15 2021 at 21:12):

Anyways, I'm off for tonight!

Cheers!

Johan Commelin (Mar 15 2021 at 21:12):

Thanks for all your help today!

Last updated: May 09 2021 at 16:20 UTC