thm95.homotopy

Stream: condensed mathematics

[Johan Commelin]

Status update: I've been working on the last part of the proof of 9.5, where we need to construct a homotopy between two maps between the first two rows of a certain double complex.
(Aside: at some point, I said that the middle part of the proof (condition col_exact) might be the hardest to formalize. Now I'm hoping sincerely that this third part is actually the hardest... because it's quite hard right now :grinning:)

What we have right now is a whole bunch of definitions and some sorryd lemmas that ultimately give us a homotopy between two maps between the first row of the double complex and another complex C. What is left:

• construct an isomorphism between C and the second row of the double complex
• show that one of the homotopic maps, composed with :this: isomorphism gives the vertical differential in the double complex
• the actual proof of the homotopy condition

[Johan Commelin]

What is making this hard, is that the objects in the double complex are functorial in something like 6 different directions, and we need to move in all those 6 directions

[Johan Commelin]

So, if we don't maneuver carefully, then we need to show that all the faces of a 6-dimensional cube commute.

[Johan Commelin]

If we had some automation to help us...

[Johan Commelin]

But I don't think this part can be easily automated

[Peter Scholze]

Hmm that's bad. What are the 6 directions?

[Johan Commelin]

Let me see:

• $\Lambda$, the lattice
• $M$, the profinitely filtered pseudo normed group with action of $T^{-1}$
• BD, a package of Breen--Deligne data (ranks + formal sums of matrices)
• $(c'_i)_i$, some constants, which can be rescaled
• $c$, an independent constant
• $V$, some normed group, on which $T$ acts

[Peter Scholze]

Wait, aren't most of those kept constant during the proof?

[Johan Commelin]

So far, I have been able to avoid tweaking the $c'_i$, but all the others move

[Peter Scholze]

Why are BD and $V$ moving?

[Johan Commelin]

$V$ doesn't really move, but $T$ acts on it, so you still need some sort of functoriality of several constructions.

[Peter Scholze]

Ah

[Johan Commelin]

BD moves because the homotopy is a priori a hom BD.double -> BD

[Peter Scholze]

Ah...

[Johan Commelin]

And you need to convert that into a homotopy between the system of M relative to BD and the system of M^2 relative to BD

[Johan Commelin]

But at first you get the system of M relative to BD.double

[Johan Commelin]

And somewhere in the middle you need to rescale M or the c'_i to take into account that summation on M isn't strict.

[Peter Scholze]

Hmm, it isn't even just for the double, but for double $^m$, right?

[Johan Commelin]

Yes, so you have to throw another induction in the mix

[Peter Scholze]

Hmm, I hoped that some of this is taken care of by those lemmas in the appendix, but I'm not sure how much they help with the question at hand

[Johan Commelin]

Currently I'm wondering whether the diagonal embedding $\Lambda \to \Lambda'$ should also be an $N$-fold iteration of $\Lambda \to \Lambda \oplus \Lambda$.

[Peter Scholze]

That might be useful

[Johan Commelin]

Those two lemmas have all the maths content. All that needs to happen is composing a bunch of "canonical" isomorphisms.

[Johan Commelin]

So, here's a question about the middle part of the proof, the Dold-Kan part/condition: do we need to know anything about the map $\Lambda \to \Lambda'$ there?

[Johan Commelin]

A first sight, it seems that we just use that we have a cosimplicial complex, and we push this through $\mathrm{Hom}(\_, M)$

[Peter Scholze]

Do you mean condition (2) of 9.6?

[Johan Commelin]

yes

[Peter Scholze]

Well, you need 9.8

[Johan Commelin]

Ooh, yes, of course.

[Peter Scholze]

But to get the right estimate for condition (3) in 9.6, you do need to take $N$ large enough

[Peter Scholze]

I think you can't get that by some inductive argument

[Johan Commelin]

So at some point we have to move between $(\_)^N$ and $((((\_)^2)^2)^2)^2$

[Peter Scholze]

Of course the desired commutative diagram can likely be chained together by an inductive argument

[Johan Commelin]

Currently I'm trying to figure out what is the most ergonomic place to do that

[Johan Commelin]

Maybe it's best to prove that $\Lambda \to \Lambda'$ is isomorphic to an n-fold iteration of $\Lambda \to \Lambda \oplus \Lambda$

[Peter Scholze]

Sounds reasonable

[Johan Commelin]

(Of course there is a rescale on the codomain, just to make sure this will not be too trivial :rofl:)

[Peter Scholze]

Right. And I think when chaining stuff together, some more constants might move... argh.

[Johan Commelin]

Hmm, which constants do you mean?

[Peter Scholze]

One question about the 6-dimensional cubes: Mathwise it's enough that all the squares commute (in $1$-categories, as we are in). Is Lean also happy with only knowing that the squares commute?

[Peter Scholze]

Well, I'm not sure which ones I mean; probably none.

[Johan Commelin]

Not without further help, but it's certainly true that after you know the squares commute, the rest of the work is mechanical and can make use of some automation

[Johan Commelin]

I mean, once you start taking paths on the cube whose length is > 2... then you can homotope them to each other along the squares.

[Peter Scholze]

right

[Johan Commelin]

But in the current setting it would take some effort to make Lean do this alone.

[Peter Scholze]

Is this something that could be proved in Lean in a very abstract setting?

[Johan Commelin]

The problem is that there isn't enough abstraction so that Lean can only do the right thing. There is too much concrete distraction, so it will probably get itself confused.

[Johan Commelin]

But I got very confused trying to figure out what the correct abstraction would be, in a form where it is still applicable to the setting at hand

[Peter Scholze]

It's funny that Lean works like a real mathematician here: You explain general statements in the right generality, then they become self-evident

[Johan Commelin]

Yes, this point is even more important when formalising things.

[Peter Scholze]

From the quasi-categorical perspective, I would probably try to formalize the statement that if $S\hookrightarrow S'$ is an injection of simplicial sets with the same $2$-skeleton, then any map $S\to C$ to some category $C$ (i.e. its nerve) extends uniquely to $S'$

[Peter Scholze]

But I'm not sure whether this can be translated into the question at hand

[Johan Commelin]

If we want to automate this, it's probably most effective to have some term rewriting system that we feed the commutativity assumptions of the squares, and then ask it to use some shortest path algorithm to rewrite one expression into another.

[Johan Commelin]

That machinery is already there, but I'm currently spoon-feeding it the order in which to rewrite along the cubes.

[Peter Scholze]

I see

[Johan Commelin]

The part that is the least functorial at the moment is $(\_)^{T^{-1}}$

[Johan Commelin]

We could factor the construction through a category NormedGroup_with_two_Tinv_actions...

[Johan Commelin]

But I'm reluctant to do that...

[Johan Commelin]

It seems that you never need to know that the homotopy is compatible with restriction maps

[Johan Commelin]

At least that is 1 square that we don't need to worry about (-;

[Peter Scholze]

That's surprising!

[Peter Scholze]

You mean even in the statement of 9.6, you don't need that?

[Peter Scholze]

Well, I guess that's even how it's formulated it in the lecture notes

[Johan Commelin]

yes, I only realised it now

[Johan Commelin]

But since it's already formalized, there wasn't some unplanned "h commutes with res" either

[Peter Scholze]

Did you already fill in some of the constants?

[Johan Commelin]

In 9.6? Or in the main proof?

[Peter Scholze]

In the main proof

[Johan Commelin]

No, I haven't really fixed the constants yet.

[Johan Commelin]

I think that in the lecture notes, it's really the computations that happen in the last lines, that justify the choice of b and N.

[Peter Scholze]

To check condition (2) of 9.6, there are also some computations that are not really carried out in detail

[Peter Scholze]

I'm just asking because the only remaining possible source of error I can see is if I was screwing up something about the choice of constants

[Johan Commelin]

I haven't spent much time thinking about how to check (2) yet. But with (3) I'm quite optimistic that it will work out (even in Lean :rofl:)

[Johan Commelin]

-- this is not `iso.refl` -- so close, and yet so far away
-- the difference is `M_{(c * c_i) * N⁻¹}` vs `M_{c * (c_i * N⁻¹)}`
def complex_rescale_iso (N : ℝ≥0) :
  BD.complex (rescale_constants c' N) r V r' M c ≅
  BD.complex c' r V r' (of r' $ rescale N M) c :=
iso_of_components (λ i, sorry) sorry

[Johan Commelin]

I really wish we could tell Lean that c * c_i * N⁻¹ is defeq to itself, no matter how the parentheses are placed.

[Peter Scholze]

That seems annoying as hell

[Kevin Buzzard]

You mean you wish they were defeq? They're not, right?

[Kevin Buzzard]

but isn't there some eq_to_iso thing which sends a proof of a = b to an isomorphism between M a and M b?

[Johan Commelin]

@Kevin Buzzard certainly, but this = is burried beneath 5 layers of functors.

[Johan Commelin]

So it's still a hassle

[Johan Commelin]

And the top-most construction isn't a functor, but taking equalizers...

[Kevin Buzzard]

this is most frustrating. It's like $R[1/f][1/g]$ not being equal to $R[1/fg]$ -- but there I could understand Lean's point because they really were not equal if you thought about it carefully.

[Johan Commelin]

So it's also not functor.map_iso

[Johan Commelin]

Yes, this is even more silly than the localisation issues

[Kevin Buzzard]

It seems to me that an algorithm could do all this.

[Kevin Buzzard]

Would eq.subst take care of all this if instead of (c * c_i) * N⁻¹ and c * (c_i * N⁻¹) you had two new variables x and y and a proof that x=y?

[Kevin Buzzard]

Or is the "motive is type incorrect" issue inevitable?

[Johan Commelin]

I currently don't see an easy way to use eq.subst

[Kevin Buzzard]

import data.real.basic

variables (a b c x y : ℝ) (T : Type) (t : T) (M : ℝ → Type)
  (F : Type → Type)

example : F (M (a * (b * c))) = F (M ((a * b) * c)) :=
begin
  rw mul_assoc, -- works
end

How do I get myself into a situation where the naive approach gives me the motive is not type correct error?

[Scott Morrison]

You need dependent arguments, where rewriting in one place will cause something somewhere else to no longer type check.

[Scott Morrison]

(I need to sleep, I won't come up with an example now. :-)

[Johan Commelin]

@Mario Carneiro if you have any sort of magic tricks that can help us through get out of the sticky mud, that would be awesome

[Johan Commelin]

The defeq trouble actually goes a bit deeper, because the parentheses also disturb the Tinv map, meaning the equalizers are now no longer defeq.

[Johan Commelin]

In particular, the hom of the iso in question is not even a restriction map along an equality.

[Johan Commelin]

lemma aux₀ (c c' N : ℝ≥0) : fact (c * c' * N⁻¹ ≤ c * (c' * N⁻¹)) :=
by simpa only [mul_assoc] using nnreal.fact_le_refl _

lemma aux₀' (c c' N : ℝ≥0) : fact (r' * (c * c') * N⁻¹ ≤ r' * (c * (c' * N⁻¹))) :=
by simpa only [mul_assoc] using nnreal.fact_le_refl _

local attribute [instance] aux₀ aux₀'

def rescale_hom (c c' N : ℝ≥0) (n : ℕ) :
  CLCFPTinv r V r' M (c * (c' * N⁻¹)) n ⟶ CLCFPTinv r V r' (rescale N M) (c * c') n :=
equalizer.map (CLCFP.res V r' _ _ _) (CLCFP.res V r' _ _ _) sorry sorry

[Johan Commelin]

Now prove the sorrys, do the same for inv, show that hom and inv are inverse to each other...

[Johan Commelin]

De Bruijn factor: $\pi^{\pi^{\pi^\pi}}$

[Mario Carneiro]

It should be possible to express this using eq.rec as long as you can get the term to be type correct if you replace c * c' * N⁻¹ with an arbitrary variable a

[Mario Carneiro]

This is generally not recommended, but as long as you only rarely need to compute the action of the isomorphism it should be fine

[Mario Carneiro]

you can still prove that it commutes with other isomorphisms by casing on the equality

[Kevin Buzzard]

@Johan Commelin can you MWE this for Mario?

[Kevin Buzzard]

I'm wondering how far we can get by somehow generalizing to two variables a and b which are equal

[Johan Commelin]

Mario Carneiro said:

It should be possible to express this using eq.rec as long as you can get the term to be type correct if you replace c * c' * N⁻¹ with an arbitrary variable a

I'm afraid we can't do that... :sad:

[Kevin Buzzard]

(or can I do it somehow? I am giving a talk in 1 hour for one hour but will be free to think about this afterwards)

[Johan Commelin]

@Kevin Buzzard let's discuss after your talk!

[Johan Commelin]

I wouldn't mind talking someone through the plan for part (3) of the proof.

[Johan Commelin]

It will probably help me clear up some details

[Kevin Buzzard]

Your aux lemmas above remind me of Reid's hack when we were doing schemes: to prove that an affine scheme was a scheme we had to pull back along the identity map, and ended up needing a map $\mathcal{F}(U)\to\mathcal{F}(i(U))$ with $i$ the identity map. Trying to make this map "the identity" was horrible, but then Reid pointed out that one could just make it restriction and then everything worked gloriously.

[Johan Commelin]

Sure, it works great, but the De Bruijn factor is still ridiculous

[Mario Carneiro]

I can check out the project if you have a line and commit to point to

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/master/src/pseudo_normed_group/homotopy.lean#L119

[Johan Commelin]

Apart from pseudo_normed_group/homotopy.lean everything compiles again. So I'm commenting out homotopy.lean (nothing else depends on it yet.

[Johan Commelin]

That means we can merge rescale_iso into master, so that we have "1 source of truth" again (-;

[Johan Commelin]

 src/breen_deligne/suitable.lean                  |  16 ++--
 src/locally_constant/Vhat.lean                   |  15 ++--
 src/polyhedral_lattice/Hom.lean                  |   8 +-
 src/polyhedral_lattice/pseudo_normed_group.lean  |   5 +-
 src/pseudo_normed_group/CLC.lean                 | 244 ++++++++++++++++++++++++++++--------------------------
 src/pseudo_normed_group/FiltrationPow.lean       | 214 +++++++++++++++++++++++++++---------------------
 src/pseudo_normed_group/LC.lean                  | 390 +++++++++++++++++++++++++++++++++++++++++---------------------------------------------
 src/pseudo_normed_group/Tinv.lean                | 396 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++---------------------------
 src/pseudo_normed_group/category.lean            |  11 +++
 src/pseudo_normed_group/homotopy.lean            |  62 +++++++++++++-
 src/pseudo_normed_group/rescale.lean             |   9 +-
 src/pseudo_normed_group/system_of_complexes.lean |  84 +++++++++++--------
 src/pseudo_normed_group/with_Tinv.lean           |  69 +++++++++-------
 src/thm95/row_iso.lean                           |   4 +-

[Johan Commelin]

merged and pushed

[Johan Commelin]

After even more relentless refactoring by @Mario Carneiro we had another huge merge into master just now.

[Johan Commelin]

The upshot:

-- this is not `iso.refl` -- so close, and yet so far away
-- the difference is `M_{(c * c_i) * N⁻¹}` vs `M_{c * (c_i * N⁻¹)}`
theorem complex_rescale_eq (N : ℝ≥0) :
  (BD.complex (rescale_constants c' N) r V r' c).obj (op M) =
  (BD.complex c' r V r' c).obj (op $ of r' $ rescale N M) :=
begin
  dsimp only [data.complex, rescale_constants],
  haveI : ∀ c c', fact (c * c' * N⁻¹ ≤ c * (c' * N⁻¹)) :=
    λ c c', by simpa only [mul_assoc] using nnreal.fact_le_refl _,
  transitivity
    (BD.complex₂ r V r' (λ (i : ℕ), c * c' i * N⁻¹) (λ (i : ℕ), r' * (c * c' i) * N⁻¹)).obj (op $ of r' M),
  { simp only [mul_assoc, ProFiltPseuNormGrpWithTinv.of_coe] },
  refine cochain_complex.ext (λ i, _),
  dsimp only [data.complex₂, rescale_constants, data.complex₂_d, universal_map.eval_CLCFPTinv₂,
    _root_.id, NormedGroup.equalizer.map_nat_app],
  refine NormedGroup.equalizer.map_congr _ _ rfl rfl rfl rfl,
  { simp only [universal_map.eval_CLCFP_rescale V r' _ _ _ _ (BD.d (succ i) i) N M] },
  { simp only [universal_map.eval_CLCFP_rescale V r' _ _ _ _ (BD.d (succ i) i) N M] },
end

[Johan Commelin]

It's clear that this proof will never be iso.refl bycause of the associativity issue.
But on line 3 of the proof you can see a mul_assoc that now "just works".

[Johan Commelin]

The rest of the proof is messing around with eval_CLCFP and friends. And that's mostly because the action of f : FreeMat is defined by evaluating some formal sum of matrices. And $\phi (\sum x_i) = \sum \phi(x_i)$ is not defeq, even if $\phi (a + b) = \phi(a) + \phi(b)$ is defeq.

[Johan Commelin]

So we need to do a bit more "honest proving", and can't rfl all the way through.

[Johan Commelin]

After a lot of refactoring of Breen Deligne data, and many computations with kronecker products of matrices, I'm delighted to announce:

def homotopy_σπ :=
homotopy.{u v} (data.homotopy_mul BD.data BD.homotopy N)
  (c' * c_) (rescale_constants c_ (2^N)) r V c M

#check homotopy_σπ

#print axioms homotopy_σπ

[Johan Commelin]

-- homotopy.lean:179:0
homotopy_σπ :
  Π (BD : package) (c_ c' : ℕ → ℝ≥0) [_inst_1 : BD.data.suitable c_] [_inst_2 : package.adept BD c_ c']
  (r : ℝ≥0) (V : NormedGroup) [_inst_3 : normed_with_aut ↑r V] [_inst_4 : fact (0 < r)] {r' : ℝ≥0}
  [_inst_5 : fact (0 < r')] [_inst_6 : fact (r' ≤ 1)] (c : ℝ≥0) (M : (ProFiltPseuNormGrpWithTinv r')ᵒᵖ)
  (N : ℕ),
    differential_object.complex_like.homotopy
      ((BD_map (BD.data.sum (2 ^ N)) (c' * c_) (rescale_constants c_ (2 ^ N)) r V c).app M)
      ((BD_map (BD.data.proj (2 ^ N)) (c' * c_) (rescale_constants c_ (2 ^ N)) r V c).app M)

The axioms:

-- homotopy.lean:181:0
propext
quot.sound
classical.choice

[Kevin Buzzard]

You rescaled!

[Johan Commelin]

Most notably: this construction is now entirely sorry-free.

[Johan Commelin]

This is now almost in the shape that we need for the proof of 9.5.

[Johan Commelin]

In particular, this homotopy is in terms of BD.data.sum (2 ^ N) instead of the N-fold iteration of the addition map.

[Johan Commelin]

@Kevin Buzzard At this point, only the constants are being rescaled. But we will need to move that over to a rescaling of some pseudo normed group. This should now be relatively straight-forward, thanks to the massive refactor that Mario did a little while ago.

[Johan Commelin]

To some extent, I would say that this is now a pretty solid proof of 9.12 and 9.13 from the appendix to section 9 of Analytic.pdf. Plus epsilon for pushing the homotopy through the system_of_complexes construction.

[Johan Commelin]

This means that we can now tick of https://leanprover-community.github.io/liquid/sec-more_breen_deligne.html#basehomotopy and the lemma after it.

[Johan Commelin]

Hmm, actually, I need to rewrite that part of the blueprint, before ticking anything off. But I first need to prepare a talk for tomorrow.

[Johan Commelin]

Up to an isomorphism between two complexes, and a very nasty Lean problem that I don't understand, the homotopy section is now done.
I don't expect and (math or Lean) problems with the iso. But I didn't expect Lean problems, and now I still have one.
If some Lean hacker wants to look at https://github.com/leanprover-community/lean-liquid/blob/master/src/thm95/default.lean#L202 and https://github.com/leanprover-community/lean-liquid/blob/master/src/thm95/default.lean#L260 that would be very kind.

[Johan Commelin]

On L202 I define a lemma, which seems to be exactly what is needed on L260.

[Johan Commelin]

But on L260, the proof times out.

[Johan Commelin]

I am stretching Lean to its limits, it seems. Which probably means I'm doing something Lean-stupid.

[Johan Commelin]

@Mario Carneiro or some other Lean hacker. Could you please take a look at this?

[Mario Carneiro]

I have some free time if you want to do some hacking on this together

[Johan Commelin]

I don't have free time this afternoon CEST. We're having a small birthday party.

[Johan Commelin]

The problem is that there is a lemma foo : X := some_proof and then a declaration

def bar : some_structure :=
{ field_of_type_X := foo, -- times out
  etc }

[Johan Commelin]

Everything is done. I just need that time out to go away (-;

[Mario Carneiro]

I'm playing with it now, I'll report back if I figure anything out

[Mario Carneiro]

def NSH_aux (M) : NSH_aux_type BD r r' V c_ c' m Λ (N₂ c' r r' m) M :=
NSH_aux' BD r r' V c_ c' m Λ M $ λ c hc q hqm,
by convert NSH_hδ V c' m Λ M c hc q hqm

works

[Mario Carneiro]

even convert using 0 works

[Mario Carneiro]

but exact takes way longer

[Johan Commelin]

Ooh, I hadn't tried convert

[Johan Commelin]

Still, this is very mysterious. Maybe related to the "slow proof" discussion happening in #general right now?

[Mario Carneiro]

you can also inline that into NSH_aux' although that declaration is pushing 10 seconds

[Johan Commelin]

Yeah there is more than 1 slow decl (-;

[Johan Commelin]

I just checked, but

begin
  have := NSH_hδ V c' m Λ M c hc q hqm,
  exact this,
end

does not work. So it's probably not the same as the issue that @Sebastien Gouezel is seeing.

[Johan Commelin]

(https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/slow.20proof/near/234979594 fyi)

[Johan Commelin]

I've pushed Mario's by convert solution.

[Johan Commelin]

I feel like there is still some issue/bug that we don't really understand. But I don't know enough about Lean's internals to understand why it's being so slow here.

[Johan Commelin]

I'm excited, exhausted and relieved to announce that all the glue that still had to be written for the homotopy argument has been filled in. It wasn't even that bad in the end. But the proofs are very slow. So I'm glad we can park these away in some separate files that we hopefully will not need to touch again in the future.

[Riccardo Brasca]

Thanks for all your incredible work!!

[Peter Scholze]

Amazing work, Johan!! :+1: