# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: progress

#### Johan Commelin (Apr 07 2021 at 19:05):

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 (Apr 07 2021 at 19:14):

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 (Apr 07 2021 at 20:26):

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

#### Peter Scholze (Apr 07 2021 at 21:10):

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 (Apr 07 2021 at 21:14):

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

#### Johan Commelin (Apr 07 2021 at 21:15):

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

#### Johan Commelin (May 01 2021 at 19:40):

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 (May 01 2021 at 19:41):

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 (May 01 2021 at 21:20):

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 (May 02 2021 at 07:41):

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 (May 02 2021 at 08:03):

@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 (May 02 2021 at 12:46):

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 (May 02 2021 at 12:50):

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 (May 02 2021 at 13:35):

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 (May 03 2021 at 01:27):

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

s and finishing up some technical part of Gordan? Or is there still some assembly to do?

#### Johan Commelin (May 03 2021 at 04:44):

@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 (May 03 2021 at 04:45):

`snakelemma`

is a remnant of the past. `weaksnakelemma`

is what we actually need and use.

#### Johan Commelin (May 03 2021 at 04:46):

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

#### Johan Commelin (May 03 2021 at 04:46):

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 (May 03 2021 at 04:53):

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

s to go! Pretty neat.

#### Johan Commelin (May 03 2021 at 04:56):

@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 (May 03 2021 at 08:33):

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 (May 03 2021 at 08:41):

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!

Last updated: May 09 2021 at 16:20 UTC