Zulip Chat Archive

Stream: condensed mathematics

Topic: sorry count


view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 22 2021 at 15:22):

Total: 70

view this post on Zulip Johan Commelin (Mar 22 2021 at 15:23):

The 1 sorry in normed_spectral will dissolve when we have semi_normed_groups

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 22 2021 at 15:25):

The sorrys in toric/* are the territory of Damiano :smiley:

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 28 2021 at 08:29):

We are on the right track :big_smile:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 14:52):

I can do these later today

view this post on Zulip Johan Commelin (Apr 28 2021 at 14:59):

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

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 15:44):

Hmm... what is the proof of closure_saturated?

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 15:44):

I mean, the math proof

view this post on Zulip Johan Commelin (Apr 28 2021 at 16:07):

Hmm, maybe I took a wrong turn there.

view this post on Zulip Johan Commelin (Apr 28 2021 at 16:07):

I guess it is true in free groups.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 28 2021 at 16:08):

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

view this post on Zulip Johan Commelin (Apr 28 2021 at 16:08):

But it will be a bit nasty.

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 16:53):

Let me think a little bit about closure_saturated. We need it for abelian groups, right?

view this post on Zulip Johan Commelin (Apr 28 2021 at 16:55):

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

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 17:14):

Well. the definition makes sense in general :grinning:

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 17:25):

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

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 17:47):

BTW instance (Λ : Type*) [polyhedral_lattice Λ] : no_zero_smul_divisors ℤ Λ is now sorry free.

view this post on Zulip Johan Commelin (Apr 28 2021 at 17:48):

Riccardo Brasca said:

Hm... what if we take {(1,2)}Z2\{(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?

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 17:52):

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

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 17:53):

Ops. OK, forget about this

view this post on Zulip Riccardo Brasca (Apr 29 2021 at 09:18):

I think I now have a counterexample: let G=Z2G = \mathbf{Z}^2 and let S={s1,s2}S = \{s_1, s_2\}, where s1=(1,1)s_1=(1,1) and s2=(1,3)s_2=(1,3). The assumption in closure_saturated is satisfied since if k(a,b)=sik \cdot(a,b) = s_i, for i=1,2i=1,2, then ka=1ka = 1, so k=±1k = \pm 1 and (a,b)=±siS(a,b) = \pm s_i \in \langle S \rangle. Now s1+s2=(1,1)+(1,3)=(2,4)=2(1,2)Ss_1+s_2=(1,1)+(1,3)=(2,4)=2\cdot(1,2) \in \langle S \rangle. If (1,2)S(1,2) \in \langle S \rangle, then there would be x,yZx,y \in \mathbf{Z} such that (1,2)=xs1+ys2=x(1,1)+y(1,3)=(x+y,x+3y)(1,2) = x \cdot s_1 + y \cdot s_2 = x \cdot (1,1) + y \cdot (1,3) = (x+y,x+3y), so y=1xy = 1-x and 2=2x+32 = -2x + 3, that is impossible. So S\langle S \rangle is not saturated.

view this post on Zulip Johan Commelin (Apr 29 2021 at 11:24):

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

view this post on Zulip Johan Commelin (Apr 29 2021 at 11:24):

The thing we care about is L_saturated

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:15):

And sorry for taking that wrong turn...

view this post on Zulip Peter Scholze (Apr 29 2021 at 12:15):

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

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:18):

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

view this post on Zulip 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 LmL_m splits off from (Λ)m(\Lambda')^m.

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:19):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:19):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:20):

Here f is an arbitrary map ΛΛ\Lambda \to \Lambda' with saturated image.

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:21):

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

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:21):

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

view this post on Zulip Peter Scholze (Apr 29 2021 at 12:21):

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

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:21):

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

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:23):

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

view this post on Zulip 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 Λm/Lm\Lambda'^m/L_m into Λm\Lambda'^m

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:24):

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

view this post on Zulip Peter Scholze (Apr 29 2021 at 12:24):

A map gg such that ΛΛΛ\Lambda\to \Lambda'\to \Lambda is the identity

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:31):

Hmm, does this lead to a different definition of LmL_m?

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Apr 29 2021 at 12:33):

That's not what I mean; I mean that Λm/Lm\Lambda'^m/L_m should also inject into Λm\Lambda'^m. Let me see... take the map ΛmΛm\Lambda'^m\to \Lambda'^m given by (λ1,,λm)(λ1fg(λ1)+a,λ2fg(λ2)+a,,λmfg(λm)+a)(\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(λ1++λm)a=fg(\lambda_1'+\ldots+\lambda_m'). Then this vanishes on LmL_m: On LmL_m, all λi\lambda_i' come from λiΛ\lambda_i\in \Lambda, and fgfg doesn't do anything to them, so the map is (λ1,,λm)(a,,a)(\lambda_1,\ldots,\lambda_m)\mapsto (a,\ldots,a), and a=0a=0 on LmL_m. The kernel is in fact exactly LmL_m: On the kernel, all λi=fg(λi)aΛ\lambda_i'=fg(\lambda_i')-a\in \Lambda, and then a=0a=0 shows that they are in LmL_m.

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

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:34):

Thanks!

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:35):

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

view this post on Zulip Johan Commelin (Apr 29 2021 at 12:35):

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

view this post on Zulip Peter Scholze (Apr 29 2021 at 12:36):

Sounds good to me.

view this post on Zulip Kevin Buzzard (Apr 29 2021 at 12:43):

Related: at some point I will need that if Λ\Lambda is a finite free Z\Z-module of rank n+1n+1 and ϕ:ΛZ\phi:\Lambda\to\Z is non-zero then the kernel is finite free of rank nn. 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\Z-modules -- anything that involves rank basically -- for the same reason).

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 29 2021 at 13:05):

Easy to state, trivial to prove.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 29 2021 at 13:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Apr 29 2021 at 13:31):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 29 2021 at 13:37):

The splitting map circumvents that in a very nice way.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 29 2021 at 13:40):

Exactly, you only choose it once.

view this post on Zulip Johan Commelin (Apr 30 2021 at 08:14):

These sorrys are now fixed.

view this post on Zulip Johan Commelin (Apr 30 2021 at 08:15):

I'm just building locally before I push.

view this post on Zulip Johan Commelin (Apr 30 2021 at 08:22):

Pushed

view this post on Zulip Peter Scholze (Apr 30 2021 at 08:26):

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

view this post on Zulip Johan Commelin (Apr 30 2021 at 08:30):

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

view this post on Zulip Johan Commelin (Apr 30 2021 at 08:30):

And this might need Gordan again

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Apr 30 2021 at 08:31):

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

view this post on Zulip Johan Commelin (Apr 30 2021 at 08:31):

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

view this post on Zulip Peter Scholze (Apr 30 2021 at 08:31):

OK, nice

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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\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

view this post on Zulip 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