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


Total: 70

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

The 1 sorry in normed_spectral will dissolve when we have semi_normed_groups

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

-- 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
def saturated (H : subgroup G) : Prop := ∀ ⦃n g⦄, gpow n g ∈ H → n = 0 ∨ g ∈ H

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

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

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.

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

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

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
src/for_mathlib/dfinsupp.lean is now sorry-free thanks to Eric's #7311