Zulip Chat Archive

Stream: condensed mathematics

Topic: lemma 9.7


view this post on Zulip Johan Commelin (Jan 20 2021 at 20:47):

I pushed a statement of lemma 9.7. I characterise "finite free abelian group" as "fin.gen. and torsion free". As far as I can see, that should work for the proof.

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:47):

If someone want to take a shot at this sorry, go ahead.

view this post on Zulip Filippo A. E. Nuccio (Jan 22 2021 at 11:23):

I have begun looking at Lemma 9.7 and it really seems feasable. I will try to work on this from next week, but I feel that (at least if one follows the proof in the paper), we need a structure theorem for finite abelian groups to characterize Λ\Lambda. I think this is OK as part of our project on Dedekind domains where I think we have the structure theorem for f.g. modules over PID.

view this post on Zulip Filippo A. E. Nuccio (Jan 22 2021 at 11:24):

I also think that there is a small typo on line 3 of the proof in the manuscript, Λ+\Lambda^{\vee}_+ should be a submodule of Λ\Lambda^{\vee}, not of Λ\Lambda.

view this post on Zulip Peter Scholze (Jan 22 2021 at 11:55):

Thanks for catching the typo! By the way, as suggested by Johan Commelin, there is now a git repository with the source code https://github.com/PeterScholze/Analytic , so you can make pull requests for typos. It should also help with version control, as I often update the version on my webpage. (I will now make sure it is synced with the version on github.)

view this post on Zulip Johan Commelin (Jan 22 2021 at 12:12):

@Filippo A. E. Nuccio I haven't thought hard about the ingredients yet. But if you already have the structure theorem, that's great!

view this post on Zulip Filippo A. E. Nuccio (Jan 22 2021 at 15:09):

Unfortunately I have to take it back! I thought that it had been implemented, but it turns out it is not the case... Never mind, I will try to figure out if it is really needed and will keep you posted.

view this post on Zulip Johan Commelin (Jan 22 2021 at 16:06):

My guess is that it would be fine to assume that all Λ\Lambda's are of the form Zn\mathbb{Z}^n. But we can't explicitly write it like that, because we'll run into defeq-issues.

view this post on Zulip Johan Commelin (Jan 22 2021 at 16:06):

So we need to describe free abelian groups in such a way that a product of two free abelian groups is again free abelian, etc...

view this post on Zulip Kevin Buzzard (Jan 22 2021 at 18:53):

@Amelia Livingston has some partial progress on this

view this post on Zulip Filippo A. E. Nuccio (Jan 25 2021 at 12:59):

Is it in mathlib or is she working on her own?

view this post on Zulip Kevin Buzzard (Jan 25 2021 at 13:06):

I'm meeting her this afternoon, I can ask her the status of things. I don't think she's actively working on it right now

view this post on Zulip Filippo A. E. Nuccio (Jan 25 2021 at 20:09):

Sorry to read your message so late, but I'm eager to read anything she's been doing, in case you ended up asking.

view this post on Zulip Kevin Buzzard (Jan 25 2021 at 22:03):

The answer was https://github.com/101damnations/fg_over_pid , which is unfinished, and currently she's more worried about her finals than finishing it (which is fair enough -- she's also working on Koszul complexes in Lean as part of her project)

view this post on Zulip Filippo A. E. Nuccio (Jan 26 2021 at 07:48):

Oh sure! Thanks, I'll have a look at the repository and see if I can extract useful pieces of code.

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:13):

Filippo, I have been thinking about how to formalize this result and I suspect that it might be a good idea to break the problem in two.

First, show that we can fit the "inequalities", working over a Q (or R). This should be easy, since the inequalities are open and homogeneous, so we should get cones that are non-empty, since we start with x that lies in these cones.

Second, we show that if we have open cones, then we can fit the congruence condition. This should be a "density" argument: an open cone and a lattice should meet.

How does that sound? I have not yet written down the statements, nor the frame of the proof of Lemma 9.7, so some details might change.

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:20):

I think that cones are not in mathlib. We could introduce them as submodules for ℝ≥0 in an add_comm_semigroup with an ℝ≥0 action. We could probably get rid of and work with a linearly ordered group_with_zero. I am less sure about this.

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:24):

you'll need a semiring, if you want to use mathlibs submodules, right?

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:26):

Ah, you are right. It would be the comm_semiring of the non-negative reals.

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:27):

Still, I think that breaking off the "inequalities" from the "congruences" will make the arguments easier to write and prove.

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:27):

sounds good

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:28):

I am teaching in half an hour, so I am not sure that I can have a skeleton ready before that, but I will try!

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:37):

Since I am not too familiar with structures, does this seem reasonable?

structure cone (V : Type*) [normed_group V] [normed_space  V] :=
(carrier : set V)
(add_mem :  {a b : V}, a  carrier  b  carrier  a + b  carrier)
(nonneg_smul_mem :  {r : },  {a : V}, 0  r  a  carrier  r  a  carrier)

Updated version with nonneg instead of pos.

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:41):

@Damiano Testa from a lean side, yes. From a maths side: can cones be empty? Or do you want zero_mem?

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:41):

if yes, then I would change pos_smul_mem to nonneg_smul_mem

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:42):

For this specific application, I am thinking of open half-spaces, and I thought that having a strict inequality might be better. I do not know whether this is really a good idea, though.

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:42):

you know more about the maths than I do

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:43):

From the presence of a point, I would like to deduce the existence of an open containing it (and inside the cone). I am hoping to eliminate a few boundary cases like this, but I may simply be shuffling the problem around... I am not sure.

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:44):

However, I do not have the time to play with either of the two possibilities before my class/meetings. I am not convinced that the positivity assumption will solve more problems than it creates.

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:45):

My intuition says that you should prove this for nontrivial cones (-;

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:46):

In any case, the first few lemmas will be about the fact that a (open/closed) half-space is a cone, that an intersection of cones is a cone... these will require small tweaks, if we change the inequality, right?

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:46):

Ah, ok, I like the non-triviality!

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:46):

Ok, I will make it non-negative multiplication. It may also be useful to have a zero element.

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:48):

I changed the definition above: our conversation appears meaningless now, but the code is correct!

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:50):

Ooh, but you still don't have a 0 (-;

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:50):

With this definition the open first quadrant in R^2 union the origin is a cone. While I am not opposed to this, it will be something to keep in mind when proving stuff about cones.

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:51):

Well, empty is easy to split off, no?

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:51):

or should I assume zero_mem?

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:52):

If you do, then it's literally submodule nnreal V, right?

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:52):

(You might need an is_scalar_tower nnreal real V instance for real vector spaces, if that doesn't yet exist.)

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:52):

I have not worked with nnreal, but given the name, I suspect that it is!

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:53):

So, maybe I can work with submodule nnreal V and then try to make statements about the submodules with non-empty interior.

view this post on Zulip Peter Scholze (Jan 26 2021 at 08:53):

Just a quick comment that the proof of 9.7 really makes critical use of the fact that the cones are defined by inequalities with rational coefficients. And the argument is also only really working with closed cones.

view this post on Zulip Johan Commelin (Jan 26 2021 at 08:53):

It is \R\ge0 for people with unicode keyboards...

Ooh well, I guess I can type R0\mathbb{R}_{\ge0}

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:55):

Peter, thank you for your comment: I will keep it in mind!

In any case, Lean will not allow me to prove something that is not true! :wink:

view this post on Zulip Peter Scholze (Jan 26 2021 at 08:56):

sure :-)! I think the central part of the argument even has an official name (blahblah's lemma or so), let me try to find it again...

view this post on Zulip Peter Scholze (Jan 26 2021 at 08:57):

Gordan's lemma it is: https://en.wikipedia.org/wiki/Gordan%27s_lemma

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:57):

At the moment, I am trying to get to a stage where proving that a non-empty open cone contains a basis. Once there will be enough lemmas to get there, I think that we can focus on the actual proof of the lemma and the tools that are needed specifically for that.

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:58):

Thanks for the reference!

view this post on Zulip Peter Scholze (Jan 26 2021 at 08:58):

What do you mean by basis here?

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:59):

I mean a basis of the rational vector space (In my mind, this is a statement about lattices and I constantly change between the integers and the rationals.)

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:59):

The reals might be useful, since there are a lot of results about real stuff already in Lean, which is why I am starting with R.

view this post on Zulip Damiano Testa (Jan 26 2021 at 08:59):

I now have to "go" to my virtual class!

view this post on Zulip Peter Scholze (Jan 26 2021 at 08:59):

ah, just a basis for the vector space, not for the cone

view this post on Zulip Peter Scholze (Jan 26 2021 at 09:00):

OK, nice chatting with you!

view this post on Zulip Damiano Testa (Jan 26 2021 at 09:00):

Yes, indeed!

view this post on Zulip Damiano Testa (Jan 26 2021 at 09:00):

more on this later!

view this post on Zulip Sebastien Gouezel (Jan 26 2021 at 09:23):

There are already cones in mathlib, in analysis/convex/cone.

view this post on Zulip Sebastien Gouezel (Jan 26 2021 at 09:24):

docs#convex_cone

view this post on Zulip Johan Commelin (Jan 26 2021 at 09:33):

@Sebastien Gouezel ooh, thanks for the pointer. Not sure why I forgot about that :face_palm:

view this post on Zulip Sebastien Gouezel (Jan 26 2021 at 09:35):

The problem when you grep for cone is that you have too much of it in category theory. I grepped for convex_cone instead :-)

view this post on Zulip Filippo A. E. Nuccio (Jan 26 2021 at 10:36):

@Damiano Testa I am teaching the whole day today and I am finishing another project, so I have been only thinking superficially at the problem. I also agree that one can split things up. I though about making a separate lemma for the case where all x(λi)x(\lambda_i) are positive, and then to take the union, which is the strategy in the paper, basically. I was also thinking about removing the freeness assumption, since at any rate any hom from a torsion group to Z\mathbb{Z} would be trivial (of course, I did not want to remove the f.g. one...). So I was trying to go in a different direction, but yours seems reasonable, and I'll look at it asap.

view this post on Zulip Damiano Testa (Jan 26 2021 at 14:00):

I am looking at convex_cone in mathlib and I am tempted to simply use this notion. It uses pos_mul, rather than nonneg_mul. In any case, I do not think that it would be a great deal to switch from one to the other.

I will import it, start playing with it and see how it pans out!

view this post on Zulip Adam Topaz (Jan 26 2021 at 15:33):

Hey, I'm just catching up on this discussion now. Why isn't a convex cone defined as a nnreal submodule of a real vectorspace?

view this post on Zulip Adam Topaz (Jan 26 2021 at 15:34):

Or I guess I should say "subsemimodule" or whatever.

view this post on Zulip Johan Commelin (Jan 26 2021 at 15:34):

might be historical reasons...

view this post on Zulip Damiano Testa (Jan 26 2021 at 15:35):

I think that the role of 0 is special in cones, and it may be better sometimes, to not automatically assume that 0 is in all cones.

view this post on Zulip Damiano Testa (Jan 26 2021 at 15:35):

However, I agree that whether you always add 0, or only sometimes, will not create any huge difference in the theory!

view this post on Zulip Adam Topaz (Jan 26 2021 at 15:54):

Is the definition of polyhedral lattice in the repo actually correct? I'm trying to fill in the sorry in polyhedral_lattice.lean and I get to the following:

instance int : polyhedral_lattice  :=
{ tf := λ m hm n h,
  begin
    rw [ nsmul_eq_smul, nsmul_eq_mul, mul_eq_zero] at h,
    simpa only [hm, int.coe_nat_eq_zero, or_false, int.nat_cast_eq_coe_nat] using h
  end,
  polyhedral' :=
  begin
    use {1},
    split,
    { simp [finset.coe_singleton],
      rw eq_top_iff,
      rintro n -,
      rw submodule.mem_span_singleton,
      use n,
      rw [ gsmul_eq_smul, gsmul_one, int.cast_id] },
    { intros x,
      let b : {a :  // a  ({1} : finset )} := 1,by simp⟩,
      have : (finset.univ : finset {a // a  ({1} : finset )}) = {b}, by tauto,
      erw this,
      simp,
      -- ∥ x b • 1 ∥ = x b • 1
    },
  end }

view this post on Zulip Adam Topaz (Jan 26 2021 at 15:55):

Full context:

x : {a // a  {1}}  ,
b : {a // a  {1}} := 1, _⟩,
this : finset.univ = {b}
 x b  1 = x b  1

view this post on Zulip Johan Commelin (Jan 26 2021 at 16:00):

@Adam Topaz I might have messed up! I just tried to get the ball rolling.

view this post on Zulip Johan Commelin (Jan 26 2021 at 16:00):

Please fix my blunders (-;

view this post on Zulip Adam Topaz (Jan 26 2021 at 16:01):

The following seems more reasonable, no?

class polyhedral_lattice (A : Type*) [normed_group A] :=
(tf : torsion_free A)
(polyhedral' [] :  s : finset A, submodule.span  (s : set A) =  
               n : {a // a  s}  , ∥∑ a, n a  a.1 =  a,  n a   a.1)

view this post on Zulip Johan Commelin (Jan 26 2021 at 16:06):

Yes, a lot more (-;

view this post on Zulip Johan Commelin (Jan 26 2021 at 16:07):

Maybe we want abs around the integer, I don't know. That's a design decision. But at least your version is maths-correct, and mine wasn't.

view this post on Zulip Adam Topaz (Jan 26 2021 at 16:07):

Is it obvious that this matches the definition in analytic.pdf on page 59?

view this post on Zulip Adam Topaz (Jan 26 2021 at 16:08):

(In any case, I made the change and killed the sorry, and pushed)

view this post on Zulip Johan Commelin (Jan 26 2021 at 16:09):

Adam Topaz said:

Is it obvious that this matches the definition in analytic.pdf on page 59?

Not obvious-obvious to me. It would be good to get something closer to p59. But that definition looks complicated to work with in Lean.

view this post on Zulip Filippo A. E. Nuccio (Jan 26 2021 at 17:40):

@Damiano Testa @Adam Topaz I have just git pulled and it seems to me that the statement of Lemma 9.7 is still the same. Are you working on paper (I'm also trying to...) or have I missed something?

view this post on Zulip Adam Topaz (Jan 26 2021 at 17:40):

Oh, I changed the definition of polyherdral_lattice.

view this post on Zulip Adam Topaz (Jan 26 2021 at 17:43):

Which file has the statement of Lemma 9.7?

view this post on Zulip Filippo A. E. Nuccio (Jan 26 2021 at 17:43):

combinatorial_lemma.lean

view this post on Zulip Filippo A. E. Nuccio (Jan 26 2021 at 17:45):

(deleted)

view this post on Zulip Filippo A. E. Nuccio (Jan 26 2021 at 17:45):

(deleted)

view this post on Zulip Damiano Testa (Jan 26 2021 at 19:44):

I did not push anything yet: I was trying to get somewhere more stable before doing so.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 10:37):

@Damiano Testa I have seen you're now actively working on polyhedral lattices. Do you think the "new" formulation you're heading to will make Lemma 9.7 useless or are you still also working on it? I am trying to come up with a " purely algebraic" strategy for it, using duals of free f.g. abelian groups, but I wonder if this is useless/obsolete.

view this post on Zulip Damiano Testa (Jan 27 2021 at 10:40):

I am not sure which strategy will work best in Lean, so at the moment, I think that we should all try to make it work and we will find out later which approach is more successful. I am still trying to get the proof of 9.7 in place, though!

view this post on Zulip Peter Scholze (Jan 27 2021 at 10:52):

I'm excited to watch this progress! But I'm curious: In which sense would Lemma 9.7 become useless?

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 10:55):

No, no, I was wondering if Damiano and others were finding another path. I don't think it will (and really: it was simply a question before starting formalizing it, not any kind of "hint")

view this post on Zulip Damiano Testa (Jan 27 2021 at 10:55):

I am not sure that it will become useless, but I would interpret this as "the proof will fall out from a formalization of the polyhedral stuff".

view this post on Zulip Peter Scholze (Jan 27 2021 at 11:05):

OK, that sounds good :-). So you are actually saying that you will formalize Lemma 9.7, but just as part of a much larger effort on polyhedral lattices?

view this post on Zulip Damiano Testa (Jan 27 2021 at 14:00):

My impression is that a lot of the tools that will go into polyhedral lattices will also be useful to prove lemma 9.7. When formalizing something, you start by proving lots of very trivial results and it makes sense to make sure to only require lots of trivial results only once! So, I think that trying to get polyhedral stuff into Lean might yield useful tools to prove lemma 9.7.

At the same time, working on the concrete goal of proving lemma 9.7 is also useful to see which results will be needed and which ones will not. So, maybe the two streams will go parallel, but closeby!

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 14:37):

Indeed, I believe that if we have a good understanding of free modules, proving Lemma 9.7 it should be "easy". But I don't know if Lean contains the statement that if you have nn linearly independent elements μ1,...μn\mu_1,...\mu_n in Zk\mathbb{Z}^k then you can produce a linear map f ⁣:ZkZf\colon\mathbb{Z}^k\to\mathbb{Z} taking any chosen values αi\alpha_i on each μi\mu_i.

view this post on Zulip Johan Commelin (Jan 27 2021 at 14:39):

Lean's biggest problem is that you can't call the elements λi\lambda_i...

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 14:57):

Corrected :wink:

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 15:02):

This isn't true for my understanding of linearly indepedent -- you can't send 2 to 1 without introducing denominators. But I should think that this sort of thing is either there already or would be easily doable

view this post on Zulip Johan Commelin (Jan 27 2021 at 15:03):

I think we can just use basis from linear algebra

view this post on Zulip Damiano Testa (Jan 27 2021 at 15:11):

It may also be the case that simply using the submodule spanned by the images is all we need...

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 15:12):

Kevin Buzzard said:

This isn't true for my understanding of linearly indepedent -- you can't send 2 to 1 without introducing denominators. But I should think that this sort of thing is either there already or would be easily doable

Oh sure! I meant to say that they were part of a basis.

view this post on Zulip Adam Topaz (Jan 27 2021 at 15:13):

The words free_module don't even show up in the mathlib API search :sad:

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 15:14):

Adam Topaz said:

The words free_module don't even show up in the mathlib API search :sad:

Yes, that is what I had realized. But I hoped to dig a bit better in the linear_algebra file.

view this post on Zulip Riccardo Brasca (Jan 27 2021 at 15:14):

But free_abelian_group does!

view this post on Zulip Adam Topaz (Jan 27 2021 at 15:15):

Is there a docs#free_abelian_group.lift ?

view this post on Zulip Adam Topaz (Jan 27 2021 at 15:17):

So this lift is what @Filippo A. E. Nuccio was looking for, right?

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 15:18):

Oh wow, it can very well be! I am teaching now and will have a deep look at this tonight. Thanks!

view this post on Zulip Adam Topaz (Jan 27 2021 at 15:18):

Or do you want to lift with respect to some other basis which need not be the "standard" basis?

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 15:18):

I don't know yet, honestly. But will try to find out soon and post here what I end up with.

view this post on Zulip Johan Commelin (Jan 27 2021 at 15:46):

No, we really don't want to use free_abelian_group. We will need characteristic predicates for this stuff.

view this post on Zulip Johan Commelin (Jan 27 2021 at 15:47):

Because once we start taking powers and quotients, you still want your API to work

view this post on Zulip Johan Commelin (Jan 27 2021 at 15:48):

The other option is that we completely rewrite the proof of 9.5 to only use lattices of the form Zk\mathbb{Z}^k. But that doesn't seem natural.

view this post on Zulip Adam Topaz (Jan 27 2021 at 15:55):

Johan Commelin said:

No, we really don't want to use free_abelian_group. We will need characteristic predicates for this stuff.

Since we're ignoring universes for the most part, perhaps it makes sense to write down the usual universal property of the free module as the characteristic predicate?

view this post on Zulip Johan Commelin (Jan 27 2021 at 15:59):

can't we just define it as "have a finite basis", and then prove the universal property?

view this post on Zulip Adam Topaz (Jan 27 2021 at 15:59):

Sure.

view this post on Zulip Adam Topaz (Jan 27 2021 at 16:00):

Don't we have this somewhere in the repo already?

view this post on Zulip Johan Commelin (Jan 27 2021 at 16:06):

nope, I don't think so

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 17:29):

Johan Commelin said:

No, we really don't want to use free_abelian_group. We will need characteristic predicates for this stuff.

@Johan Commelin Can you speculate a bit about this notion of "characteristic predicates", or point to a reference? In particular, what would the issue with quotients/powers be? Concerning rewriting 9.5 entirely, I want to insist that I haven't finished my proof on paper yet, so if the rewriting has to do with Lemma 9.7 in light of using free abelian groups, please wait! May be Damiano's approach will be more efficient and his work on polyhedral lattices will be the right path.

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:31):

@Filippo A. E. Nuccio for example we would want the fact that the product of two free modules is free, so you want to characterize free modules in some way that makes it easy to obtain such facts.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 17:32):

Makes sense, sure. But why is

def free_abelian_group : Type u :=
additive $ abelianization $ free_group α

"bad" in this perspecitve? Do we like something like a is_free_abelian_group : (Type *) ---> Prop more?

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:32):

because the definitions dont matter :rofl:

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:33):

It's not bad per se. Rather it's just a construction that says "hey, look, the free abelian group on a type \alpha actually exists."

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:34):

But this is somehow separate from the characterization of free modules that Johan was referring to.

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:35):

@Filippo A. E. Nuccio if you write a lot of lemmas about free_abelian_group X, then you cannot apply those lemmas to (free_abelian_group X) \times (free_abelian_group Y). If instead, you prove the lemmas about torsion free groups with a finite basis, then everything is fine.

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:36):

Same thing with (fin n) -> \Z and finsupp (fin n) \Z and 37 other ways that we can build free abelian groups.

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:37):

You want lemmas that work for all of those. So you need to find a characterisation that takes an arbitrary group as input, and asserts that it behaves like a free_abelian_group X.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 17:37):

Ok, so something like is_free_abelian_group : (Type *) ---> Prop?

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:38):

Or maybe is_free (R) (M) that characterizes free modules

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:38):

More like is_free_abelian_group A X : Prop

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:38):

import linear_algebra.basis

variables (A M : Type*) [ring A] [add_comm_group M] [module A M]

class fg_free_module :=
(S : set M)
(finite : S.finite)
(is_basis : is_basis A (coe : S  M))

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:38):

which says A ~= free_abelian_group X

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:38):

that's not quite right....

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:38):

I don't know if we want to fix the basis in the predicate, or only assert the existence.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 17:39):

Yes, it seems dangerous to fix the basis, I believe, no?

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:39):

For free groups I think you want to fix the basis

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:39):

@Adam Topaz your class is not a Prop

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 17:39):

These would be "framed free groups", no?

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:39):

for fg you probably want to quantify over it

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:39):

Better:

import linear_algebra.basis

variables (A M : Type*) [ring A] [add_comm_group M] [module A M]

def fg_free_module : Prop :=  (S : set M), S.finite  (is_basis A (coe : S  M))

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:40):

Why is S a subset of M instead of just an arbitrary finite type or fin n?

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:40):

I think we can then continue to prove theorems about arbitrary fintypes with basis-maps to M.

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:41):

import category_theory.Fintype
import linear_algebra.basis

open category_theory

variables (A M : Type*) [ring A] [add_comm_group M] [module A M]

def fg_free_module : Prop :=  (S : Fintype) (ι : S  M), (is_basis A ι)

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:41):

:smile:

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:41):

which universe does S live in?

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:41):

Does it matter?

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:41):

I would suggest quantifying only over fin n and proving the fintype version

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:42):

because there is a universe issue as johan points out

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:42):

docs#category_theory.Fintype.skeleton

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:42):

but why not just use the finset in the defn?

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:42):

I think the finset adds an unnecessary injectivity restriction

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:43):

If you use fin n, then you would need to go back and forth with the equuivalence between fin n \sum fin mand fin (n+m) which isn't much fun.

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:43):

is_basis makes it injective, right?

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:43):

yes it's a basis so injectivity is almost always redundant, but it's an extra thing that has to be dealt with in proofs

view this post on Zulip Adam Topaz (Jan 27 2021 at 17:44):

Okay, how about this:

import category_theory.Fintype
import linear_algebra.basis

open category_theory

variables (A M : Type*) [ring A] [add_comm_group M] [module A M]

def fg_free_module : Prop :=  (S : Fintype.{0}) (ι : S  M), (is_basis A ι)

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:44):

I don't really care. We want a defn and 37 constructors (-;

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:45):

To clarify, with the fin n version you have a constructor

def fg_free_module.mk (A) [fintype A] (f : A -> M) : is_basis A f -> fg_free_module A M

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:45):

and note that A can come from any universe

view this post on Zulip Damiano Testa (Jan 27 2021 at 18:30):

How hard would it be to work with the property that any surjective map to a free abelian group admits a section?

view this post on Zulip Johan Commelin (Jan 27 2021 at 18:34):

that should be a theorem, not a def

view this post on Zulip Johan Commelin (Jan 27 2021 at 18:35):

because it quantifies over types, which is better avoided

view this post on Zulip Damiano Testa (Jan 27 2021 at 18:36):

Ah, I see

view this post on Zulip Damiano Testa (Jan 27 2021 at 18:42):

And a finsupp from a (finite if wanted) Type to Z?

view this post on Zulip Johan Commelin (Jan 27 2021 at 18:44):

that shouldn't be a defn either, but an example of free abelian groups

view this post on Zulip Damiano Testa (Jan 27 2021 at 18:45):

Ok, I will keep quiet!

view this post on Zulip Johan Commelin (Jan 27 2021 at 18:45):

because the product of two finsupp _ _s is not of the form finsupp _ _

view this post on Zulip Johan Commelin (Jan 27 2021 at 18:46):

So you want a definition that works for all free abelian groups... not just for some constructions.
This is a concept that is somewhat strange for mathematicians. Because Zm×Zn=Zm+n\mathbb{Z}^m \times \mathbb{Z}^n = \mathbb{Z}^{m+n}, right?

view this post on Zulip Johan Commelin (Jan 27 2021 at 18:46):

But lean will not agree about that =

view this post on Zulip Peter Scholze (Jan 27 2021 at 19:12):

I think algebraic topologists wouldnt agree either. Ask them about signs (or, in fact, all higher homotopy groups of spheres) arising from swapping factors ;-)

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 19:23):

Here's a question I ran into the other day. Say we have a short exact sequence of short exact sequences, i.e. a 3x3 grid of modules (say for a group G) with all rows and columns exact. Say the top left hand module is A1A_1 and the bottom right is C3C_3. Using boundary maps we can construct two maps Hn(G,C3)Hn+2(G,A1)H^n(G,C_3)\to H^{n+2}(G,A_1) (one going around two sides of the square, the other around the other two sides). Are these maps (a) the same, (b) different by a sign, (c) depends on conventions? Not a serious question, but it does remind you how scary this stuff is.

view this post on Zulip Adam Topaz (Jan 27 2021 at 19:39):

@Kevin Buzzard You just gave me something to give my students on their next homework assignment. Thanks.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 19:42):

I wanted to compute explicitly for n=0 but managed to get confused about what the explicit boundary map was from 1-cocycles to 2-cocycles. What do you tell your students is the map from 0-cocycles to 1-cocycles? Given cCc\in C pull back to bBb\in B, and now the difference of bb and gbgb is in AA, and that's where you send gg. But is it bgbb-gb or gbbgb-b?

view this post on Zulip Adam Topaz (Jan 27 2021 at 19:43):

My go-to convention is gbbgb-b.

view this post on Zulip Adam Topaz (Jan 27 2021 at 19:43):

.... I think.... I can't even remember...

view this post on Zulip Adam Topaz (Jan 27 2021 at 19:45):

Okay, my go-to convention is indeed gbbgb-b because [NSW] says so on page 15
https://www.mathi.uni-heidelberg.de/~schmidt/NSW2e/NSW2.1.pdf

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 19:46):

So you agree that this is just a convention?

view this post on Zulip Adam Topaz (Jan 27 2021 at 19:46):

absolutely.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 19:49):

Is your convention for the map from C-valued 1-cocycles to A-valued 2-cocycles a second independent convention, or is it somehow tied down by your convention for 0-cocycles to 1-cocycles?

view this post on Zulip Adam Topaz (Jan 27 2021 at 19:52):

It's a priori independent, but I would generally follow the "consistent" formula from page 14 of [NSW] :smile:

view this post on Zulip Johan Commelin (Jan 27 2021 at 19:52):

Kevin Buzzard said:

Are these maps (a) the same, (b) different by a sign, (c) depends on conventions? Not a serious question, but it does remind you how scary this stuff is.

It depends on whether the first map goes clockwise and the second counter-clockwise around the diagram, or the other way round...

view this post on Zulip Adam Topaz (Jan 27 2021 at 19:57):

Maybe it is pinned down with the formula for the boundary of the cup-product.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 19:57):

p14 of NSW doesn't give conventions for signs for boundary maps, it seems to me, only for the definitions of the cohomology groups themselves. p15 of the version I'm looking at writes down an explicit map H0(C)H1(A)H^0(C)\to H^1(A) which seems to come out of the blue, and of course there is the claim that it is "canonical".

view this post on Zulip Adam Topaz (Jan 27 2021 at 19:58):

Oh, I'm thinking of the usual thing where you choose a lift to the middle term of the exact sequence and apply the differential in the complex to obtain the bounday map on cohomology.

view this post on Zulip Riccardo Brasca (Jan 27 2021 at 19:59):

This is just because derived functors are defined via a universal property, so they are unique up to isomorphism, right?

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 19:59):

but derived functors are not just a choice of cohomology groups, they are also a compatible choice of boundary maps for every short exact sequence.

view this post on Zulip Riccardo Brasca (Jan 27 2021 at 20:00):

Sure, they are unique up to isomorphism of δ\delta-functors, or whatever the terminology is

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:00):

So in particular here is an isomorphism between group cohomology and itself -- it's the identity on HnH^n for all n37n\not=37, and 1-1 for n=37n=37. This changes some boundary maps.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:01):

In particular it does not even really make sense to ask what "the" boundary map H36(C)H37(A)H^{36}(C)\to H^{37}(A) is. You have to tell me, when you're defining cohomology.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:02):

And there is certainly no guarantee that it is the same one that is being used in the references you're using.

view this post on Zulip Patrick Massot (Jan 27 2021 at 20:05):

Isn't there a famous paper by Deligne about all this fun?

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:05):

Fortunately, the choices Hn(C)Hn+1(A)H^n(C)\to H^{n+1}(A) all have to be compatible, so you can only change them all at once. This means that my question about Hn(C3)Hn+2(A1)H^n(C_3)\to H^{n+2}(A_1) is at least well-defined, in the sense that it is independent of convention. It is either always the same for each route round the square, or always off by a sign.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:05):

Yes, I took a look at this paper only last week in an attempt to resolve this issue, but he doesn't go explicitly into this point.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:06):

I am still really confused about the cup product issue which Adam raised. Any diagram at all which has only one occurrence of a boundary map HnHn+1H^n\to H^{n+1} -- it seems to me that it does not even make sense to ask whether it commutes until more information is given about the definitions of the boundary maps.

view this post on Zulip Peter Scholze (Jan 27 2021 at 20:09):

Well, it probably also uses maps from some concrete things into HnH^n's, and then you have to look how those are defined in turn. If they make use of explicit cochain representatives, then yeah.

For the question, my guess is that it's 1-1; you seem to be swapping to degree 11 maps, which should introduce a sign. Although you can surely find many papers of mine where I pretend it's the identity.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:17):

According to Neukirch it is indeed -1.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:26):

Oh Adam -- the 3x3 question is 1.3.4 in NSW, I just ran into it whilst looking through the book hoping for some more enlightenment about cup products. Amelia has been collapsing double complexes Ci,j:=AiBjC_{i,j}:=A_i\otimes B_j into single complexes and defining explicit boundary maps in Lean. Her collapsed Cn:=i+j=nCi,jC_n:=\oplus_{i+j=n}C_{i,j} are fine, but when she defined the differential between them she simply had to choose between (1)i(-1)^i and (1)j(-1)^j at some point, and it really felt to me that it was just a coin-toss.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:32):

Got one: NSW 1.4.3 is a claim about a diagram commuting which has precisely one boundary map from degree p+qp+q to p+q+1p+q+1. I don't even see how it makes sense to claim that this diagram commutes unless you announce your conventions and make it clear that anyone who uses that result needs to be using the same conventions for boundary maps. This is just like the nightmare I faced when writing some parts of Buzzard-Diamond-Jarvis and I had to try to figure out everyone's convention on Shimura varieties. Some people explicitly said they were using Deligne's convention for class field theory (typically the people working in large generality); some said explicitly they were using Artin's (typically the people doing Heegner point computations for Shimura curves over totally real fields, for whom the inverse is just an unnecessary bother for the equations they deal with) and some people simply did not say at all. Those folk of course had the best of both worlds, because in their ignorance they could borrow computations from all the literature instead of just half of it.

view this post on Zulip Adam Topaz (Jan 27 2021 at 20:32):

Sorry -- I have "zoom office hours" right now, so I can't really follow all the discussion...

view this post on Zulip Adam Topaz (Jan 27 2021 at 20:33):

But good to know that [NSW] has the details :)

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:59):

I think I understand now. Let's say a pinning of a cohomology theory is a choice of signs for all boundary maps. Once it is pinned, then there is a choice of cup products Hp(A)×Hq(B)Hp+q(AB)H^p(A)\times H^q(B)\to H^{p+q}(A\otimes B) whose sign depends on the pinning (i.e. if I change my boundary map H37(C)H38(A)H^{37}(C)\to H^{38}(A) then some of these cup product maps change sign too) and which satisfies all the theorems in the book.

view this post on Zulip Adam Topaz (Jan 27 2021 at 21:11):

Yeah, that sounds reasonable. And as for the boundary map, in NSW they actually prove the snake lemma, and part of the proof is the "construction" of the boundary map, so that's what they take as their definition throughout.

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 21:21):

I am still a bit confused by this because the boundary map in the snake lemma really _does_ feel like it's "more canonical than the other choice" -- like the obvious map from a vector space to its double-dual really is better than the one where you randomly introduce a minus sign.

view this post on Zulip Adam Topaz (Jan 27 2021 at 21:25):

What happens if we want to define group cohomology for semimodules :expressionless: ?

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 21:27):

But there is something I don't understand: Grothendieck writes in his Tohokou :

Soit T=(Ti),0iaT = (T^i), 0 \leq i\leq a un δ\delta-foncteur
covariant de CC dans CC', où a>0a > 0. TT est dit un δ\delta-foncteur universel si pour tout δ\delta-foncteur T=(Ti)T '= (T'^i) fonctoriel défini pour les mêmes degrés, et tout morphisme fonctoriel fi0f^{i_0} de Ti0T^{i_0} dans Ti0T'^{i_0}, il existe un seul morphisme et un seul ff de TT dans TT' qui pour le degré i0i_0 se réduise à fi0f^{i_0}.

In particular, all our functors (say, group cohomology) are not universal δ\delta functors, because the functorial isomorphism in question is not unique?

view this post on Zulip Adam Topaz (Jan 27 2021 at 21:28):

It is unique, but if you change the δ\delta in one of these functors by δ-\delta then you need to change the corresponding morphism comparing them as well.

view this post on Zulip Adam Topaz (Jan 27 2021 at 21:28):

At least I think that's the idea...

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 21:29):

Well, but if I can change the 37-th, I have infinitely many choices.

view this post on Zulip Adam Topaz (Jan 27 2021 at 21:29):

The boundary maps are part of the "data" of a δ\delta-functor.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 21:29):

This I understand. But what is a universal one, then?

view this post on Zulip Adam Topaz (Jan 27 2021 at 21:31):

It's one satisfying the universal property, which says that for all blah blah blah there exists a unique morphism such that blah blah. So if I multiply the boundary map by 1-1 in such a universal delta functor, it's still universal, but the "unique morphism" will be different...

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 21:31):

Ah, I see. If I take two cohomology theories, one with a certain δ37\delta_{37} and the other with all the δi\delta_i's equal to those of the first, but the 37-th, then the map comparing them is unique.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 21:35):

Kevin Buzzard said:

I am still a bit confused by this because the boundary map in the snake lemma really _does_ feel like it's "more canonical than the other choice" -- like the obvious map from a vector space to its double-dual really is better than the one where you randomly introduce a minus sign.

If you're looking at the snake lemma on page 25 of NSW leading to Theorem 1.3.2, I agree that it is somehow "more canonical that the other choice", but the \partial_\ast are not.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 21:36):

They are defined explicitly through the alternating sum on page 15, I guess, and there is clearly a choice of sign there (you can index from 0 to n or from 1 to n+1, affecting the (1)n(-1)^n).

view this post on Zulip Patrick Massot (Jan 27 2021 at 22:10):

This is all nice and fun, but we drifted quite a bit. I think we should try to stay closer to the main topic in this stream, otherwise Peter may miss messages that actually need his input.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 22:17):

Yes, I agree. Apologies to Peter, we might continue this discussion with @Kevin Buzzard and @Adam Topaz elsewhere.

view this post on Zulip Peter Scholze (Jan 27 2021 at 22:22):

I enjoy random conversations, don't bother about me :-)

view this post on Zulip Peter Scholze (Jan 27 2021 at 22:23):

By the way, for more fun regarding signs, this project actually also needs simplicial stuff, in the proof of 8.19 (used later when there is also some simplicial stuff in the main proof 9.5)

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 22:26):

In the first part of its proof, when you split the hypercover?

view this post on Zulip Peter Scholze (Jan 27 2021 at 22:26):

well, the statement itself is simplicial!

view this post on Zulip Peter Scholze (Jan 27 2021 at 22:27):

or do you mean the signs? I just mean that in Dold-Kan etc you can surely have fun fixing all the signs

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 22:27):

Yes, I meant the signs.

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 22:28):

(And we might debate if "fun" is the most appropriate word... :smile: )

view this post on Zulip Peter Scholze (Jan 27 2021 at 22:28):

Sorry, this is my sense of humour ;-)

view this post on Zulip Peter Scholze (Jan 27 2021 at 22:29):

well, anyways I'm off for tonight. See you around!

view this post on Zulip Filippo A. E. Nuccio (Jan 27 2021 at 22:29):

See you, bye!

view this post on Zulip Filippo A. E. Nuccio (Jan 29 2021 at 19:19):

I am a bit confused about the sign requirement of Lemma 9.7: now it reads

the numbers x(λi)x'(\lambda_i) and (xx)(λi)(x-x')(\lambda_i) have the same sign

but I wonder if it should not be

the numbers x(λi)x(\lambda_i) and (xx)(λi)(x-x')(\lambda_i) have the same sign

Or am I misunderstanding the idea of the lemma?

view this post on Zulip Peter Scholze (Jan 29 2021 at 20:41):

The first implies the second, and I really want the first

view this post on Zulip Filippo A. E. Nuccio (Jan 29 2021 at 21:05):

Ah, ok. I agree that the first implies the second, but I thought the second was enough

view this post on Zulip Filippo A. E. Nuccio (Jan 29 2021 at 21:07):

@Johan Commelin I think you have coded the second, weaker version of the inequality in the file. No?

view this post on Zulip Johan Commelin (Jan 29 2021 at 21:51):

Ooh, my bad. That must have been a typo. Please fix it.

view this post on Zulip Filippo A. E. Nuccio (Jan 30 2021 at 13:55):

Ok, fixed and pushed.

view this post on Zulip Peter Scholze (Feb 02 2021 at 19:45):

Let's continue this conversation in the proper thread. Are you OK with the proof as given? I assume Gordan's lemma is the nontrivial part in the formalization?

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 19:52):

Yes, indeed. I agree with the proof, although it took me a while to figure out the x(λi)0x(\lambda_i)\geq 0 vs x(λi)0x'(\lambda_i)\geq 0 business. But as you explained the other day, it is the second that you need.

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 19:54):

Indeed, formalizing Gordan's lemma seems a bit painful: I am more and more going to convince myself that the prove isn't that hard: basically, a compact intersected with a discrete is finite, more or less. And this is certainly in mathlib. But I need that the dual of a free module is free, and to extract the positive cone from it. This I still do not know how to do.

view this post on Zulip Peter Scholze (Feb 02 2021 at 19:54):

The first proof here https://en.wikipedia.org/wiki/Gordan's_lemma seems like it shouldn't be too hard

view this post on Zulip Peter Scholze (Feb 02 2021 at 19:54):

I see

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 19:55):

The final part with the congruences should really be painless.

view this post on Zulip Peter Scholze (Feb 02 2021 at 19:55):

But actually, you don't need a basis -- these cones may need more generators than the vector space

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 19:55):

Right

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 19:56):

Still I need that it is f.g., and for this I ended up thinking if it wasn't possible to have a more constructive proof.

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 19:58):

Assuming always that xx is in the "positive dual cone", I wanted to somehow produce the xx' by looking at successive minima : fix λ1\lambda_1 and look for a x0x_0 which takes on λ1\lambda_1 the minimum, on all xΛ+x\in\Lambda_+^\vee of x(λ1)x(\lambda_1).

view this post on Zulip Peter Scholze (Feb 02 2021 at 19:58):

Aha. That seems tricky.

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 19:59):

Then do the same for λ2\lambda_2, etc... Of course, this will hugely depend on the choice of the ordering, but there are m!m! choices.

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 19:59):

(was mm the number of λ\lambda's?)

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:00):

I was thinking about that tonight and had been teaching the whole day, so I haven't checked whether this makes sense.

view this post on Zulip Peter Scholze (Feb 02 2021 at 20:00):

For the proof on wikipedia, you effectively need that if in a finite-dimensional Q\mathbb Q-vector space VV, if you intersect finitely many half-spaces f(v)0f(v)\geq 0 where ff is a linear function on VV, then this Q0\mathbb Q_{\geq 0}-module is finitely generated. (Once you have that, the rest of the proof on wikipedia should be easy to get.)

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:00):

If you see an evident obstruction, I might give up, otherwise, I'll think a little bit in this direction for a while.

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:01):

Peter Scholze said:

For the proof on wikipedia, you effectively need that if in a finite-dimensional Q\mathbb Q-vector space VV, if you intersect finitely many half-spaces f(v)0f(v)\geq 0 where ff is a linear function on VV, then this Q0\mathbb Q_{\geq 0}-module is finitely generated. (Once you have that, the rest of the proof on wikipedia should be easy to get.)

I agree.

view this post on Zulip Peter Scholze (Feb 02 2021 at 20:01):

Well, I really think it would be cleanest to prove Gordan's lemma

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:01):

Surely cleanest, you're right.

view this post on Zulip Peter Scholze (Feb 02 2021 at 20:02):

OK, so how does one get at that result on Q\mathbb Q-vector spaces...

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:03):

This should be what @Damiano Testa has been thinking about for a while, I haven't started yet.

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:03):

In particular, I haven't done a good analysis of what is in mathlib yet to know what is missing.

view this post on Zulip Peter Scholze (Feb 02 2021 at 20:04):

I see

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:05):

Already the dual cone scares me a bit (I mean: to show it is a cone), but I really need to think more before talking nonsense.

view this post on Zulip Peter Scholze (Feb 02 2021 at 20:07):

yeah, that's why I wrote that statement about Q0\mathbb Q_{\geq 0}-modules above -- I think it gets more directly to the point than defining cones

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:11):

I'll be thinking about the statement and will put here any advance. Now I really have to run for dinner, but as soon as I get somewhere I'll post here what I have.

view this post on Zulip Filippo A. E. Nuccio (Feb 02 2021 at 20:11):

Thanks for the clues! :wave:

view this post on Zulip Damiano Testa (Feb 03 2021 at 14:49):

Sorry for going quiet a bit. I will have more time on Friday, and only a few scattered moments before that.

Anyway, I had also converged on the fact that the main statement that we should formalize is that intersecting finitely many half-spaces in Q0\mathbb{Q}_{\geq 0} is finitely generated. I will try to at least formulate a statement that asserts this fact and will report back once I have it!

view this post on Zulip Johan Commelin (Mar 10 2021 at 07:12):

I think we are now at a point where we can state a version of Gordan's lemma (https://en.wikipedia.org/wiki/Gordan%27s_lemma) that we think will be nice to work with. @Damiano Testa is working hard on all the machinery needed to prove Gordan's lemma. But at the same time, we can start trying to prove lemma 9.7 assuming Gordan's lemma.

view this post on Zulip Filippo A. E. Nuccio (Mar 15 2021 at 15:54):

I made some advances for lemma 9.7. Assuming @Damiano Testa 's proof of Gordan's lemma, I have set-up the reduction step. What needs to be proved is only the "positive case", so the claim for all xx which pair positively with all λi\lambda_i's, which should be quite easy (am I writing this? :thinking: ) using Gordan's lemma.

view this post on Zulip Filippo A. E. Nuccio (Mar 15 2021 at 15:55):

The file still has a lot of "easy" sorry's, so I don't know how to proceed. Is it better to pull it to master or to wait to have it sorry-free?

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

No, just push to master

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

sorry s are fine, but there shouldn't be errors

view this post on Zulip Filippo A. E. Nuccio (Mar 15 2021 at 15:56):

No, no, there are no errors (but I will double-check before pushing).

view this post on Zulip Filippo A. E. Nuccio (Mar 15 2021 at 15:57):

I will at any rate keep on working on this on the coming days (not so much for today, I fear, but who knows). If you find that the strategy is bad/needs a fundamental revision, please warn me.

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

@Filippo A. E. Nuccio I think I've pushed errors to master several times :see_no_evil: but I always try to fix them asap...

view this post on Zulip Filippo A. E. Nuccio (Mar 15 2021 at 16:14):

Ok, I've pushed my changes. I have to prepare my lesson for tomorrow, but I'll probably be around on Zulip and hope to resume the work later on in the evening.

view this post on Zulip Filippo A. E. Nuccio (Mar 19 2021 at 17:53):

I have just pushed a proof of the "reduction step" from the positive version of lemma 9.7 to the full one. There are still some very minor sorry's here and there concerning sign vectors, and I hope to get rid of them tonight.

view this post on Zulip Johan Commelin (Mar 19 2021 at 18:00):

Sounds great, thanks!

view this post on Zulip Johan Commelin (Mar 19 2021 at 20:11):

@Filippo A. E. Nuccio It seems that you renamed lem97' to lem97''. I adapted combinatorial_lemma.lean.

view this post on Zulip Filippo A. E. Nuccio (Mar 19 2021 at 22:55):

Oh yes, you're right. I ended up with three versions of the lemma before deciding which one to throw away, and modified yours since I did not know it was already quoted somewhere. Of course, it makes more sense to go back to the previous numbering, as having a lem97'' without lem97' seems odd...

view this post on Zulip Filippo A. E. Nuccio (Mar 19 2021 at 23:14):

@Johan Commelin I have renamed it back to lem97' and modified combinatorial_lemma.lean accordingly, so that it compiles. I have also started the proof of lem97' building on lem97. I arrived at the point where the three lemmas you put in the "preamble" are needed, and wanted to know if you confirm they're in mathlib (and where).

view this post on Zulip Riccardo Brasca (Mar 19 2021 at 23:29):

Yes, they are now in mathlib... docs#abs_add_eq_add_abs_iff

view this post on Zulip Filippo A. E. Nuccio (Mar 20 2021 at 11:15):

Thanks!

view this post on Zulip Filippo A. E. Nuccio (Mar 20 2021 at 12:19):

I'm running into some coercion issues that I don't really know how to solve. The current statement of lem97' contains something like N * (y (l i)).nat_abs + (x' (l i)).nat_abs and I would like to apply some of the lemmas pointed out at by @Riccardo Brasca . For this, I need to convert nat_abs to abs, which I could do using int.abs_eq_nat_abs, but here the problem shows up. Since abs : ℤ → ℤ takes values in and nat_abs takes values in , the true equality is abs m = ↑ nat_abs m. Hence, I would need to change the statement to `N * ↑(y (l i)).nat_abs + ↑(x' (l i)).nat_abs. But if I do so, then combinatorial_lemma.lean does not compile any longer (it is unhappy with the terms being integers rather than natural numbers, and I can't but sympathize with it).

view this post on Zulip Kevin Buzzard (Mar 20 2021 at 12:21):

You first want to zify and then use the fact that the coercion of nat_abs back to int is abs

view this post on Zulip Filippo A. E. Nuccio (Mar 20 2021 at 12:21):

zify?

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

A tactic that turns statements about nat into statements about int

view this post on Zulip Filippo A. E. Nuccio (Mar 20 2021 at 12:23):

Wonderful! :grinning:

And dreadful at the same time: I could have spent two days looking for it without ever finding it... :sad:

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

I saw that Filippo made some more progress here! Thanks

view this post on Zulip Filippo A. E. Nuccio (Mar 30 2021 at 18:54):

In the proof of Lemma 9.7 I am using that N \neq 0. I can either do a case distinction at the beginning, getting rid of the case N=0 or, what seems more reasonable to me (since we're going to divide by N at any rate) to assume throughout that N \neq 0. But this requires a bit of refactoring, to add the assumption everywhere. What is best?

view this post on Zulip Johan Commelin (Mar 30 2021 at 19:16):

@Filippo A. E. Nuccio I think [fact (0 < N)] is fine, and shouldn't require much refactoring (hopefully)

view this post on Zulip Patrick Massot (Mar 30 2021 at 19:30):

The standard procedure is to do a case distinction at the beginning, especially if this assumption helps only with this lemma.

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 06:20):

Great, in this case I will add this and do a bit of refactoring when/where needed. But do you think it would overall be a good idea to leave N explicit or to make it implicit at the beginning of the section/file?

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

I think N should be explicit almost everywhere

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 06:23):

OK, I will simply add then (hN: 0 < N) in the statement of all results in lem 97 and all those that depend on them...

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:24):

Right, but if you use fact, then it might be automatic

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:24):

Typeclass inference will just find the [fact (0 < N)] if you add it to variables at the top of the file

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:25):

But is your lemma provable for N = 0?

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:25):

I didn't think about it

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 06:25):

Yes, I do think it is (I haven't though about it and am teaching now, but a brief thought yesterday evening convinced me it is trivial in that case).

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:26):

hmm... it looks like you can't get the finiteness in that case

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:26):

anyway, I need to run now

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 06:26):

OK, can you point at a file using fact where I can see how to use it?

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 06:26):

(if not, I'll figure out)

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 06:37):

And no, you were right: N needs to be positive (and it is also required to be positive in the .pdf). So there is no choice.

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:48):

@Filippo A. E. Nuccio If you add [hN : fact (0 < N)] as assumption, then hN.out (or hN.1) is a proof of 0 < N.

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:49):

And afterwards you just add [fact (0 < N)] to all lemmas that need it.

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:49):

Or you add it to a variables line, and then you need to change almost nothing, hopefully

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:53):

Otherwise, it behaves the same way as [group G] etc

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 07:04):

Thanks

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 07:06):

Johan Commelin said:

Or you add it to a variables line, and then you need to change almost nothing, hopefully

Well, but for this I thought it needed to be implicit. What is the difference between

variables (T : Type*) [add_monoid T]
lemma foo : (T : Type*) [add_monoid T] T = 0 :=

and simply

lemma foo : (T : Type*) [add_monoid T] T = 0 :=

Also, what is the difference between hN : 0 < N and [hN : fact (0 < N)] (i.e. : what's the magic in the word "fact")?

view this post on Zulip Johan Commelin (Mar 31 2021 at 07:09):

fact is a class, so you can use typeclass inference to automatically figure out those arguments.

view this post on Zulip Johan Commelin (Mar 31 2021 at 07:10):

With implicit, I thought you were talking about (N : nat) vs {N : nat}.

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 07:14):

Yes, I agree it was misleading (and, given the role played in the paper, I agree it needs to be explicit). Thank for the explanation of the fact as an instance. Is it the same for declaring variables at the beginning of sections/files? I thought this was only useful if wanting to leave things implicit, but if they're explicit in the statement, is there a point in setting up variables at the beginning?

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 09:04):

I am sorry but I'm unable to make this work. What I have now is

lem97_pos (N : nat) : blabla

and no variables. I can transform it in

lem97_pos (N : nat) (hN : 0 < N) : blabla

and then modify all calls to lem97_pos from apply lem_97pos \Lambda N to apply lem97_pos \Lambda N hN by adding hN : 0 < N to all statements relying on lem97_pos. But I guess you had a more clever solution...

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 09:11):

Forget: it worked! :octopus:

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 09:38):

Lemma 9.7 is now sorry-free.

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 09:39):

I have pushed to master the final proof and have moved the file into the toric folder. Two things left:
1) Add a couple of things to mathlib from the move section: I am going to create the PR straight away, when they'll be in mathlib I'll remove from them from the file.
2) Prove Gordan...

view this post on Zulip Johan Commelin (Mar 31 2021 at 09:43):

Filippo A. E. Nuccio said:

Lemma 9.7 is now sorry-free.

That's great!

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 09:52):

Well, actually there is a problem on line 250 of combinatorial_lemma, but this has nothing to do with lemma 9.7 (I realized this because I modified the final part of the file, where it calls lemma_97)

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 10:15):

(It occurs in the proof of lemma lem98_int)

view this post on Zulip Johan Commelin (Mar 31 2021 at 10:16):

Is this on your branch? master seems to compile just fine

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 11:00):

...hmm, let me update and build.

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 11:27):

Yes, everything is fine now!

view this post on Zulip Filippo A. E. Nuccio (Mar 31 2021 at 11:28):

I'll now PR a couple of things to mathlib, and then I will need to slow a bit to concentrate also on another project. But in the spare time I'd like to work on the fact that quotients of polyhedral lattices are still polyhedral lattices. Where is it?

view this post on Zulip Johan Commelin (Mar 31 2021 at 11:35):

It's not true in general. Only some specific quotients are...

view this post on Zulip Johan Commelin (Mar 31 2021 at 11:37):

polyhedral_lattice/cech.lean, there are 4 sorrys.

  • nr 1 will vanish when we have semi_normed_group quotients
  • nr 2 and 3 are the ones you are looking for
  • nr 4 is also a todo, shouldn't be too hard

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

I pushed \leanok to the blueprint! Green is taking over the graph (-;

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

Thanks again @Filippo A. E. Nuccio

view this post on Zulip Filippo A. E. Nuccio (Apr 01 2021 at 08:22):

I have just pushed a slightly improved version of lemma 9.7 avoiding PR anything to mathlib, as the results were too specific and could be golfed to two rw (thanks @Eric Wieser ).


Last updated: May 09 2021 at 16:20 UTC