spectral 9.6

Stream: condensed mathematics

[Johan Commelin]

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]

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

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]

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]

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

[Riccardo Brasca]

In the main theorem everything is complete, right?

[Johan Commelin]

yup

[Riccardo Brasca]

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]

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]

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]

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

[Johan Commelin]

Is anyone working towards this?

[Johan Commelin]

I think we have all the ingredients

[Peter Scholze]

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

[Johan Commelin]

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]

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

[Floris van Doorn]

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]

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]

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]

Ah, I see. Thanks.

[Floris van Doorn]

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]

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]

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

Thanks for refactoring row and col.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Because we'll need that for the proof of 9.6

[Riccardo Brasca]

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]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Johan Commelin]

Maybe...

[Johan Commelin]

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

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

[Riccardo Brasca]

Yes

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

It's probably fine

[Johan Commelin]

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

[Johan Commelin]

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

[Sebastien Gouezel]

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]

Yes, thanks for reminding me of that

[Riccardo Brasca]

@Sebastien Gouezel yes, of course!

[Riccardo Brasca]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

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]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

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]

@Riccardo Brasca great work, thanks a lot!

[Johan Commelin]

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]

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]

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]

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]

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

[Mario Carneiro]

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

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

[Bhavik Mehta]

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]

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

[Mario Carneiro]

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]

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]

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]

hah, good point... breen_deligne.package.system returns a system for which all objects in negative degrees are 0.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

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]

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]

yes, you might need to modify the conclusion (I didn't check) to say that you only prove something about nonneg indices

[Kevin Buzzard]

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]

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]

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]

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

[Johan Commelin]

Why are you worried that this isn't enough?

[Sebastien Gouezel]

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]

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

[Johan Commelin]

@Sebastien Gouezel I agree, and I think Scott has been experimenting with a new definition that generalises both concepts

[Johan Commelin]

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]

@Kevin Buzzard if assuming M_{i.j} = 0 works, then that's fine. But I'm worried that it isn't practical

[Johan Commelin]

Because of DTT issues

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

Our i is Peter's i+1 but Peter allows i=0 so we need to allow i=-1. That's all.

[Kevin Buzzard]

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]

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]

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]

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]

Riccardo you are right that the proofs might work in general. This hadn't occurred to me.

[Johan Commelin]

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

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

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]

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

yes, that's also what I was hoping to do by assuming d i = 0 for negative i

[Johan Commelin]

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

[Kevin Buzzard]

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]

I guess we could change is_bounded_exact to ignore negative i

[Johan Commelin]

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

[Kevin Buzzard]

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]

One reason for why one might want Z-indexed complexes is because you might want to use the shift functors.

[Kevin Buzzard]

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]

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]

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]

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]

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

[Johan Commelin]

It would be nice if we could just start formalising it, and fix the conclusion along the way

[Kevin Buzzard]

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

[Johan Commelin]

Would it make sense to add assumptions that things are is_bounded_exact for certain negative m to the assumptions?

[Johan Commelin]

That might make the whole thing provable again

[Kevin Buzzard]

The issue right now is that the constants are all wrong

[Kevin Buzzard]

I mean literally wrong

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

Sure, provable modulo constants :rofl:

[Damiano Testa]

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]

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

[Johan Commelin]

Maybe we want the \eps to be an nnreal, and use nnnorm instead of norms, to stay in the nonnegative world.

[Adam Topaz]

Johan Commelin said:

Sure, provable modulo constants :rofl:

Can this be formalized with filters?

[Johan Commelin]

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]

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]

I moved everything about 9.6 to normed_spectral.lean

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

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]

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]

Idem for weak exactness

[Johan Commelin]

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]

Probably a difference in terminology, but I would call the fold operation soft_truncation at 1.

[Johan Commelin]

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

[Johan Commelin]

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

[Julian Külshammer]

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

[Johan Commelin]

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

[Johan Commelin]

After all, we already have the shift functor.

[Johan Commelin]

And presumably soft_truncation would take i as argument, and truncate at degree i, instead of only at 0.

[Johan Commelin]

On the other hand, for i = 0, it can very nicely be defined using the equation compiler.

[Julian Külshammer]

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]

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

[Johan Commelin]

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]

You are right, I also noticed in the meantime.

[Johan Commelin]

maybe we can still call this soft_truncation'

[Riccardo Brasca]

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]

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

[Johan Commelin]

Because we aren't working in the category CompleteNormedGroup

[Johan Commelin]

And I don't think we should define it... sounds like we don't need the trouble

[Johan Commelin]

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]

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

Did you define some sort of lift?

[Johan Commelin]

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

[Riccardo Brasca]

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]

you only need boundedness

[Riccardo Brasca]

OK, boundedness of the lift is trivial (I thought that boundedness and continuity were equivalent... for normed space they are...)

[Riccardo Brasca]

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

[Johan Commelin]

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

[Riccardo Brasca]

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]

Even better, the proof of this more general fact seems easier than the current proof :sweat_smile:

[Johan Commelin]

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

[Johan Commelin]

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

[Peter Scholze]

OK...

[Johan Commelin]

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]

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

[Johan Commelin]

Instead of 2 * K * H

[Peter Scholze]

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

[Peter Scholze]

Hmm, is this in Lean or on paper?

[Johan Commelin]

it's not completely in Lean yet.

[Peter Scholze]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Peter Scholze]

That sounds too complicated

[Peter Scholze]

Do you agree with second displayed inequality on page 61?

[Johan Commelin]

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

[Johan Commelin]

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

[Peter Scholze]

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

[Johan Commelin]

Ok, and then you need to pass from the final part of that 2nd display to the conclusion

[Johan Commelin]

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

[Peter Scholze]

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]

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

[Johan Commelin]

ooh, of course :face_palm:

[Johan Commelin]

gotcha, you're not just chaining them

[Peter Scholze]

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

[Peter Scholze]

I should have maybe made that more explicit

[Peter Scholze]

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

[Johan Commelin]

Ok, this also means that I canceled K too early

[Johan Commelin]

@Peter Scholze thanks for getting me unstuck there! The base case is now sorry-free in lean

[Kevin Buzzard]

In some sense that felt like most of the work -- the inductive step follows from something else, right?

[Johan Commelin]

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]

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]

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]

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]

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

[Johan Commelin]

You are completely right

[Kevin Buzzard]

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]

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]

This sounds exactly like the annoyance we already had in 9.10... if the issue persists, I'll think about it tomorrow

[Kevin Buzzard]

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]

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]

But it might certainly be the case that we are just chaining some inequalities in the wrong order again.

[Peter Scholze]

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

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

[Peter Scholze]

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]

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

[Peter Scholze]

In any case, this stronger condition is verified when 9.6 is applied in the proof of 9.5.

[Peter Scholze]

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]

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

[Johan Commelin]

Great! Let's see if this fixes it

[Peter Scholze]

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

[Peter Scholze]

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

[Johan Commelin]

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

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

[Johan Commelin]

@Peter Scholze I can confirm that lean thinks the problem with 9.6 is now solved :grinning:

[Johan Commelin]

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]

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

[Peter Scholze]

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]

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]

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]

Instead of hidden deep inside a subproof

[Johan Commelin]

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]

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

[Johan Commelin]

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]

Because it doesn't make this explicit

[Johan Commelin]

Well, I guess it's about the same level of explicit as the proof in the PDF

[Johan Commelin]

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

[Peter Scholze]

That's right

[Peter Scholze]

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

[Johan Commelin]

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]

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

[Peter Scholze]

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]

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]

The most hairy part will probably be 8.19

[Johan Commelin]

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

[Johan Commelin]

Because that certainly is not going to be a defeq.

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

We wrote 3 iterations of (co)chain complexes in two weeks time, and every version was better than the previous.

[Johan Commelin]

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]

OK, that sounds great! :-)

[Johan Commelin]

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]

Chapeau!

[Peter Scholze]

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]

Yes, I can totally believe that

[Peter Scholze]

Especially because I always had at least 33% of me believing I was going in an insane direction

[Johan Commelin]

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]

Hmm OK; which parts do you want to generalize?

[Johan Commelin]

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

[Johan Commelin]

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

[Peter Scholze]

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

[Johan Commelin]

So it would be something like: given a functor System : ProFinFiltPseuNormGrpWithTinv -> SystemOfComplexes that satisfies some homotopy condition...

[Johan Commelin]

Yes, so 9.8 will become an axiom

[Peter Scholze]

Hmm, but maybe more than that...

[Johan Commelin]

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

[Johan Commelin]

Then you require as axiom that the columns are hypercovers.

[Peter Scholze]

Ah

[Johan Commelin]

And also admissibility becomes an axiom.

[Johan Commelin]

But I haven't thought much further beyond that.

[Peter Scholze]

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

[Johan Commelin]

9.2 has to enter the picture as well.

[Peter Scholze]

Right

[Johan Commelin]

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

[Peter Scholze]

Sure... I think I can see your point, it may also help in digesting this proof to analyze it in this way

[Johan Commelin]

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

[Johan Commelin]

@[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]

Bah

[Johan Commelin]

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]

Fun! :octopus:

[Johan Commelin]

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]

What do you mean?

[Johan Commelin]

/-- 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
(admissible : M.admissible)

[Johan Commelin]

This is the a definition before the statement of the lemma

[Johan Commelin]

/-- 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]

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]

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

[Peter Scholze]

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

[Johan Commelin]

Yep

[Peter Scholze]

Cool!

[Peter Scholze]

Anyways, I'm off for tonight!

[Peter Scholze]

Cheers!

[Johan Commelin]

Thanks for all your help today!