Zulip Chat Archive

Stream: condensed mathematics

Topic: spectral 9.6


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 21:31):

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

view this post on Zulip Riccardo Brasca (Jan 25 2021 at 21:34):

In the main theorem everything is complete, right?

view this post on Zulip Johan Commelin (Jan 25 2021 at 21:34):

yup

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 25 2021 at 21:48):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:51):

Is anyone working towards this?

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:52):

I think we have all the ingredients

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Feb 05 2021 at 21:49):

Ah, I see. Thanks.

view this post on Zulip 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)] :
   (ε : ) ( : ε > 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) xMc0,q+1x \in M_c^{0,q+1}. This has a typo: the cc should be kck'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.

view this post on Zulip 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) xMc0,q+1x \in M_c^{0,q+1}. This has a typo: the cc should be kck'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=0q=0, in which case hq1=0h^{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.

view this post on Zulip Johan Commelin (Feb 06 2021 at 03:44):

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

view this post on Zulip Johan Commelin (Feb 06 2021 at 03:51):

Thanks for refactoring row and col.

view this post on Zulip Johan Commelin (Feb 06 2021 at 04:02):

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

view this post on Zulip 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.

view this post on Zulip 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.

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

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

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Feb 06 2021 at 07:00):

Thanks for the improvements @Johan Commelin.

Indexing complexes by all of Z\mathbb{Z} makes sense. I just fixed so hh is also defined for q<0q<0. I expect we will also need to add assumptions to various theorems stating that Mp,q=0M^{p,q}=0 if p<0p<0 or q<0q<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.

view this post on Zulip 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)

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

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

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

Because we'll need that for the proof of 9.6

view this post on Zulip 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?

view this post on Zulip 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)

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

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

view this post on Zulip 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

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

Maybe...

view this post on Zulip 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

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

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

view this post on Zulip Riccardo Brasca (Feb 15 2021 at 13:33):

Yes

view this post on Zulip 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

view this post on Zulip 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.

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

It's probably fine

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

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

view this post on Zulip 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

view this post on Zulip 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.

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

Yes, thanks for reminding me of that

view this post on Zulip Riccardo Brasca (Feb 15 2021 at 14:00):

@Sebastien Gouezel yes, of course!

view this post on Zulip 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

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

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

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

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 16 2021 at 14:43):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Feb 16 2021 at 14:56):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Feb 16 2021 at 16:30):

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

view this post on Zulip 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 ε/2\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.

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

@Riccardo Brasca great work, thanks a lot!

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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 :=
...

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 17:05):

The PR is talking about a def. The file in lean-liquid is littered with @s.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 28 2021 at 17:07):

If it's usually left unapplied then I would keep the other arguments explicit

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 28 2021 at 17:10):

if it's a function, then the later argument would be C.X c' p q

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 :-/

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 01 2021 at 13:55):

But of course some of the theorems might need to assume this.

view this post on Zulip Johan Commelin (Mar 01 2021 at 13:55):

By the way, it might be easier to assume that d i = 0 for negative i

view this post on Zulip Johan Commelin (Mar 01 2021 at 13:56):

Because that's an equality of terms, instead of some isom in a category.

view this post on Zulip Johan Commelin (Mar 01 2021 at 13:57):

Note that for the proof of normed_snake we don't need any nonzeroness assumptions

view this post on Zulip Riccardo Brasca (Mar 01 2021 at 13:57):

In the paper all complexes are indexed by nonnegative integer, aren't they? 9.6 says "Mcp,q,p,q0M_c^{p,q}, p,q \geq 0..."

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 13:57):

but d i = 0 doesn't imply Mi,j=0M_{i,j}=0 right? Are you saying that I have to modify the statement of 9.6 that we have?

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:04):

Hmm, I thought that claiming we only prove something for p,q >= 0 would suffice

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:04):

Why are you worried that this isn't enough?

view this post on Zulip 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\N? I can see many settings in math where the complex is genuinely indexed by N\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.

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:05):

ooh, you mean that is_bounded_exact doesn't make that assumption?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:07):

Because of DTT issues

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 14:09):

OK so here is a mathematics question: is i=1i=-1 OK in that definition?

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 14:12):

From my reading of the proof of 9.6, i=1i=-1 is OK because this is exactly what is being proved in the m=0m=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.

view this post on Zulip Riccardo Brasca (Mar 01 2021 at 14:17):

Does 9.6 really requires Mcp,q=0M_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 jm j \leq m" instead of "for j=0,,mj = 0,\ldots, m..." etc, but I have the impression that, if we want to keep Z\mathbb{Z}-graded complexes, this is the most natural think to do

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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=0i= 0" just because, strictly speaking, Cci1C^{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 00 in negative degrees. But I don't know if all the proofs works in general

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 00.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:34):

But I don't know whether that's strong enough

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:38):

I guess we could change is_bounded_exact to ignore negative i

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:38):

Or i < -1, if we need the -1 case

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)->...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 14:47):

Well we won't be proving the theorem as it currently stands :-)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 14:48):

Yes I agree! I just hadn't realised that this was the game we were playing :-)

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:48):

That might make the whole thing provable again

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 14:49):

The issue right now is that the constants are all wrong

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 14:49):

I mean literally wrong

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 14:51):

I can fix this, I just need to write a two hour workshop first

view this post on Zulip Johan Commelin (Mar 01 2021 at 14:52):

Sure, provable modulo constants :rofl:

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Mar 01 2021 at 15:09):

I'm going to make m an integer in that file

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 01 2021 at 16:17):

Johan Commelin said:

Sure, provable modulo constants :rofl:

Can this be formalized with filters?

view this post on Zulip 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.

view this post on Zulip 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 1\le -1.

view this post on Zulip Johan Commelin (Mar 02 2021 at 07:04):

I moved everything about 9.6 to normed_spectral.lean

view this post on Zulip Johan Commelin (Mar 02 2021 at 12:14):

I think we need to be very careful with how we phrase 9.6.

view this post on Zulip Johan Commelin (Mar 02 2021 at 12:15):

Because, when working with nat, im1\forall i \le m - 1 is an empty condition when m=0m = 0, in ordinary maths. But in lean it isn't...

view this post on Zulip Johan Commelin (Mar 02 2021 at 12:15):

On the other hand, i<m\forall i < m, would work...

view this post on Zulip Johan Commelin (Mar 02 2021 at 12:15):

These sort of annoyances will have to be sorted out (-;

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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 ---> ...

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Mar 03 2021 at 11:08):

Idem for weak exactness

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 03 2021 at 11:44):

@Julian Külshammer ok, that's a useful tip!

view this post on Zulip Johan Commelin (Mar 03 2021 at 11:45):

Does that include the shift? Or would soft_truncation place C1/C0 in degree 1?

view this post on Zulip Julian Külshammer (Mar 03 2021 at 11:47):

This does not include the shift, so there is a slight difference, right.

view this post on Zulip Johan Commelin (Mar 03 2021 at 11:49):

Well, I guess we could factor it into those two steps, that doesn't hurt.

view this post on Zulip Johan Commelin (Mar 03 2021 at 11:49):

After all, we already have the shift functor.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 03 2021 at 12:12):

Hah, that would actually be quite nice, if we could get to that definition.

view this post on Zulip 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.

view this post on Zulip Julian Külshammer (Mar 03 2021 at 13:09):

You are right, I also noticed in the meantime.

view this post on Zulip Johan Commelin (Mar 03 2021 at 13:13):

maybe we can still call this soft_truncation'

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Mar 03 2021 at 13:35):

@Riccardo Brasca hmm, good point... my sketch was a bit too naive

view this post on Zulip Johan Commelin (Mar 03 2021 at 13:35):

Because we aren't working in the category CompleteNormedGroup

view this post on Zulip 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

view this post on Zulip 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/

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 03 2021 at 13:37):

Did you define some sort of lift?

view this post on Zulip Johan Commelin (Mar 03 2021 at 13:38):

We'll need some sort of universal property to define soft_truncation'

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 03 2021 at 13:40):

you only need boundedness

view this post on Zulip 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...)

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 13:45):

I don't have time this afternoon, but I can write it later today

view this post on Zulip Johan Commelin (Mar 03 2021 at 13:50):

boundedness implies continuity, but I have no idea whether the converse is true in this setting

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 14:06):

Now I have the impression that a small modification the proof that the seminorm on X/YX/Y is actually a norm only requires YY to be closed in XX (now the assumption is completeness), without assuming that XX is complete. The kernel of a continuous map is always closed, so maybe have cokernel without too much troubles

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Mar 03 2021 at 14:30):

Nice... that seems to be a general pattern (-;

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:26):

@Peter Scholze I'm confused about the base case of the normed spectral sequence 9.6.

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:26):

OK...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:26):

I seem to be getting K * (H + 1/2)

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:27):

Instead of 2 * K * H

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:27):

oh, ok, that's not too bad then :-)

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:28):

Hmm, is this in Lean or on paper?

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:28):

it's not completely in Lean yet.

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:29):

Because if it's on paper, I would think you do the wrong manipulation

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:29):

You need to subtract the term kϵxcMc0,0k\epsilon ||x_c||_{M_c^{0,0}}

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:30):

I guess that's now KϵxcMc0,0K\epsilon||x_c||_{M_c^{0,0}}, but never mind

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:30):

Ooh, I wasn't planning on doing that :oops:

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:30):

I see... then I need to think about the correct manipulation again

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:33):

I thought dkc0,0(xkc)dkc0,0(xkc)hk2c0(dk2c0,0(x))+hk2c0(dk2c0,0(x))\|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))\|

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:33):

Is that one of the manipulations that you had in mind?

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:33):

That sounds too complicated

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:34):

Do you agree with second displayed inequality on page 61?

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:34):

I'm stuck on the second \le in that display

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:35):

Well, I managed to prove it using the beast I posted above

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:35):

Ah, yes, sorry, I guess this uses what you've written

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:36):

And I thought this would just reuse the final display on p60

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:36):

Yes. But if you set ϵ=12k\epsilon=\tfrac 1{2k}, then the first summand on the right is half of the term on the left

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:37):

So you can subtract, leaving half of the left-hand side, so multiplying by 22 gives what I claim

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:37):

ooh, of course :face_palm:

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:37):

gotcha, you're not just chaining them

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:37):

Yeah, it's a confusing part! Usually you never do that thing

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:37):

I should have maybe made that more explicit

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:38):

This argument actually feels "wrong" to me, but I think it works

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:39):

Ok, this also means that I canceled K too early

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 + ε

view this post on Zulip 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 -.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 11 2021 at 13:01):

Lol, I need to take a break I guess (-; :face_palm:

view this post on Zulip Johan Commelin (Mar 11 2021 at 13:01):

You are completely right

view this post on Zulip 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 Mp,qM^{p,q} and shift it all one to the left, giving us a new complex Np,qN^{p,q} with the "0th column" Np,0N^{p,0} defined as Mp,1/Mp,0M^{p,1}/M^{p,0} with its quotient norm. The claim (as I understand it) is that if MM satisfies all the conditions in the statement of 9.6 for mm then (with possibly different constants) NN satisfies all the conditions for m1m-1. The one I'm stuck on is condition (3), the case q=0q=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 xx in N0,0N^{0,0}, L(x)ϵres(x)|L(x)| \leq\epsilon|res(x)|. Here LL is an abelian group hom (a sum of three homs actually, two of them with ±\pm signs) from N0,0:=M0,1/M0,0N^{0,0} :=M^{0,1}/M^{0,0} to N1,0:=M1,1/M1,0N^{1,0} := M^{1,1}/M^{1,0} induced by some L:M0,1M1,1L' : M^{0,1}\to M^{1,1}, and the fact that MM satisfies the conditions of 9.6 tells us that L(x~)ϵres(x~)|L'(\tilde{x})| \leq\epsilon|res(\tilde{x})| for all x~\tilde{x} in M0,1M^{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 NN in the q=0q=0 case.

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 19:13):

Aah! As well as LL' I also have L:M0,0M1,0L'' : M^{0,0}\to M^{1,0} with L(y)ϵres(y)|L''(y)|\leq\epsilon|res(y)| for all yM0,0y\in M^{0,0}. Am I supposed to be using this somehow? This is condition (3) when q=0q=0 for MM; the LL' in the previous post was coming from q=1q=1 for MM.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 23:59):

I can't use LL'' because I don't know any relation between hkc0h^0_{k'c} and hkc1h^1_{k'c} (for MM). I had assumed that to define h0h^0 for NN I just used hkc1h^1_{k'c} for MM. But now I realise that in fact maybe LL' doesn't even reduce to LL the way I thought things worked because in the NN world there is no dkc1,q1d'^{1,q-1}_{k'c} term when d=0d=0 but in the MM world you have q=1q=1 so there's an extra term -- oh but it's in the image of M1,0M^{1,0} so makes no difference.

To summarise, my worry is if xM0,1x\in M^{0,1} is close to the image of M0,0M^{0,0}, because then in the NN world the norm of xx 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 h1:M0,2M1,1h^1:M^{0,2}\to M^{1,1} term.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 15 2021 at 10:01):

OK, I'm getting myself seriously confused here. It may take a moment.

view this post on Zulip 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 Mk2c0,Mkc1,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 Mk2c0,Mc0,M_{k'^2c}^{0,\bullet}\to M_c^{0,\bullet} and a map of complexes Mc0,Mkc1,M_c^{0,\bullet}\to M_{k'c}^{1,\bullet} that is (in each degree) of norm ϵ\leq\epsilon.

view this post on Zulip Peter Scholze (Mar 15 2021 at 10:14):

(Actually, maybe it's not necessary that this is a map of complexes?)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Peter Scholze (Mar 15 2021 at 10:16):

OK, it should be map of complexes, but anyway it is.

view this post on Zulip Johan Commelin (Mar 15 2021 at 10:17):

Great! Let's see if this fixes it

view this post on Zulip Peter Scholze (Mar 15 2021 at 10:18):

Well, let's wait for a moment...

view this post on Zulip Peter Scholze (Mar 15 2021 at 10:49):

OK, I think this works :cold_sweat: New version of Analytic.pdf is on my homepage

view this post on Zulip 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)

view this post on Zulip Peter Scholze (Mar 15 2021 at 11:08):

Yes; I checked again how homotopies work, and apparently they shouldn't introduce minus signs there

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 15 2021 at 14:04):

Ah, that's great to hear :-)!

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 15 2021 at 14:20):

Instead of hidden deep inside a subproof

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 15 2021 at 19:26):

I think one uses it when implicitly arguing that δ(x~)\delta(\tilde{x}) maps to δ(x)\delta(x) in the notation of the manuscript

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Mar 15 2021 at 19:53):

Because it doesn't make this explicit

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 15 2021 at 19:54):

In fact, I guess it's used in the definition of δ0,0\delta^{0,0} for the truncated double complex.

view this post on Zulip Peter Scholze (Mar 15 2021 at 20:05):

That's right

view this post on Zulip Peter Scholze (Mar 15 2021 at 20:05):

Well it's great if Lean is able to figure this out itself

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 15 2021 at 20:43):

OK, I feel like this is going in a good direction :-)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 15 2021 at 20:49):

The most hairy part will probably be 8.19

view this post on Zulip Johan Commelin (Mar 15 2021 at 20:51):

And the moving back end forth between Hom(Λ(m),M)\mathrm{Hom}(\Lambda'^{(m)}, M) and Hom(Λ,M)m/...\mathrm{Hom}(\Lambda', M)^{m/...}

view this post on Zulip Johan Commelin (Mar 15 2021 at 20:51):

Because that certainly is not going to be a defeq.

view this post on Zulip 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 Hom(Λ,M)Hom(Λ,M)\mathrm{Hom}(\Lambda', M) \to \mathrm{Hom}(\Lambda, M).

view this post on Zulip Johan Commelin (Mar 15 2021 at 20:53):

Or at least, we need to show that the columns are hypercovers.

view this post on Zulip Johan Commelin (Mar 15 2021 at 20:53):

But I think we should just dive in. We hit a wall, and then we learn.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 15 2021 at 20:58):

OK, that sounds great! :-)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 15 2021 at 20:58):

Chapeau!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 15 2021 at 20:59):

Yes, I can totally believe that

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:01):

Hmm OK; which parts do you want to generalize?

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:01):

Such an abstraction usually helps in guiding lean in the right direction, and keeping things fast

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:01):

Ideally Mbar r' S, and maybe even the construction of the system of complexes.

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:02):

Aha. Well you need that Lemma 9.8 is true for this

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:02):

Yes, so 9.8 will become an axiom

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:03):

Hmm, but maybe more than that...

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:03):

And then you build Λ()\Lambda'^{(\bullet)}, and use that to construct the system of double complexes.

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:03):

Then you require as axiom that the columns are hypercovers.

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:03):

Ah

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:03):

And also admissibility becomes an axiom.

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:04):

But I haven't thought much further beyond that.

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:04):

Hmm... OK... I'm slightly afraid there'll be lots of axioms

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:04):

9.2 has to enter the picture as well.

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:04):

Right

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:04):

Yes, but Lean doesn't care about having a list of 25 axioms.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:06):

Just to illustrate: here is the output of #print linear_ordered_comm_ring

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:07):

Bah

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:08):

Fun! :octopus:

view this post on Zulip 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.)

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:08):

What do you mean?

view this post on Zulip 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))
( :  (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
(admissible : M.admissible)

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:09):

This is the a definition before the statement of the lemma

view this post on Zulip 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₀ :=

view this post on Zulip 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))

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:11):

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

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:12):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:12):

Yep

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:12):

Cool!

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:12):

Anyways, I'm off for tonight!

view this post on Zulip Peter Scholze (Mar 15 2021 at 21:12):

Cheers!

view this post on Zulip Johan Commelin (Mar 15 2021 at 21:12):

Thanks for all your help today!


Last updated: May 09 2021 at 16:20 UTC