# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: sorry count

#### Johan Commelin (Mar 22 2021 at 15:21):

```
$ rg -l sorry | xargs -I % sh -c 'nsorry=`rg sorry % | wc -l`; echo -n "$nsorry\t%\n"'
1 src/normed_spectral.lean
3 src/lem97.lean
9 src/thm95/default.lean
15 src/thm95/constants.lean
5 src/thm95/double_complex.lean
3 src/toric/scarti_commentati.lean
5 src/toric/dual_extremal_API_sorry.lean
10 src/pseudo_normed_group/profinitely_filtered.lean
15 src/toric/toric.lean
4 src/polyhedral_lattice/cech.lean
```

#### Johan Commelin (Mar 22 2021 at 15:22):

Total: 70

#### Johan Commelin (Mar 22 2021 at 15:23):

The 1 sorry in `normed_spectral`

will dissolve when we have `semi_normed_group`

s

#### Johan Commelin (Mar 22 2021 at 15:23):

The `15`

sorrys in `thm95/constants`

will be fixed along the way, when we figure out the exact way the constants are increased during the proof of 9.5

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

The `10`

sorrys in `pseudo_normed_group/profinitely_filtered`

are setting up products of profinitely filtered pseudo normed groups. If you enjoy showing that a space `(X^n)_c`

is comp Haus tot disc because it is canonically isomorphic to `(X_c)^n`

(where the claim is obvious), then feel free to kill these sorrys.

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

The sorrys in `toric/*`

are the territory of Damiano :smiley:

#### Johan Commelin (Mar 22 2021 at 15:26):

The sorrys in `polyhedral_lattice/cech`

are tricky. We need to show that a certain quotient group is free abelian.

#### Damiano Testa (Mar 22 2021 at 15:56):

As for the `sorry`

s that I own, I am not as good as "others", so not all are actually needed/useful and not everything that I would like is sorried, so the count there is somewhat inaccurate. However, now that the teaching term is over, I should have some time to clean up and make some progress!

#### Riccardo Brasca (Mar 22 2021 at 17:20):

When #6819 will be merged I can start the refactoring of`for_mathlib/normed_group_quotient`

to add quotient by non closed subspace.

#### Johan Commelin (Apr 28 2021 at 08:29):

I think that two or three weeks ago we have > 70 sorry's in the repo. Now it's 47 :tada:

```
2 src/thm95/row_iso.lean
11 src/thm95/polyhedral_iso.lean
3 src/thm95/default.lean
1 src/thm95/double_complex.lean
1 src/locally_constant/NormedGroup.lean
4 src/pseudo_normed_group/profinitely_filtered.lean
3 src/polyhedral_lattice/basic.lean
4 src/polyhedral_lattice/cech.lean
2 src/for_mathlib/dfinsupp.lean
1 src/for_mathlib/Gordan.lean
5 src/for_mathlib/int_grading_lemma.lean
10 src/thm95/constants.lean
```

#### Johan Commelin (Apr 28 2021 at 08:29):

We are on the right track :big_smile:

#### Johan Commelin (Apr 28 2021 at 14:42):

Advertising some `sorry`

s:

```
-- src/polyhedral_lattice/basic.lean
instance (Λ : Type*) [polyhedral_lattice Λ] : no_zero_smul_divisors ℤ Λ :=
sorry
```

#### Johan Commelin (Apr 28 2021 at 14:42):

and

```
-- src/polyhedral_lattice/cech.lean
@[to_additive]
def saturated (H : subgroup G) : Prop := ∀ ⦃n g⦄, gpow n g ∈ H → n = 0 ∨ g ∈ H
@[to_additive]
lemma closure_saturated (s : set G) (H : ∀ n g, gpow n g ∈ s → n = 0 ∨ g ∈ closure s) :
(closure s).saturated :=
begin
intros n g h,
rw or_iff_not_imp_left,
intro hn,
sorry
end
```

#### Johan Commelin (Apr 28 2021 at 14:42):

In `src/polyhedral_lattice/cech.lean`

there is another lemma about proving that a specific subgroup is saturated. I've stubbed out a proof, but there are still some sub-`sorry`

s

#### Riccardo Brasca (Apr 28 2021 at 14:52):

I can do these later today

#### Johan Commelin (Apr 28 2021 at 14:59):

They are mostly math-trivial. But several of them are quite fiddly, I think.

#### Riccardo Brasca (Apr 28 2021 at 15:44):

Hmm... what is the proof of `closure_saturated`

?

#### Riccardo Brasca (Apr 28 2021 at 15:44):

I mean, the math proof

#### Johan Commelin (Apr 28 2021 at 16:07):

Hmm, maybe I took a wrong turn there.

#### Johan Commelin (Apr 28 2021 at 16:07):

I guess it is true in free groups.

#### Johan Commelin (Apr 28 2021 at 16:07):

But maybe we should just not think about that, and try to find a different proof for `L_saturated`

#### Johan Commelin (Apr 28 2021 at 16:08):

I think we can write down an explicit basis of `L f m`

.

#### Johan Commelin (Apr 28 2021 at 16:08):

But it will be a bit nasty.

#### Johan Commelin (Apr 28 2021 at 16:09):

And then we have to show that you can extend that basis to a basis of the full group. So that `L f m`

splits off.

#### Riccardo Brasca (Apr 28 2021 at 16:53):

Let me think a little bit about `closure_saturated`

. We need it for abelian groups, right?

#### Johan Commelin (Apr 28 2021 at 16:55):

Oh did I forget the commutativity assumption?? :face_palm:

#### Riccardo Brasca (Apr 28 2021 at 17:14):

Well. the definition makes sense in general :grinning:

#### Riccardo Brasca (Apr 28 2021 at 17:25):

Hm... what if we take $\{(1,2)\} \subseteq \mathbf{Z}^2$? The condition seems satisfied, but the generated subgroup is not saturated.

#### Riccardo Brasca (Apr 28 2021 at 17:47):

BTW `instance (Λ : Type*) [polyhedral_lattice Λ] : no_zero_smul_divisors ℤ Λ`

is now sorry free.

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

Riccardo Brasca said:

Hm... what if we take $\{(1,2)\} \subseteq \mathbf{Z}^2$? The condition seems satisfied, but the generated subgroup is not saturated.

I think the subgroup generated by `(1,2)`

will be saturated, right?

#### Riccardo Brasca (Apr 28 2021 at 17:52):

~~$2\cdot (1,1)$ is in the subgroup but $(1,1)$ is not~~. Saturated means that the quotient is torsion-free (if I didn't misunderstood everything).

#### Riccardo Brasca (Apr 28 2021 at 17:53):

Ops. OK, forget about this

#### Riccardo Brasca (Apr 29 2021 at 09:18):

I think I now have a counterexample: let $G = \mathbf{Z}^2$ and let $S = \{s_1, s_2\}$, where $s_1=(1,1)$ and $s_2=(1,3)$. The assumption in `closure_saturated`

is satisfied since if $k \cdot(a,b) = s_i$, for $i=1,2$, then $ka = 1$, so $k = \pm 1$ and $(a,b) = \pm s_i \in \langle S \rangle$. Now $s_1+s_2=(1,1)+(1,3)=(2,4)=2\cdot(1,2) \in \langle S \rangle$. If $(1,2) \in \langle S \rangle$, then there would be $x,y \in \mathbf{Z}$ such that $(1,2) = x \cdot s_1 + y \cdot s_2 = x \cdot (1,1) + y \cdot (1,3) = (x+y,x+3y)$, so $y = 1-x$ and $2 = -2x + 3$, that is impossible. So $\langle S \rangle$ is not saturated.

#### Johan Commelin (Apr 29 2021 at 11:24):

@Riccardo Brasca Hmm, good example. So we can throw that lemma away.

#### Johan Commelin (Apr 29 2021 at 11:24):

The thing we care about is `L_saturated`

#### Johan Commelin (Apr 29 2021 at 12:15):

@Riccardo Brasca Do you have an idea how to attack `L_saturated`

? Otherwise I'll start thinking about it.

#### Johan Commelin (Apr 29 2021 at 12:15):

And sorry for taking that wrong turn...

#### Peter Scholze (Apr 29 2021 at 12:15):

Can you remind me of the precise statement you need here?

#### Johan Commelin (Apr 29 2021 at 12:18):

We have $\Lambda^{(m)} := (\Lambda')^m / L_m$, and to prove that this if finite free, we need to show that $L_m$ is saturated.

#### Johan Commelin (Apr 29 2021 at 12:18):

So, I think you said some time in the past that it might be best to show that $L_m$ splits off from $(\Lambda')^m$.

#### Johan Commelin (Apr 29 2021 at 12:19):

But now we need to figure out how to execute that in practice.

#### Riccardo Brasca (Apr 29 2021 at 12:19):

To be honest I forgot what `L f m`

means :sweat_smile: I tried the other lemma since it didn't use complicated objects... but let me have a look at it

#### Johan Commelin (Apr 29 2021 at 12:19):

Ooh, no worries. I can also look at this one.

#### Johan Commelin (Apr 29 2021 at 12:19):

In Lean

```
def Lset : set (fin m →₀ Λ') :=
{x | ∃ (l : Λ) (n : fin m →₀ ℤ) (hn : n.sum (λ _, add_monoid_hom.id _) = 0),
x = finsupp.map_range_hom (int.cast_add_hom' (f l)) n}
def L : add_subgroup (fin m →₀ Λ') := add_subgroup.closure $ Lset f m
```

#### Johan Commelin (Apr 29 2021 at 12:20):

Here `f`

is an arbitrary map $\Lambda \to \Lambda'$ with saturated image.

#### Johan Commelin (Apr 29 2021 at 12:21):

We can't really write $L_m := (\Lambda \otimes \Z^m)_{\Sigma = 0}$

#### Johan Commelin (Apr 29 2021 at 12:21):

That would require internal tensor products of submodules (additive subgroups actually, in this Lean code).

#### Peter Scholze (Apr 29 2021 at 12:21):

How hard is it to prove that the map $\Lambda\to \Lambda'$ splits (as abelian groups)?

#### Johan Commelin (Apr 29 2021 at 12:21):

We don't have that yet, so I gave a hands on definition of `Lset`

.

#### Johan Commelin (Apr 29 2021 at 12:23):

In the actual application, where $\Lambda' = \Lambda^N$, it shouldn't be hard. So here we can just assume it.

#### Peter Scholze (Apr 29 2021 at 12:23):

I would have thought that knowing this splitting should make the desired result quite easy, as one would get an explicit splitting of $\Lambda'^m/L_m$ into $\Lambda'^m$

#### Johan Commelin (Apr 29 2021 at 12:24):

With splitting, you just mean a map $g : \Lambda' \to \Lambda$, right? Or a direct sum decomposition?

#### Peter Scholze (Apr 29 2021 at 12:24):

A map $g$ such that $\Lambda\to \Lambda'\to \Lambda$ is the identity

#### Johan Commelin (Apr 29 2021 at 12:25):

Right. I agree that if we have such a map, then showing that the range of `f`

is saturated shouldn't be Lean-hard.

#### Johan Commelin (Apr 29 2021 at 12:31):

Hmm, does this lead to a different definition of $L_m$?

#### Johan Commelin (Apr 29 2021 at 12:31):

I wouldn't mind swapping out the current definition. It's not that pleasant to work with.

#### Peter Scholze (Apr 29 2021 at 12:33):

That's not what I mean; I mean that $\Lambda'^m/L_m$ should also inject into $\Lambda'^m$. Let me see... take the map $\Lambda'^m\to \Lambda'^m$ given by $(\lambda_1',\ldots,\lambda_m')\mapsto (\lambda_1'-fg(\lambda_1')+a,\lambda_2'-fg(\lambda_2')+a,\ldots,\lambda_m'-fg(\lambda_m')+a)$ where $a=fg(\lambda_1'+\ldots+\lambda_m')$. Then this vanishes on $L_m$: On $L_m$, all $\lambda_i'$ come from $\lambda_i\in \Lambda$, and $fg$ doesn't do anything to them, so the map is $(\lambda_1,\ldots,\lambda_m)\mapsto (a,\ldots,a)$, and $a=0$ on $L_m$. The kernel is in fact exactly $L_m$: On the kernel, all $\lambda_i'=fg(\lambda_i')-a\in \Lambda$, and then $a=0$ shows that they are in $L_m$.

So indeed $\Lambda'^m/L_m$ injects into $\Lambda'^m$ and hence is torsion-free.

#### Johan Commelin (Apr 29 2021 at 12:34):

Thanks!

#### Johan Commelin (Apr 29 2021 at 12:35):

So one *could* define $L_m$ to be that kernel. But it's not clear to me that this will make the "Cech" part of the construction easier.

#### Johan Commelin (Apr 29 2021 at 12:35):

So maybe we should stick to the current definition for now, and formalize your argument.

#### Peter Scholze (Apr 29 2021 at 12:36):

Sounds good to me.

#### Kevin Buzzard (Apr 29 2021 at 12:43):

Related: at some point I will need that if $\Lambda$ is a finite free $\Z$-module of rank $n+1$ and $\phi:\Lambda\to\Z$ is non-zero then the kernel is finite free of rank $n$. I've been putting this off because I am dimly aware that Anne is refactoring `is_basis`

(in fact I've also been putting off a ton of completely trivial things about finite free $\Z$-modules -- anything that involves rank basically -- for the same reason).

#### Johan Commelin (Apr 29 2021 at 13:05):

So this is the correct lemma, instead of that `closure_saturated`

:

```
lemma add_subgroup.ker_saturated [no_zero_smul_divisors ℤ G₂] (f : G₁ →+ G₂) :
(f.ker).saturated :=
begin
intros n g hg,
simpa only [f.mem_ker, gsmul_eq_smul, f.map_gsmul, smul_eq_zero] using hg
end
```

#### Johan Commelin (Apr 29 2021 at 13:05):

Easy to state, trivial to prove.

#### Johan Commelin (Apr 29 2021 at 13:09):

So, now we have:

```
lemma L_saturated
[hf : fact (∃ f' : polyhedral_lattice_hom Λ' Λ, (f'.comp f) = polyhedral_lattice_hom.id)] :
(L f m).saturated :=
begin
unfreezingI { obtain ⟨f', h⟩ := hf },
rw ← finite_free.claim f f' m h,
apply add_subgroup.ker_saturated
end
```

#### Johan Commelin (Apr 29 2021 at 13:10):

What is left is to fill in this sorry:

```
namespace finite_free
-- move this, better names?
def Δ : Λ' →+ (fin m →₀ Λ') :=
add_monoid_hom.mk' (λ l, ∑ i, finsupp.single_add_hom i l) $
λ l₁ l₂, by simp only [add_monoid_hom.map_add, finset.sum_add_distrib]
def σ : (fin m →₀ Λ') →+ Λ' :=
add_monoid_hom.mk' (λ l, l.sum (λ _, add_monoid_hom.id _)) $
λ l₁ l₂, finsupp.sum_add_index' _
def a : (fin m →₀ Λ') →+ Λ' :=
add_monoid_hom.comp (f.comp f').to_add_monoid_hom (σ m)
def φ : (fin m →₀ Λ') →+ (fin m →₀ Λ') :=
(finsupp.map_range_hom $ add_monoid_hom.id _ - (f.comp f').to_add_monoid_hom) +
((Δ m).comp (a f f' m))
lemma claim (h : (f'.comp f) = polyhedral_lattice_hom.id) : (φ f f' m).ker = L f m :=
begin
sorry
end
end finite_free
```

#### Johan Commelin (Apr 29 2021 at 13:28):

Hmm, I actually think that defining $L_m$ to be that kernel is not so bad.

#### Johan Commelin (Apr 29 2021 at 13:29):

You need to prove that this kernel plays will with morphisms from the simplex category. But that seems to be a straightforward calculation, so far.

#### Johan Commelin (Apr 29 2021 at 13:30):

Whereas working with the additive subgroup closure of

```
{x | ∃ (l : Λ) (n : fin m →₀ ℤ) (hn : n.sum (λ _, add_monoid_hom.id _) = 0),
x = finsupp.map_range_hom (int.cast_add_hom' (f l)) n}
```

is just painful.

#### Peter Scholze (Apr 29 2021 at 13:31):

Why not define it as the set of elements of $\Lambda'^m$ all of whose coordinates are in $\Lambda$, and sum to $0$? That's very close to the kernel of this map, but seems a bit easier to manipulate still.

#### Johan Commelin (Apr 29 2021 at 13:37):

Asking that the coordinates are in $\Lambda$ introduces an existential. Which means that you constantly have to choose witnesses.

#### Johan Commelin (Apr 29 2021 at 13:37):

The splitting map circumvents that in a very nice way.

#### Peter Scholze (Apr 29 2021 at 13:38):

Aha! But the splitting map in itself is a choice... but maybe it doesn't matter so much if you just make this choice globally

#### Johan Commelin (Apr 29 2021 at 13:40):

Exactly, you only choose it once.

#### Johan Commelin (Apr 30 2021 at 08:14):

These sorrys are now fixed.

#### Johan Commelin (Apr 30 2021 at 08:15):

I'm just building locally before I push.

#### Johan Commelin (Apr 30 2021 at 08:22):

Pushed

#### Peter Scholze (Apr 30 2021 at 08:26):

So this takes care of the polyhedral lattice - Cech nerve?

#### Johan Commelin (Apr 30 2021 at 08:30):

Well, we still need to check that the quotients are polyhedral

#### Johan Commelin (Apr 30 2021 at 08:30):

And this might need Gordan again

#### Johan Commelin (Apr 30 2021 at 08:31):

We need to write down generators for the norm, and we need to show that the quotient is a normed group.

#### Peter Scholze (Apr 30 2021 at 08:31):

But can you already verify that it is a Cech nerve?

#### Johan Commelin (Apr 30 2021 at 08:31):

(At the moment it's only semi-normed.)

#### Peter Scholze (Apr 30 2021 at 08:31):

OK, nice

#### Johan Commelin (Apr 30 2021 at 08:32):

Right, we have the Cech construction. But it's a bit ad hoc, and needs to be glued to the general theory that Adam developed.

#### Johan Commelin (Apr 30 2021 at 09:58):

Current sorry count:

```
1 src/thm95/default.lean
1 src/thm95/row_iso.lean
10 src/thm95/constants.lean
1 src/locally_constant/NormedGroup.lean
3 src/polyhedral_lattice/basic.lean
4 src/pseudo_normed_group/profinitely_filtered.lean
2 src/polyhedral_lattice/cech.lean
2 src/for_mathlib/dfinsupp.lean
1 src/for_mathlib/Gordan.lean
3 src/for_mathlib/int_grading_lemma.lean
8 src/for_mathlib/grading_monoid_algebra.lean
4 src/thm95/polyhedral_iso.lean
Total: 40
```

#### Johan Commelin (Apr 30 2021 at 15:24):

```
1 src/thm95/default.lean
1 src/thm95/row_iso.lean
1 src/locally_constant/NormedGroup.lean
10 src/thm95/constants.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: 32
```

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

The list of files is getting shorter:

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

#### Kevin Buzzard (May 01 2021 at 21:19):

Those last four files are a work in progress. I've stated Gordan and yesterday I also managed to state the intermediate commutative algebra lemma about $\Z$-graded rings, so things are going in the right direction. It's a long weekend in the UK and I'm away from my home and unlikely to do much, but on the other hand @Eric Wieser has filled in a couple of sorries in a DM so the true total is lower

#### Kevin Buzzard (May 01 2021 at 23:40):

`src/for_mathlib/dfinsupp.lean`

is now sorry-free thanks to Eric's #7311

Last updated: May 09 2021 at 23:10 UTC