# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: thm95.homotopy

#### 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 `sorry`

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

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

#### Johan Commelin (Mar 25 2021 at 08:45):

If we had some automation to help us...

#### Johan Commelin (Mar 25 2021 at 08:45):

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

#### Peter Scholze (Mar 25 2021 at 08:45):

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

#### Johan Commelin (Mar 25 2021 at 08:49):

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 (Mar 25 2021 at 08:50):

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

#### Johan Commelin (Mar 25 2021 at 08:50):

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

#### Peter Scholze (Mar 25 2021 at 08:50):

Why are `BD`

and $V$ moving?

#### Johan Commelin (Mar 25 2021 at 08:51):

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

#### Peter Scholze (Mar 25 2021 at 08:51):

Ah

#### Johan Commelin (Mar 25 2021 at 08:51):

`BD`

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

#### Peter Scholze (Mar 25 2021 at 08:51):

Ah...

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

#### Johan Commelin (Mar 25 2021 at 08:52):

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

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

#### Peter Scholze (Mar 25 2021 at 08:53):

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

#### Johan Commelin (Mar 25 2021 at 08:53):

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

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

#### Johan Commelin (Mar 25 2021 at 08:54):

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 (Mar 25 2021 at 08:54):

That might be useful

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

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

#### 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 $\mathrm{Hom}(\_, M)$

#### Peter Scholze (Mar 25 2021 at 08:56):

Do you mean condition (2) of 9.6?

#### Johan Commelin (Mar 25 2021 at 08:56):

yes

#### Peter Scholze (Mar 25 2021 at 08:56):

Well, you need 9.8

#### Johan Commelin (Mar 25 2021 at 08:56):

Ooh, yes, of course.

#### 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 $N$ large enough

#### Peter Scholze (Mar 25 2021 at 08:57):

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

#### Johan Commelin (Mar 25 2021 at 08:57):

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

#### Peter Scholze (Mar 25 2021 at 08:57):

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

#### Johan Commelin (Mar 25 2021 at 08:58):

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

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

#### Peter Scholze (Mar 25 2021 at 08:59):

Sounds reasonable

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

#### Peter Scholze (Mar 25 2021 at 09:02):

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

#### Johan Commelin (Mar 25 2021 at 09:03):

Hmm, which constants do you mean?

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

#### Peter Scholze (Mar 25 2021 at 09:04):

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

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

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

#### Peter Scholze (Mar 25 2021 at 09:05):

right

#### Johan Commelin (Mar 25 2021 at 09:05):

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

#### Peter Scholze (Mar 25 2021 at 09:05):

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

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

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

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

#### Johan Commelin (Mar 25 2021 at 09:07):

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

#### Peter Scholze (Mar 25 2021 at 09:10):

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 (Mar 25 2021 at 09:10):

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

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

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

#### Peter Scholze (Mar 25 2021 at 09:13):

I see

#### Johan Commelin (Mar 25 2021 at 09:15):

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

#### Johan Commelin (Mar 25 2021 at 09:16):

We could factor the construction through a category `NormedGroup_with_two_Tinv_actions`

...

#### Johan Commelin (Mar 25 2021 at 09:16):

But I'm reluctant to do that...

#### Johan Commelin (Mar 25 2021 at 09:38):

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

#### Johan Commelin (Mar 25 2021 at 09:39):

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

#### Peter Scholze (Mar 25 2021 at 09:40):

That's surprising!

#### Peter Scholze (Mar 25 2021 at 09:40):

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

#### Peter Scholze (Mar 25 2021 at 09:41):

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

#### Johan Commelin (Mar 25 2021 at 09:45):

yes, I only realised it now

#### Johan Commelin (Mar 25 2021 at 09:46):

But since it's already formalized, there wasn't some unplanned "`h`

commutes with `res`

" either

#### Peter Scholze (Mar 25 2021 at 09:51):

Did you already fill in some of the constants?

#### Johan Commelin (Mar 25 2021 at 09:52):

In 9.6? Or in the main proof?

#### Peter Scholze (Mar 25 2021 at 09:52):

In the main proof

#### Johan Commelin (Mar 25 2021 at 09:53):

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

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

.

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

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

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

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

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

#### Peter Scholze (Mar 25 2021 at 10:15):

That seems annoying as hell

#### Kevin Buzzard (Mar 25 2021 at 10:15):

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

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

?

#### Johan Commelin (Mar 25 2021 at 10:16):

@Kevin Buzzard certainly, but this `=`

is burried beneath 5 layers of functors.

#### Johan Commelin (Mar 25 2021 at 10:17):

So it's still a hassle

#### Johan Commelin (Mar 25 2021 at 10:18):

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

#### Kevin Buzzard (Mar 25 2021 at 10:18):

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 (Mar 25 2021 at 10:18):

So it's also not `functor.map_iso`

#### Johan Commelin (Mar 25 2021 at 10:18):

Yes, this is even more silly than the localisation issues

#### Kevin Buzzard (Mar 25 2021 at 10:18):

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

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

?

#### Kevin Buzzard (Mar 25 2021 at 10:21):

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

#### Johan Commelin (Mar 25 2021 at 10:25):

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

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

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

#### Scott Morrison (Mar 25 2021 at 10:27):

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

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

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

#### Johan Commelin (Mar 25 2021 at 10:54):

In particular, the `hom`

of the iso in question is not even a `res`

triction map along an equality.

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

#### Johan Commelin (Mar 25 2021 at 10:57):

Now prove the `sorry`

s, do the same for `inv`

, show that `hom`

and `inv`

are inverse to each other...

#### Johan Commelin (Mar 25 2021 at 10:57):

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

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

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

#### Mario Carneiro (Mar 25 2021 at 11:17):

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

#### Kevin Buzzard (Mar 25 2021 at 11:49):

@Johan Commelin can you MWE this for Mario?

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

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

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

#### Johan Commelin (Mar 25 2021 at 11:52):

@Kevin Buzzard let's discuss after your talk!

#### Johan Commelin (Mar 25 2021 at 11:53):

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

#### Johan Commelin (Mar 25 2021 at 11:53):

It will probably help me clear up some details

#### 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 $\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 (Mar 25 2021 at 11:57):

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

#### Mario Carneiro (Mar 25 2021 at 12:02):

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

#### Johan Commelin (Mar 25 2021 at 12:06):

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

#### 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 (-;

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

#### Johan Commelin (Mar 30 2021 at 14:56):

merged and pushed

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

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

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

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

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

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

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

#### Kevin Buzzard (Apr 14 2021 at 07:02):

You rescaled!

#### Johan Commelin (Apr 14 2021 at 07:02):

Most notably: this construction is now entirely `sorry`

-free.

#### Johan Commelin (Apr 14 2021 at 07:02):

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

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

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

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

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

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

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

#### Johan Commelin (Apr 16 2021 at 12:48):

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

#### Johan Commelin (Apr 16 2021 at 12:48):

But on L260, the proof times out.

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

#### Johan Commelin (Apr 17 2021 at 11:17):

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

#### Mario Carneiro (Apr 17 2021 at 11:29):

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

#### Johan Commelin (Apr 17 2021 at 11:48):

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

#### 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 }
```

#### Johan Commelin (Apr 17 2021 at 11:50):

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

#### Mario Carneiro (Apr 17 2021 at 11:50):

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

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

#### Mario Carneiro (Apr 17 2021 at 11:54):

even `convert using 0`

works

#### Mario Carneiro (Apr 17 2021 at 11:54):

but `exact`

takes way longer

#### Johan Commelin (Apr 17 2021 at 11:55):

Ooh, I hadn't tried `convert`

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

#### Mario Carneiro (Apr 17 2021 at 11:56):

you can also inline that into `NSH_aux'`

although that declaration is pushing 10 seconds

#### Johan Commelin (Apr 17 2021 at 12:00):

Yeah there is more than 1 slow decl (-;

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

#### Johan Commelin (Apr 17 2021 at 12:28):

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

#### Johan Commelin (Apr 17 2021 at 17:17):

I've pushed Mario's `by convert`

solution.

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

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

#### Riccardo Brasca (May 01 2021 at 19:59):

Thanks for all your incredible work!!

#### Peter Scholze (May 01 2021 at 20:04):

Amazing work, Johan!! :+1:

Last updated: May 09 2021 at 16:20 UTC