Zulip Chat Archive

Stream: condensed mathematics

Topic: thm95.homotopy


view this post on Zulip Johan Commelin (Mar 24 2021 at 20:46):

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

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

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

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

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:45):

If we had some automation to help us...

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:45):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:45):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:49):

Let me see:

  • Λ\Lambda, the lattice
  • MM, the profinitely filtered pseudo normed group with action of T1T^{-1}
  • BD, a package of Breen--Deligne data (ranks + formal sums of matrices)
  • (ci)i(c'_i)_i, some constants, which can be rescaled
  • cc, an independent constant
  • VV, some normed group, on which TT acts

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:50):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:50):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:50):

Why are BD and VV moving?

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:51):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:51):

Ah

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:51):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:51):

Ah...

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:52):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:52):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:52):

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.

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:53):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:53):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:54):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:54):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:54):

That might be useful

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:54):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:55):

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?

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:56):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:56):

Do you mean condition (2) of 9.6?

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:56):

yes

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:56):

Well, you need 9.8

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:56):

Ooh, yes, of course.

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:57):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:57):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:57):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:57):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:58):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 08:59):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:59):

Sounds reasonable

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:00):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:02):

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

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

Hmm, which constants do you mean?

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:03):

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?

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:04):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:04):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:05):

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.

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:05):

right

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:05):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:05):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:05):

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.

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:06):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:07):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:07):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:10):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:10):

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

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

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.

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

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:13):

I see

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

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:16):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:16):

But I'm reluctant to do that...

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:38):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:39):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:40):

That's surprising!

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:40):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:41):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:45):

yes, I only realised it now

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:46):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:51):

Did you already fill in some of the constants?

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:52):

In 9.6? Or in the main proof?

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:52):

In the main proof

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:53):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:53):

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.

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:54):

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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:57):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:58):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:14):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:14):

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

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

That seems annoying as hell

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 10:15):

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

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 10:16):

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?

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:16):

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

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

So it's still a hassle

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:18):

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

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 10:18):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:18):

So it's also not functor.map_iso

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:18):

Yes, this is even more silly than the localisation issues

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 10:18):

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

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 10:20):

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?

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 10:21):

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

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

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

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 10:26):

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?

view this post on Zulip Scott Morrison (Mar 25 2021 at 10:27):

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

view this post on Zulip Scott Morrison (Mar 25 2021 at 10:27):

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

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

@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

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:53):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:54):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:56):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:57):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 10:57):

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

view this post on Zulip Mario Carneiro (Mar 25 2021 at 11:16):

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

view this post on Zulip Mario Carneiro (Mar 25 2021 at 11:17):

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

view this post on Zulip Mario Carneiro (Mar 25 2021 at 11:17):

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

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 11:49):

@Johan Commelin can you MWE this for Mario?

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 11:50):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 11:50):

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:

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 11:51):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 11:52):

@Kevin Buzzard let's discuss after your talk!

view this post on Zulip Johan Commelin (Mar 25 2021 at 11:53):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 11:53):

It will probably help me clear up some details

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 11:56):

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 F(U)F(i(U))\mathcal{F}(U)\to\mathcal{F}(i(U)) with ii 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.

view this post on Zulip Johan Commelin (Mar 25 2021 at 11:57):

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

view this post on Zulip Mario Carneiro (Mar 25 2021 at 12:02):

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

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

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

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

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

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

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

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

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

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

merged and pushed

view this post on Zulip Johan Commelin (Apr 06 2021 at 08:02):

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

view this post on Zulip Johan Commelin (Apr 06 2021 at 08:02):

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

view this post on Zulip Johan Commelin (Apr 06 2021 at 08:03):

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

view this post on Zulip Johan Commelin (Apr 06 2021 at 08:05):

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 ϕ(xi)=ϕ(xi)\phi (\sum x_i) = \sum \phi(x_i) is not defeq, even if ϕ(a+b)=ϕ(a)+ϕ(b)\phi (a + b) = \phi(a) + \phi(b) is defeq.

view this post on Zulip Johan Commelin (Apr 06 2021 at 08:05):

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

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

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_σπ

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

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

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 07:02):

You rescaled!

view this post on Zulip Johan Commelin (Apr 14 2021 at 07:02):

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

view this post on Zulip Johan Commelin (Apr 14 2021 at 07:02):

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

view this post on Zulip Johan Commelin (Apr 14 2021 at 07:03):

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

view this post on Zulip Johan Commelin (Apr 14 2021 at 07:04):

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

view this post on Zulip Johan Commelin (Apr 14 2021 at 07:05):

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.

view this post on Zulip Johan Commelin (Apr 14 2021 at 07:15):

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.

view this post on Zulip Johan Commelin (Apr 14 2021 at 07:31):

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.

view this post on Zulip Johan Commelin (Apr 16 2021 at 12:48):

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.

view this post on Zulip Johan Commelin (Apr 16 2021 at 12:48):

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

view this post on Zulip Johan Commelin (Apr 16 2021 at 12:48):

But on L260, the proof times out.

view this post on Zulip Johan Commelin (Apr 16 2021 at 12:49):

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

view this post on Zulip Johan Commelin (Apr 17 2021 at 11:17):

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

view this post on Zulip Mario Carneiro (Apr 17 2021 at 11:29):

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

view this post on Zulip Johan Commelin (Apr 17 2021 at 11:48):

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

view this post on Zulip Johan Commelin (Apr 17 2021 at 11:50):

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 }

view this post on Zulip Johan Commelin (Apr 17 2021 at 11:50):

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

view this post on Zulip Mario Carneiro (Apr 17 2021 at 11:50):

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

view this post on Zulip Mario Carneiro (Apr 17 2021 at 11:51):

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

view this post on Zulip Mario Carneiro (Apr 17 2021 at 11:54):

even convert using 0 works

view this post on Zulip Mario Carneiro (Apr 17 2021 at 11:54):

but exact takes way longer

view this post on Zulip Johan Commelin (Apr 17 2021 at 11:55):

Ooh, I hadn't tried convert

view this post on Zulip Johan Commelin (Apr 17 2021 at 11:55):

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

view this post on Zulip Mario Carneiro (Apr 17 2021 at 11:56):

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

view this post on Zulip Johan Commelin (Apr 17 2021 at 12:00):

Yeah there is more than 1 slow decl (-;

view this post on Zulip Johan Commelin (Apr 17 2021 at 12:27):

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.

view this post on Zulip Johan Commelin (Apr 17 2021 at 12:28):

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

view this post on Zulip Johan Commelin (Apr 17 2021 at 17:17):

I've pushed Mario's by convert solution.

view this post on Zulip Johan Commelin (Apr 17 2021 at 17:18):

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.

view this post on Zulip Johan Commelin (May 01 2021 at 19:37):

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.

view this post on Zulip Riccardo Brasca (May 01 2021 at 19:59):

Thanks for all your incredible work!!

view this post on Zulip Peter Scholze (May 01 2021 at 20:04):

Amazing work, Johan!! :+1:


Last updated: May 09 2021 at 16:20 UTC