progress

Stream: condensed mathematics

[Johan Commelin]

We've been closing a couple of todos/issues: https://github.com/leanprover-community/lean-liquid/projects/1
Most notably the semi_normed refactor by @Riccardo Brasca, but also Lemma 9.7, recently by @Filippo A. E. Nuccio.
It feels really good that the right hand list contains more items than the two columns left of it.

[Riccardo Brasca]

It was a pleasure, and let me stress that as usual nothing would have been possible without Johan's coordination of the project.

In any case I have even learnt some math! Do you know that the quotient of a semi_normed_group by a closed subspace is always a normed_group? The proof is easy (I mean, it is literally the same as for quotients of normed groups), but I find the result quite counter-intuitive.

[Kevin Buzzard]

A topological group is Hausdorff iff points are closed iff {e} is closed.

[Peter Scholze]

Congratulations on the progress you are making! It's great to see that the rest of the way towards 9.4 is cut down into nice "little" pieces. (Aside: The GitHub color-coding seems really counterintuitive. Green is for to-do's, Red is for things completed?)

[Johan Commelin]

Yes, I agree that the colors are a bit weird.

[Johan Commelin]

It comes from green = open issue, red = closed issue. I don't know if that helps :rofl:

[Johan Commelin]

The homotopy argument is now completely done. So what is left:

• Gordan's lemma. Kevin and Eric have been making good progress towards this.
• Polyhedral lattice quotients:
  • show that polyhedral lattices have the discrete topology, so that quotients are normed groups (this probably also needs Gordan)
  • show that the quotients have a polyhedral norm
• The col_exact part of the proof of thm 9.5. Adam has done an enormous amount of work to setup all the Cech machinery. It looks like we are getting into good shape for the attack on this part of the proof.

[Johan Commelin]

I think that I will spend the beginning of next week with resyncing the blueprint. It will need quite some heavy editing to reflect everything that has happened in the homotopy part that is now finished.

[Kevin Buzzard]

One thing you could do with the blueprint is to drop in the Gordan sketch If you like, but actually it's just essentially the Wikipedia proof with @Damiano Testa 's inductive argument replacing the projection claim that nobody could figure out

[Patrick Massot]

What is the status of 9.2? I started working on the first step one week ago but was stopped by Adam who wanted to do it his way. Is is now done? Where? Should I still work on the remaining of the proof?

[Patrick Massot]

@Adam Topaz and @Heather Macbeth, could you tell what are your current plans regarding this Proposition 9.2 (8.5 in the blueprint)? What part did you prove and what do you intend to work on (soon)?

[Adam Topaz]

Patrick Massot said:

What is the status of 9.2? I started working on the first step one week ago but was stopped by Adam who wanted to do it his way. Is is now done? Where? Should I still work on the remaining of the proof?

There must have been some miscommunication here.... I wasn't intending on working 9.2 (in the near future). All I was saying is that the argument with clopen covers that Peter sketched in zulip has some parts that were similar to what I was doing with representing profinite sets as limits of finite sets. And if anything, this is only useful for the very first part of 9.2 where you extend locally constant function along a closed embedding.

[Adam Topaz]

The stuff related to discrete quotients is now in mathlib docs#discrete_quotient btw, but even if it's not used for 9.2, I don't think it matters at the end.

[Adam Topaz]

FWIW, with this definition of a discrete quotient, proving that any locally constant map $f : X \to Y$ factors through a discrete quotient is easy, as you can take the relation to be \lambda a b, f a = f b.

[David Michael Roberts]

Can someone tell me how I should read the progress marked on the dependency graph, with respect to the overall goal of the LTE of proving the main theorem? As it currently stands, the graph doesn't generate a category with a terminal object, which is what one might expect. There are also theorems that don't seem to be used anywhere, for instance snakelemma. Of course, if the actual statement that is the main goal is not yet in the project, then this might be expected.

But, more generally, what's a human-level explanation of where things are at? (Given the TeX blueprint needs updating, apparently, and things are getting down and dirty in the depths of the Gordan lemma material). Is the main theorem proved, modulo some minor sorrys and finishing up some technical part of Gordan? Or is there still some assembly to do?

[Johan Commelin]

@David Michael Roberts I plan on updating the blueprint today and tomorrow. The first target is first_target which is one of the bottom nodes in the dependency graph. It is maybe a bit deceptive that it is already colored green, but that is because the proof explicit => first_target is done already in Lean. So what really needs doing is explicit, which is what corresponds to Thm 9.5 in Analytic.pdf.

[Johan Commelin]

snakelemma is a remnant of the past. weaksnakelemma is what we actually need and use.

[Johan Commelin]

It's not yet clear to me what to do with these lemmas that use "strong bounded exactness".

[Johan Commelin]

I'm inclined to remove them, since they are not on the critical path. But maybe others think there is value in keeping them around.

[David Michael Roberts]

Oh, I see. So the three nodes on the right of the graph are all old bits that aren't used. Cool, thanks! I guess we only have 32 (or possibly slightly fewer) sorrys to go! Pretty neat.

[Johan Commelin]

@David Michael Roberts Here's a grep for sorry in the codebase:

1       src/thm95/default.lean
10      src/thm95/constants.lean
1       src/locally_constant/NormedGroup.lean
3       src/polyhedral_lattice/basic.lean
2       src/polyhedral_lattice/cech.lean
2       src/for_mathlib/dfinsupp.lean
1       src/for_mathlib/Gordan.lean
8       src/for_mathlib/grading_monoid_algebra.lean
3       src/for_mathlib/int_grading_lemma.lean
Total:  31

[Peter Scholze]

Those fiddly constants are indeed my remaining (small) worry. The parts where these constants enter in tricky ways are 9.6 and the homotopy part of the proof of 9.5, and these have been done (and even if the constants haven't been finalized even for those parts, it is easy to see from the code that this poses no problems). So yes, it definitely looks firmer now, but as you say it ain't over till it's over.

[Peter Scholze]

By the way, there's a purely mathematical question asked in Analytic.pdf, namely Question 9.9 about the growth of certain constants in the proof. Once the first target 9.4 is complete, we will have a Lean-certified answer to this!