Zulip Chat Archive

Stream: condensed mathematics

Topic: toric


view this post on Zulip Damiano Testa (Feb 28 2021 at 19:03):

An update from the toric branch.

I just pushed the latest version of toric: it has several sorries, but compiles. It also contains a full proof that the dual set of a ℤ-basis in a ℤ-lattice is pointed (i.e. intersects a hyperplane in just the origin). There is also a lemma that says that dual sets are (anti-)monotone, so it should be easy to show that the dual set of any set that contains a basis is pointed.

This is for ℤ-modules with a basis, which seem to work very well as a replacement to torsion free, finitely generated modules. There is no finite generation assumption, but there is the requirement of having a basis.

I would like this to work with fewer assumptions, but this is where I am at the moment. The good thing is that I think that this should work equally well over ℚ or ℝ, which should be the cases of interest for the applications to the liquid project!

view this post on Zulip Damiano Testa (Feb 28 2021 at 19:04):

There is still work to do to prove that saturated submonoids are finitely generated, but I consider it progress!

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

@Damiano Testa did a massive amount of work here, and it has just been merged into master

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

Be sure to git pull before working on master

view this post on Zulip Damiano Testa (Mar 30 2021 at 19:50):

I pushed a few more additions to the toric branch: it is not yet ready for unguided sorry-proving, but it is getting there!

view this post on Zulip Damiano Testa (Mar 30 2021 at 19:50):

I work more on it this week and hopefully soon I will be able to have sorrys that can be proven with minimal insider knowledge.

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 21:07):

I would like to help with Gordan's lemma! Do you think it's better to wait to have some more readable sorry or should I try to read the code now?

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

I was thinking that the statement of Gordan's lemma should end up in some of the toric file, and that it gets simply quoted in lem97. I think this would make it easier to adapt the form you'll prove to the one that I'm using. Do you agree? And, if yes, where would you suggest that I insert it?

view this post on Zulip Damiano Testa (Mar 31 2021 at 07:35):

Dear All,

I am very happy about the interest in Gordan's lemma! Part of the problem is that, while I write the steps in the proof, I confront myself with issues in the formalization and decide to change the approach. If you are willing to write a proof and then having to adapt it to a (hopefully slightly) different context, then feel free to remove sorrys from the file toric/towards_Gordan.lean (this is the toric folder in the toric branch).

However, I have had to change the setup a couple of times, since I was not able to make a few of the initial approaches work. This is quite possibly due to my own inability to use Lean, though!

I am trying to document towards_Gordan.lean in a systematic way, so that it should be easy to follow what the steps do, how they fit in the general proof and what are the important assumptions. If you can prove a lemma "close" to one of the stated ones, that might also be very useful!

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

And do you think towards_Gordan will eventually become Gordan (i.e. : I can insert the statement there and refer to it) or do you plan to have two files?

view this post on Zulip Damiano Testa (Mar 31 2021 at 07:38):

Filippo, I am now upgrading my branch to the current master. I will check the exact statement of Lemma 9.7 and will see how to fit it with what I have.

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

Thanks, at any rate I find it most reasonable to put what I use in the toric directory, and that I quote it from there. If the statement you end up with is not exactly the one I am using, we can write the bridge between the two there more easily, I guess.

view this post on Zulip Damiano Testa (Mar 31 2021 at 07:40):

Yes, at this stage, I am trying to get some Gordan-like statement proven. Once that is done, I am hoping that merging the proven one with the one that you used should be a simple matter.

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

The statement I am using is

lemma explicit_gordan (hΛ : finite_free Λ) [fintype ι] (l : ι  Λ) :
  (explicit_dual_set l).fg :=
sorry

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

where

def explicit_dual_set (l : ι  Λ) : submodule  (Λ →+ ) :=
{ carrier := {x |  i, 0  x (l i)},
  zero_mem' := λ i, le_rfl,
  add_mem' := λ x y hx hy i, add_nonneg (hx i) (hy i),
  smul_mem' := λ n x hx i, by { rw [add_monoid_hom.nat_smul_apply], exact nsmul_nonneg (hx i) n } }

view this post on Zulip Damiano Testa (Mar 31 2021 at 07:42):

Also, it does make sense to have the statement of Gordan's lemma in the toric folder.

I am building the toric branch now, with the master that I just merged.

view this post on Zulip Damiano Testa (Mar 31 2021 at 07:44):

Ok, I have not yet fixed the nat_submodule issue, but, apart from that, I am getting close to having the function l appearing in explicit_dual_set defined.

view this post on Zulip Damiano Testa (Mar 31 2021 at 07:46):

Ok, master merged with no issues into toric, leanproject build also only warned me about sorrys and I pushed again to the toric branch. There are no changes from what I pushed yesterday, except that it is now up to date with master.

view this post on Zulip Damiano Testa (Mar 31 2021 at 07:53):

... and CI is also happy with the branch! I also noticed a sign error in a doc-string and pushed the fix. This is just a change in a comment, so there should be no CI issues.

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 07:57):

I will try to read what you have done in the next days, so please don't hesitate to leave a lot of small sorry (even inside proofs!)... killing them is my favorite way of getting used to new stuff :big_smile:

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

Damiano Testa said:

Also, it does make sense to have the statement of Gordan's lemma in the toric folder.

I am building the toric branch now, with the master that I just merged.

Ok, are you going to put it somewhere and push to master? In that way, I can adapt my branch and when I'll push to master that part will be solid.

view this post on Zulip Damiano Testa (Mar 31 2021 at 08:01):

Riccardo, If you stick to the file towards_Gordan, the sorrys there should be provable (at least, this is my intention!). If you stray to a different file, you should also try to figure out if the statement is actually correct, since the sorrys outside of towards_Gordan are more of a playground, than actual steps in the formalization.

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 08:03):

I will have a look at towards_Gordan, thank you!

view this post on Zulip Damiano Testa (Mar 31 2021 at 08:12):

Filippo, maybe the best thing would be to simply move the file lem97.lean into the toric folder, just to sort lemmas by "semantic similarity". I still feel that I would like to have the option of tweaking the actual statement of Gordan's lemma to adapt it to what I feel is easier to formalize first, and worry about how to link it to what you have been using later. I really think that the glue should be some simple juggling with finite sets and coercions.

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

I agree, that it's best to formalize the statement that "falls out of all the preliminary work" and worry about the glue later.

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

You want to keep the coe-juggling in a small place. It shouldn't infect the rest of the story (-;

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

Oh I certainly agree it will be easy. OK, I will movelem97 in the toric folder leaving the explicit_gordan sorried. I'll be happy to come and help for the bridge once and if it will be needed. :bridge:

view this post on Zulip Peter Scholze (Mar 31 2021 at 08:29):

What is the math proof of Gordan's lemma that you are trying to formalize? The wikipedia one is nice but leaves most of the work implicit in using duality of cones. Is there a good complete textbook account of duality of (rational) cones that you follow?

view this post on Zulip Damiano Testa (Mar 31 2021 at 08:46):

I have patched together a proof, following partly the outline in Wikipedia.

Quickly, here is my strategy.

I have already proved a bunch of infrastructure to work with cones and duals, so that should be (mostly) in place.

  • Reduce to the case in which the dual is confined in an octant. This is achieved by making sure that the set of which you are taking the dual contains a basis.
  • Prove that the "extremal rays" are indexes by (some) subsets of the set of which you are taking the dual. This is mostly a matter of making the definition of "extremal rays" and "1-dimensional subcone" match up.
  • Once you have finitely many extremal rays, what is left is a form of saturation. This will be filled in by taking linear combinations of the extremal rays with rational coefficients in [0,1] and intersecting with the lattice. Here, the main finiteness condition will follow from intersecting a (pre-)compact set with a discrete one.

view this post on Zulip Damiano Testa (Mar 31 2021 at 08:47):

From a formalization point of view, I am trying to make the transitions between linear combinations with coefficients in ℕ, ℤ, ℚ or ℝ be as smooth as possible, since they all play some partial role in the argument.

view this post on Zulip Damiano Testa (Mar 31 2021 at 08:49):

While this feels to be within my "formalization grasp", I also find it challenging!

view this post on Zulip Peter Scholze (Mar 31 2021 at 09:22):

@Damiano Testa OK, sounds great!

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 21:11):

I have proved reduction_to_lattice here
https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/toric/towards_Gordan.lean
There is something I don't understand in the proof: I have the impression that the hypothesis I called goal is exactly what we want to prove, but exact goal doesn't work. If you try to play with it it's very easy to get to a point where you need to prove foo and you have foo in the local context, but there should be some problem with possibly different -actions. If someone wants to play with it feel free to modify it... at the moment it is very ugly.

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2021 at 21:17):

Perhaps you've tried it already, but in that situation I often use tactic#convert to show what Lean is having trouble with.

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 21:21):

I did it, in line 80. The goal becomes

(λ (i : fin n), g i  b i) = λ (i : fin n), g i  b i

After ext i the goal becomes

(g i  b i) = (g i  b i)

I proved this by induction on g i, that is an integer. The proof worked because essentially zero_smul add_smul,sub_smul and one_smul work for any , but I don't know how to do it better.

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2021 at 21:23):

Ah, sorry, I hadn't looked at the proof yet!

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 21:25):

It must have something to to with coercion from Λ₁ to submodules of V, or something like that.

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2021 at 21:25):

Hmm, is it something that norm_cast should be helping with?

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 21:26):

Let me see

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 21:36):

Hmm, it does something, but it doesn't really change the proof

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 21:46):

Ah! A combination of norm_cast and congr simplified the proof quite a lot

view this post on Zulip Riccardo Brasca (Mar 31 2021 at 22:36):

The proof is now reasonably small, even if there still is something I don't understand completely. If it's OK for @Damiano Testa I will push it into toric.

view this post on Zulip Damiano Testa (Apr 01 2021 at 03:19):

@Riccardo Brasca thank you very much for your help!

Feel free to push your proof to toric!

I have not looked at it, but I suspect that the issues that you mention have to do with Lean finding it tricky to convert between \Z and \Q.

In any case, any proof is the same as any other proof in Lean!

view this post on Zulip Damiano Testa (Apr 01 2021 at 04:27):

Ok, I took a look at this and I could golf it slightly, mostly by extracting a part of the proof to something more general:

-- general fact, also asked in mathlib
lemma algebra_map.injective.linear_independent {R S M ι : Type*} [comm_semiring R] [semiring S]
  [add_comm_monoid M] [algebra R S] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
  (hinj : function.injective (algebra_map R S)) {v : ι  M} (li : linear_independent S v) :
  linear_independent R v :=
begin
  refine linear_independent_iff'.mpr (λ s g hg i hi, hinj (eq.trans _ (ring_hom.map_zero _).symm)),
  refine (((@linear_independent_iff' _ _ _ v _ _ _).mp li) _ _ _) i hi,
  simp_rw algebra_map_smul,
  exact hg,
end

-- marginally shorter proof
lemma reduction_to_lattice (s : submodule  V) (bv : is_basis  v) :
   (n : ) (vn : fin n  s.restrict_scalars   submodule.span  (set.range v)),
  is_basis  vn :=
begin
  obtain n, b, hb :=
    submodule.exists_is_basis_of_le_span (_ : linear_independent  v) inf_le_right,
  { refine n, b, _, by convert hb.2⟩⟩,
    replace hb := hb.1,
    rw [linear_independent_iff'] at  hb,
    intros t g hg i hi,
    refine hb t g _ i hi,
    convert hg,
    ext i,
    erw [submodule.coe_smul_of_tower, submodule.coe_smul_of_tower, algebra_map_smul] },
  { refine algebra_map.injective.linear_independent _ bv.1,
    exact λ a b ab, int.cast_inj.mp ab }
end

view this post on Zulip Damiano Testa (Apr 01 2021 at 04:29):

It may be that the main weirdness in the proof is that is_scalar_tower ℤ ℚ V and the coercion from ℤ to ℚ do not recognize each other.... maybe.

view this post on Zulip Johan Commelin (Apr 01 2021 at 05:04):

I think that sometimes you can have aux : int.module \Z = ring.to_module \Z (or something like that). The proof of that have will be subsingleton.elim. And after that, you can rw aux so that all the scalar multiplications are now really the same.

view this post on Zulip Johan Commelin (Apr 01 2021 at 05:04):

But I agree that this is an annoying side effect of (conf)using abelian groups and Z-modules.

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:08):

Ok, analyzing this further, in the erw step there are two submodule.coe_smul_of_tower: the first one, changes

(g i  b i) --> g i • ↑(b i)

but the second one, changes

(g i  b i) --> ⇑(algebra_map ℤ ℤ) (g i) • ↑(b i)

maybe this is the issue?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 05:11):

Can this boil down to the non-defeq diamond of the Z-module over itself:

import algebra.module.basic

example : @add_comm_group.int_module.{0} int (@ring.to_add_comm_group _ int.ring) =
  @semiring.to_semimodule.{0} int
    (@comm_semiring.to_semiring.{0} int (@comm_ring.to_comm_semiring.{0} int int.comm_ring)) := rfl -- unfortunately not rfl right now

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:12):

Johan, I am trying with your suggestion, but I might be missing an import, since Lean does recognize neither int.module nor ring.to_module!

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:13):

Yakov, it may be, but I am really not sure what is going on... Even with the widgets, the pieces of the terms look identical quite a long way down.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 05:14):

Can you try int_module and semiring.to_semimodule instead?

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:14):

with int_module I still get unknown identifier 'int_module'.

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:15):

(however, lean recognized semiring.to_semimodule)

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 05:16):

@add_comm_group.int_module \Z (by apply_instance)

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:18):

Lean considers this a valid statement:

have aux : @add_comm_group.int_module  (by apply_instance) = semiring.to_semimodule,
sorry,

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:19):

But I am not sure how to use it afterwards (nor how to prove it).

Johan did say how to prove it:

have aux : @add_comm_group.int_module  (by apply_instance) = semiring.to_semimodule :=
subsingleton.elim _ _,

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 05:21):

When you get to your seemingly identical goal, convert rfl should work now, hopefully with convert pulling in this hypothesis. Or try simp_rw aux as Johan suggested above.

view this post on Zulip Johan Commelin (Apr 01 2021 at 05:23):

In several files on polyhedral lattices, I disabled the add_comm_group.int_module instance at the top of the file, forcing Lean (and myself) to work explicitly with Z\Z-modules.

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:25):

I tried simp_rw at * at each line in the proof, followed by assumption, solve_by_elim or exact ... and it did not seem to work. I will try with convert rfl now!

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:27):

convert rfl either leaves the goal unchanged (at least in the infoview, I did not check if it changed some parts of the terms that is not "just visible"), or it introduces a has_lift_t.lift.

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:30):

I just read Johan's freestyle post: I guess that I am doing the exact opposite here... :upside_down:

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 05:34):

@Damiano Testa do you have this on a branch? I'll take a look

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 05:46):

If I understand correctly, the issue is the error at this lemma and proof:

lemma reduction_to_lattice (s : submodule  V) :
   (n : ) (vn : fin n  s.restrict_scalars   submodule.span  (set.range v)),
  is_basis  vn :=
begin
  have hind : linear_independent  v,
  { replace bv := bv.1,
    rw [linear_independent_iff'] at  bv,
    intros s g hg i hi,
    have H :  (i : ι), ((g i) : )  v i = (g i)  v i,
    { intro i,
      rw [ gsmul_eq_smul, gsmul_eq_smul_cast _ _] },
    have hg' : s.sum (λ (i : ι), (λ (i : ι), ((g i) : )) i  v i) = 0,
    { simp only [H, hg]},
    simpa using bv s (λ i, g i) hg' i hi },
  --The RHS seems to be the statement we want, but some work is needed
  obtain n, b, hb := submodule.exists_is_basis_of_le_span hind inf_le_right,
  refine n, b, _, by convert hb.2⟩⟩,
  replace hb := hb.1,
  exact hb
end

view this post on Zulip Damiano Testa (Apr 01 2021 at 05:48):

Sorry, having breakfast!

Yakov, that is the alto error [weird autocorrect], though!

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:37):

The issue isn't in the int_module but rather int.semiring vs

            (@ring.to_semiring 
               (@domain.to_ring 
                  (@integral_domain.to_domain 
                     (@linear_ordered_comm_ring.to_integral_domain  int.linear_ordered_comm_ring))))

and related

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:41):

Doing local attribute [-instance] int.semiring int.ring int.comm_semiring results in the following diamond as an issue:

           (@ring.to_semiring 
              (@domain.to_ring 
                 (@integral_domain.to_domain 
                    (@linear_ordered_comm_ring.to_integral_domain  int.linear_ordered_comm_ring))))

vs

           (@ring.to_semiring 
              (@ordered_ring.to_ring 
                 (@linear_ordered_ring.to_ordered_ring 
                    (@linear_ordered_comm_ring.to_linear_ordered_ring  int.linear_ordered_comm_ring))))

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:41):

Ok, this is now not so much about this special case, but in general, does it mean that there is a missing instance somewhere? A missing proof? What constitutes a "good, structural way" of fixing these issues?

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:44):

So, should Lean be forbidden to use that int is an integral domain?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:44):

Although in a mathlib repo I have, it seems

example :
  (@ring.to_semiring 
    (@domain.to_ring 
        (@integral_domain.to_domain 
          (@linear_ordered_comm_ring.to_integral_domain  int.linear_ordered_comm_ring)))) =
  (@ring.to_semiring 
    (@ordered_ring.to_ring 
        (@linear_ordered_ring.to_ordered_ring 
          (@linear_ordered_comm_ring.to_linear_ordered_ring  int.linear_ordered_comm_ring)))) := rfl

works fine

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:46):

I copy pasted your example in the file that I have with the convoluted proof and Lean accepts it there as well.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:47):

OK so one can see the issue earlier in the gordon lemma proof

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:47):

Consider this tactic step:

  refine n, b, _, by convert hb.2⟩⟩,

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:47):

Switching it to just

  refine n, b, _⟩,

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:47):

We can see a difference between the hypothesis hb and the goal

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:47):

image.png

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:48):

image.png

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:48):

I see: ordered_ring vs domain.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:49):

Right. So why is it unhappy? And, even though it is unhappy, is there a way to get the exists_is_basis_of_le_span to use the "correct" ring as a workaround?

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:49):

It is funny, but in the other stuff that I was doing in a similar vein, I had separate assumptions:

  • one to work with regular elements (close to integrality conditions) and
  • one with non-negative stuff (close to orders).

I am impressed that Lean picks up on this also in this case!

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:50):

One issue with exists_is_basis_of_le_span as it is right now is there is a free metavariable

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:51):

So, are you suggesting that an @ and underscore-fest might solve this?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:51):

Specifically, which submodule \Z V is on the left of the \inf.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:51):

Could be? I'm not sure yet.

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:53):

Let me try to work this out.

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:54):

(Just an observation -- you found the source of the integral_domain: it is the assumption coming from exists_is_basis_of_le_span!)

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:57):

I am tempted to say that it is this one:

submodule.restrict_scalars  s

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:58):

What about that submodule?

view this post on Zulip Damiano Testa (Apr 01 2021 at 06:58):

I think that this is the submodule that is implicit, no?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 06:59):

Yes, that's right. I'm just trying to slay little things that might get in the way, process of elimination

view this post on Zulip Damiano Testa (Apr 01 2021 at 07:01):

There is indeed a hidden goal, after the obtain step: there are three goals after it, but only two need to be proven, since one disappears. I think that it disappears when Lean realizes that the module is what I wrote above. At least, this is my interpretation!

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 07:02):

Yes, agreed. I am still not sure why the integral_domain > domain > ring < comm_ring < integral_domain diamond seems to be getting in the way

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 07:03):

(that is, even after getting rid of the other ring instances)

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 07:18):

I see that you are playing with more or less what I did yesterday (with a far better understanding :)
I don't know if this is relevant, but my first attempt to prove the proposition was to start like this (before realizing there is submodule.exists_is_basis_of_le_span)

lemma reduction_to_lattice (s : submodule  V) :
   (n : ) (vn : fin n  s.restrict_scalars   submodule.span  (set.range v)),
  is_basis  vn :=
begin
  let Λ := submodule.span  (set.range v),
  let w : ι  Λ := λ i, v i, submodule.subset_span (set.mem_range_self _)⟩,
  have hind : linear_independent  w := sorry --this is OK
  have hbasis : is_basis  w := is_basis_span hind, --this is not OK
end

view this post on Zulip Damiano Testa (Apr 01 2021 at 07:19):

Actually, the proof feels like it could be simply:

  convert submodule.exists_is_basis_of_le_span
    ((by { refine algebra_map.injective.linear_independent _ bv.1, exact λ a b ab, int.cast_inj.mp ab })) (@inf_le_right _ _ (submodule.restrict_scalars  s) _),

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 07:20):

So my idea was to prove that Λ is free, the basis should of course be w. Now, proving that w is linear independent is easy... but I wasn't able to prove that it is a spanning set, and if you try you see immediately what goes wrong.

view this post on Zulip Damiano Testa (Apr 01 2021 at 07:21):

since the resulting goal of this looks like the equality of two "identical" terms: the only apparent difference seems to be the choice of symbol for the exists variable.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 07:23):

Ah there is another difference

view this post on Zulip Damiano Testa (Apr 01 2021 at 07:23):

This is all very weird and I am getting the impression that the difficulty is generated by working with "explicit" types, like ℤ and ℚ.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 07:23):

Not sure if it is a meaningful one

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 07:24):

submodule.has_inf vs semilattice_inf.to_has_inf (submodule ℤ V)

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 07:29):

Those are also rfl =/

view this post on Zulip Damiano Testa (Apr 01 2021 at 07:31):

Hmm, I have a feeling that these "just work" since they are contained in the part that "disappears" in the proof. I take this to mean that Lean correctly understand what we are saying and moves on, right?

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 07:39):

Do you have a #mwe of what goes wrong, hopefully just mathlib dependent but otherwise I'll clone LTE?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 07:42):

import linear_algebra.free_module

lemma algebra_map.injective.linear_independent {R S M ι : Type*} [comm_semiring R] [semiring S]
  [add_comm_monoid M] [algebra R S] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
  (hinj : function.injective (algebra_map R S)) {v : ι  M} (li : linear_independent S v) :
  linear_independent R v :=
begin
  refine linear_independent_iff'.mpr (λ s g hg i hi, hinj (eq.trans _ (ring_hom.map_zero _).symm)),
  refine (((@linear_independent_iff' _ _ _ v _ _ _).mp li) _ _ _) i hi,
  simp_rw algebra_map_smul,
  exact hg,
end

variables {V ι : Type*} [add_comm_group V] [semimodule  V] [fintype ι] {v : ι  V}
  (bv : is_basis  v)
include bv
lemma reduction_to_lattice (s : submodule  V) :
   (n : ) (vn : fin n  s.restrict_scalars   submodule.span  (set.range v)),
  is_basis  vn :=
begin
  obtain n, b, hb := submodule.exists_is_basis_of_le_span
    ((by { refine algebra_map.injective.linear_independent _ bv.1, exact λ a b ab, int.cast_inj.mp ab }))
    (@inf_le_right _ _ (submodule.restrict_scalars  s) _),
  refine n, b, _⟩,
  exact hb -- :C
end

view this post on Zulip Damiano Testa (Apr 01 2021 at 07:43):

Alternatively, you could also hope to finish the proof earlier:

lemma reduction_to_lattice (s : submodule  V) (bv : is_basis  v) :
   (n : ) (vn : fin n  s.restrict_scalars   submodule.span  (set.range v)),
  is_basis  vn :=
begin
  convert submodule.exists_is_basis_of_le_span
    ((by { refine algebra_map.injective.linear_independent _ bv.1, exact λ a b ab, int.cast_inj.mp ab }))
    (@inf_le_right _ _ (submodule.restrict_scalars  s) _),
  refl, -- does not work
end

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 07:45):

Thanks!

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 07:49):

First comment: it's probably coming from add_comm_group.int_module, which is not defeq to other int actions. Indeed, if you disable it with

local attribute [-instance] add_comm_group.int_module

at the start of your mwe, then Lean does not understand the statement of the second lemma any more. So it has to be used somewehere.

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 08:24):

Here is a working proof:

import linear_algebra.free_module

local attribute [-instance] add_comm_group.int_module

lemma algebra_map.injective.linear_independent {R S M ι : Type*} [comm_semiring R] [semiring S]
  [add_comm_monoid M] [algebra R S] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
  (hinj : function.injective (algebra_map R S)) {v : ι  M} (li : linear_independent S v) :
  linear_independent R v :=
begin
  refine linear_independent_iff'.mpr (λ s g hg i hi, hinj (eq.trans _ (ring_hom.map_zero _).symm)),
  refine (((@linear_independent_iff' _ _ _ v _ _ _).mp li) _ _ _) i hi,
  simp_rw algebra_map_smul,
  exact hg,
end

variables {V ι : Type*} [add_comm_group V] [semimodule  V] [semimodule  V]
  [is_scalar_tower   V] [fintype ι] {v : ι  V}
  (bv : is_basis  v)
include bv

set_option profiler true

lemma reduction_to_lattice (s : submodule  V) :
   (n : ) (vn : fin n  s.restrict_scalars   submodule.span  (set.range v)),
  is_basis  vn :=
begin
  have A : function.injective (algebra_map  ) := λ a b ab, int.cast_inj.mp ab,
  have B := algebra_map.injective.linear_independent A bv.1,
  obtain n, b, hb :=
    submodule.exists_is_basis_of_le_span B (@inf_le_right _ _ (submodule.restrict_scalars  s) _),
  refine n, b, _⟩,
  convert hb,
end

I disabled add_comm_group.int_module, and instead assumed [semimodule ℤ V] [is_scalar_tower ℤ ℚ V] to make sure that we did not use the bad int module structure, and instead used a generic one.

But: the proof is way too slow (62s on my computer), so this is not acceptable.

view this post on Zulip Damiano Testa (Apr 01 2021 at 08:27):

Thanks Sébastien! This is looking much better (albeit slow) now!

While we are at it, I wanted your A statement to be already in mathlib, but I could not find it: is it hiding in there somewhere?

[Also, on my computer the proof is so slow that it times out...]

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 08:37):

Yes, the proof is clearly wrong now. I'm not able to find the culprit for now, sorry...

view this post on Zulip Kevin Buzzard (Apr 01 2021 at 08:44):

Even convert hb using 1 takes time (essentially the same amount of time as far as I can see).

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 08:55):

Minimal diamond:

import linear_algebra.free_module

lemma foo : algebra.id  = algebra_int  := rfl -- fails

both instances are registered in mathlib.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 08:56):

I tried turning -instance algebra_int off but that hadn't helped in my experiments.

view this post on Zulip Johan Commelin (Apr 01 2021 at 09:03):

We need a better way to deal with these "initial objects"

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 09:03):

The thing is that these instances are used in other files when defining various objects, so it is already too late. Maybe changing algebra.id to something nicer would help (expanding the fields instead of relying on an abstract construction).

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 17:47):

I played a little bit more with this. My conclusion is that "Yury's rule of thumb" for decidable instances should also apply in this situation. We need to find a better name for this rule, but it amounts to: "in a context where there is a subsingleton with data, and several natural instances of it which are not defeq, then mention the instance explicitly in theorems that use it".

As @Eric Wieser has pointed out several times, we are exactly in this situation here. For instance, if E and F are two add_comm_group, then they are both -modules, and then you get two non-defeq module instances on E x F, the one coming from the add_comm_group instance and the one coming from the module product instance. And there is no way to make these defeq.

A solution is to not register add_comm_group.nat_semimodule as a global instance, and only use it when needed in proofs, and use suitable typeclass assumptions in statements. (Or register it as a global instance, but only once we are sure that it's not used in statements, and only to make it available for proofs -- this could probably be enforced by a linter). I had a go at refactoring mathlib along these lines, to see how things go. The good news is that, with this refactor, the above problem in this thread completely disappears, i.e., no need for convert or whatever. And a few proofs that were painful because of instance mismatch become smoother. The bad news is that I'm not done fixing it, because there are many places where the previous instance is used. My work in progress is in the branch branch#gsmul_instance, if anyone wants to have a look/fix a few proofs.

view this post on Zulip Johan Commelin (Apr 01 2021 at 18:06):

@Sebastien Gouezel thanks a lot for all your debugging, and your efforts for refactoring!

view this post on Zulip Johan Commelin (Apr 01 2021 at 18:06):

I'm coming around to these ideas of disabling these global instances

view this post on Zulip Damiano Testa (Apr 01 2021 at 18:09):

Sébastien, thank you so much for looking into this! I am only superficially following the discussion, but I find it interesting to see how much I am used to abuse notations and definitions and how Lean picks up on it!

view this post on Zulip Eric Wieser (Apr 01 2021 at 18:38):

Another option would be to use gsmul and nsmul in lemma statements, and convert to smul and back inside the lemma

view this post on Zulip Sebastien Gouezel (Apr 01 2021 at 18:41):

The problem with gsmul and nsmul is that all the linear algebra lemmas do not apply (for instance, when you want to use the fact that a linear map satisfies f (c • v) = c • f v, this won't work out of the box for gsmul). So they are really a pain to use together with linear algebra.

view this post on Zulip Johan Commelin (Apr 01 2021 at 19:04):

Somehow, in LTE we're in this weird limbo, where we use additive group homomorphisms, but also scalar multiplication.

view this post on Zulip Johan Commelin (Apr 01 2021 at 19:05):

And one of my reasons is extremely mundane: the notation for scalar multiplication is just nicer than gsmul/nsmul. And at the same time the notation for group homs looks better than that for linear maps (especially if you are just working with Z-modules anyway).

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 20:41):

I've uploaded here
https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/toric/towards_Gordan.lean
a proof of pre_generators_finite. I am little tired to golf it, but as usual if someone wants to play with it no problem.

The idea of the proof is very simple: the function i takes a pre_generator g and sends it to the set t of the definition. Since t ⊆ s and s is finite, it is enough to prove that i is injective. The mathematical proof is between the lines 197 and 218. The rest of the proof is me fighting against classical.some and the fact that to use fintype.of_injective the codomain of i must be set s, but morally the "true" codomain, where it's easier to work, is set M.

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 20:43):

Note that here the problem is my inexperience, Lean seems innocent.

view this post on Zulip Kevin Buzzard (Apr 01 2021 at 21:29):

What I am still confused/surprised about is that surely all of these issues were experienced by people using Coq or Agda or UniMath or whatever?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 22:04):

Do you have to say fintype? Or can you just prove set.finite pre_generators f s when set.finite s?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 22:05):

Because you get noncomputable fintype from set.finite anyway

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 22:05):

And then you don't have to juggle sort coercions

view this post on Zulip Riccardo Brasca (Apr 01 2021 at 22:11):

I don't know, @Damiano Testa wrote the statement and I didn't want to modify it... my current goal is just to get familiar with convex geometry in Lean

view this post on Zulip Johan Commelin (Apr 02 2021 at 04:35):

Yakov Pechersky said:

Do you have to say fintype? Or can you just prove set.finite pre_generators f s when set.finite s?

That sounds like it might help. (But I haven't looked at the code yet.)

view this post on Zulip Damiano Testa (Apr 02 2021 at 05:23):

I have not finished writing a full proof, so the stuff in towards_Gordan is still subject to change. However, I try to give indications of what is important in each statement in the doc-strings above each lemma. If a change in an assumption makes the proof simpler, and leaves the statement "essentially the same", feel free to go for it!

Some of these statements might have to be changed anyways, since I decided to go for a full sorry-explosion, rather than figuring out what the best way of doing things is step-by-step.

view this post on Zulip Damiano Testa (Apr 02 2021 at 05:24):

What I do try, though, is to make the statements "true": hopefully this also makes them provable! :upside_down:

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:02):

Also, the reason I used fintype is because I read somewhere that fintypes were easier than finsets. If set.finite is even easier, then I would probably change finiteness assumptions everywhere to set.finite!

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:11):

My understanding is that the power of finset and fintype is their computability. If you're going to already mark it as noncomputable, then you can make your statements be about set.finite because of docs#set.finite.fintype, which will give you a noncomputable fintype anyway

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:12):

Because set.finite s is just nonempty (fintype s)

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:18):

Ok, from nonempty (fintype s) I would deduce that s is going to be non-empty? I am not sure if I like this: I am usually careful about including the empty set in my statements, excluding it only when the statement is false for the empty set. The possibility of having an empty set is often simplifying for proofs.

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:19):

Ah, maybe the nonempty is simply the assertion that there is a fintype structure on s, possibly with s being the empty finset?

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:24):

You don't have to unfold what set.finite is to prove things about it, which is what's nice. I don't know if the relevant lemmas get easier to prove in that API. But I'd think anything that can be proven about fintype implying fintype should be easier across set.finite, and if it isn't, then that's missing API.

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:33):

Ok, I will try to replace fintype with set.finite!

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:38):

So, the expectation is that this statement

lemma fg_with_basis (vm : ι  M) (hf : is_full_on f v vm) {s : set M} (hs : (set.range vm)  s) :
   g : set N, set.finite g  dual_set nat_submodule f s = submodule.span  g :=

should be easier than

lemma fg_with_basis (vm : ι  M) (hf : is_full_on f v vm) {s : set M} (hs : (set.range vm)  s) :
   g : finset N, dual_set nat_submodule f s = submodule.span  g :=

right? (The only intended difference is in the properties of the asserted existence of g.)

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:39):

Yeah, possibly

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:40):

Ok, I pushed the change.

Thanks!

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:40):

As long as it is not likely harder, I am happy to go with whatever!

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:40):

And something like this (if one really wanted to refactor the lemma):

lemma pre_generators_finite (bv : is_basis  v) (s : set M) (hs : s.finite) :
  (pre_generators f s).finite :=

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:41):

Ah, I used

lemma pre_generators_finite (s : set M) (fs : set.finite s) : set.finite (pre_generators f s) :=

which should simply be your version, without taking advantage of dot-notation, right? :smile:

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:42):

(There is an include bv in the file that I am using.)

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:42):

Yeah. For example, this is the goal after these steps

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:43):

(However, I suspect that bv plays no role in the proof.)

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:43):

lemma pre_generators_finite (bv : is_basis  v) (s : set M) (hs : s.finite) :
  (pre_generators f s).finite :=
begin
  rw pre_generators,
  simp_rw [submodule.ext'_iff, set.ext_iff, submodule.mem_coe, mem_dual_set],
  /-
  {c : N |
    (∀ (m : M), m ∈ s → ⇑(⇑f m) c ∈ nat_submodule) ∧
    ∃ (t : set M) (H : t ⊆ s), ∀ (x : N),
      (∀ (m : M), m ∈ {1, -1} • t → ⇑(⇑f m) x ∈ nat_submodule) ↔ x ∈ submodule.span ℕ {c}}.finite
  -/
  sorry
end

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:44):

In my version, the simp_rw submodule.ext'_iff does not work:

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:45):

Then you can use things like

  refine set.finite.subset _ (set.inter_subset_right _ _),

to prove finiteness solely on the right hand side of the condition, if that is sufficient

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:45):

invalid simplification lemma 'submodule.ext'_iff' (use command 'set_option trace.simp_lemmas true' for more details)

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:45):

which branch are you on?

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:46):

I am on toric, the one that I just pushed.

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:51):

Ok, looking at the proof that Riccardo wrote, I think that it should make use of is_cyclic. This probably means that I should change the definition of pre_generators. This will probably make the coercion to type of a set simpler, by going via a subtype instead.

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:52):

However, I will not have time to do this before Monday: I have some non-Lean Easter plans!

view this post on Zulip Damiano Testa (Apr 02 2021 at 06:53):

Thank you all for your feedback: I really have the impression that we are making good progress on Gordan's lemma!

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:57):

The ext'_iff lemma is now a part of set_like after a refactor

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 06:59):

Now it would be simp_rw [@set_like.ext_iff (submodule ℕ N) N]

view this post on Zulip Riccardo Brasca (Apr 02 2021 at 07:58):

@Damiano Testa If you happy with set.finite I can do it.

view this post on Zulip Riccardo Brasca (Apr 02 2021 at 07:59):

BTW I use bv to prove that M is torsion free.

view this post on Zulip Damiano Testa (Apr 02 2021 at 09:07):

I think that the version that I pushed to toric has set.finite and also your proof of the reduction to Z.

I need to think about bv: I did not think that it was needed, but it is an important assumption for the final result anyway!

view this post on Zulip Riccardo Brasca (Apr 02 2021 at 09:22):

My mathematical proof is the following: I have to prove that a pre_generator g is determined by the subset t of the definition. If g₁ and g₂ are associated to the same subset, then submodule.span ℕ {g₁} = submodule.span ℕ {g₂}, by definition. So there are a b : ℕ such that g₁ = a • g₂ and g₂ = b • g₁ so g₁ = a • b • g₁ = (a * b) • g₁. Now I want a * b = 1 (or g₁ = 0), and here is where I used torsion freeness.

view this post on Zulip Riccardo Brasca (Apr 02 2021 at 10:43):

I pushed to toric the new proof of pre_generators_finite. It is indeed better then before. For some reason I am not able to define i using if then else and so I did it in tactic mode.

view this post on Zulip Sebastien Gouezel (Apr 02 2021 at 14:18):

Sebastien Gouezel said:

A solution is to not register add_comm_group.nat_semimodule as a global instance, and only use it when needed in proofs, and use suitable typeclass assumptions in statements. (Or register it as a global instance, but only once we are sure that it's not used in statements, and only to make it available for proofs -- this could probably be enforced by a linter). I had a go at refactoring mathlib along these lines, to see how things go. The good news is that, with this refactor, the above problem in this thread completely disappears, i.e., no need for convert or whatever. And a few proofs that were painful because of instance mismatch become smoother. The bad news is that I'm not done fixing it, because there are many places where the previous instance is used. My work in progress is in the branch branch#gsmul_instance, if anyone wants to have a look/fix a few proofs.

I have worked a bit more on this. Now, I am stuck in Witt vectors, where there is a tactic to be adjusted and I don't know anything about tactics. Or maybe set a global instance for all these files. An expert look would be most welcome :-)

view this post on Zulip Sebastien Gouezel (Apr 02 2021 at 15:04):

Never mind, problem solved :-)

view this post on Zulip Johan Commelin (Apr 02 2021 at 18:46):

Wow, I'm glad it is already solved! Otherwise, I would certainly have tried to help.

view this post on Zulip Johan Commelin (Apr 02 2021 at 18:46):

I feel somewhat responsible for maintaining Witt vectors (-;

view this post on Zulip Damiano Testa (Apr 02 2021 at 19:57):

Riccardo, this is also more or less what I had in mind and it is certain sufficient for the application to Gordan's lemma. You could probably get away without bv, observing that a cyclic nat module has finitely many generators (1, if it is infinite and ϕ(n)\phi (n) if it has nn elements). However, it might be better to observe that there are finitely many subsets that produce a cyclic module and bypass the second issue altogether!

view this post on Zulip Sebastien Gouezel (Apr 02 2021 at 19:57):

Well, not everything is solved in the Witt vectors part yet, which is probably the most painful part for now :-) I wanted to see how much work it would be to make the change, and it is much more than I expected -- which is a sign that mathlib is now pretty big, in fact big enough that such refactors become nontrivial.

view this post on Zulip Johan Commelin (Apr 03 2021 at 05:44):

@Sebastien Gouezel I think I figured out how to fix the tactic in Witt vectors

view this post on Zulip Johan Commelin (Apr 03 2021 at 05:44):

You need an extra intro to take care of the algebra instance.

view this post on Zulip Johan Commelin (Apr 03 2021 at 06:01):

I've pushed a bunch of fixes. We need to add an instance algebra int (zmod n). I haven't done that yet, but it should fix the remaining problems (I hope!)

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

Pushed that instance for zmod, let's see what CI thinks of it.

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 15:58):

OK I am trying to get on top of this Gordan's Lemma thing. As far as I can see, in master we have a file toric/lem97.lean which contains a complete proof of Lemma 9.7 of analytic.pdf modulo

lemma explicit_gordan (hΛ : finite_free Λ) [fintype ι] (l : ι  Λ) :
  (explicit_dual_set l).fg :=
sorry

Here Λ\Lambda is a finite free Z\Z-module, andexplicit_dual_set l is the sub-N\mathbb{N}-module of Λ:=Hom(Λ,Z)\Lambda^*:=Hom(\Lambda,\Z) consisting of things which pair to something non-negative with the image of l; the claim is that it's finitely-generated as an N\mathbb{N}-module. Clearly explicit_gordan is what we should be aiming for.

I've been trying to make some sense of the toric branch, which right now contains quite a lot of what seems to me to be dead code and commented code. I've made a couple of recent commits to this branch adding some docstrings, although right now it seems to me like the branch is more like an experimental playground rather than something which will ultimately be merged into master -- which is fine, we have branches of mathlib which are like this, and when stuff is working then it gets migrated into new branches which get PR'ed. I'm kind of guessing that this is the plan here too.

What I cannot extract from this branch right now is where we are going. I talked to Damiano yesterday and my understanding is that the formalisation of the proof of Gordan's Lemma is going on in the file toric.towards_Gordan on the toric branch. I note with a little concern that it's not actually proving the precise statement which we need in lem97 though, and sometimes glue is harder than you think. But my main concern is that I cannot see the wood for the trees right now and if I don't know what we're formalising then it's hard to jump in.

So I propose making a mini-blueprint to explain where we're going. There are a whole bunch of comments in toric.towards_Gordan which Damiano said might help but right now they're not enough for me (I don't know much at all about toric geometry though).

I have uploaded a file toric/gordan_blueprint.tex to the toric branch, which right now is a bunch of questions about stuff on the toric branch and nowhere near a mathematical proof. If someone (@Damiano Testa or @Riccardo Brasca or @Filippo A. E. Nuccio -- you seem to be the active contributors to this branch) can perhaps turn this tex sketch into a mathematical proof -- forget the formalisation for now -- then we can perhaps decide how best to formalise it. Is there a proof you guys have in mind?

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 16:06):

I've just googled around a bit. Is the idea that we're formalising the "topological proof" in Wikipedia?

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 16:44):

I'm not entirely sure I understand the Wikipedia proof right now. Is it using some result of the form "double dual of a fg cone (:= nnreal-submodule) in a real vector space is itself? Or maybe "dual of an fg cone is fg"? Are these things obvious?

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:45):

Dear Kevin,

thank you very much for your effort! I am not sure that I will have time to work on this right now, but I will take a serious look next week.

I have been making PRs to mathlib as I was going along, to move the more "stable" part. For this reason, the stuff left in toric is less coherent. I have started making the file towards_Gordan with the idea of making it a path towards a proof of Gordan's lemma, but I feel that it became "public" a little too early.

I have had conversations with Johan about the "glue" and he also agreed that what will come out of the toric branch should be easily converted to what is the explicit Gordan statement. I was trying to prepare the towards_Gordan file to a level that was usable to someone who did not know the proof of Gordan's lemma, but, given Kevin's unsuccessful effort, I am not done doing it!

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:46):

Yes, the proof that I am formalising is close to the topological proof in wikipedia. I gave a very rough outline of the main steps in a conversation with Peter, let me fetch it!

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:47):

This is an outline:

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/toric/near/232555538

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 16:54):

What is an "octant" and what is an "extremal ray"?

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:54):

"Octant" (in a vector space/Z-module) is the set of all vectors with non-negative coordinates, with respect to a basis.

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:56):

In the Lean formalization is what I would have called pointed, except that you noticed that the definition was not correct. Luckily, I had not started using this. The good thing about "octants" (or nat-submodules of octants), is that they have finitely many extremal rays. (Which I am now going to define.)

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:56):

An extremal ray is a one-dimensional subcone of a cone with the property that is c d are in the cone and c + d is in the extremal ray, then c and d are actually already in the extremal ray.

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:58):

In intuitive terms, extremal rays are the "edges" of the cone.

What should be proved is that the elements of the cone are in the convex hull of the extremal rays... up to saturation. Thus, we should prove that there are finitely many extremal rays and that the saturation only adds finitely many more elements.

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:59):

Finite generation of extremal rays follows from the fact that extremal rays are correspond to what is called, I think, pre_generators in toric (the relationship between extremal rays and pre_generators needs to be proven).

view this post on Zulip Damiano Testa (Apr 10 2021 at 16:59):

(pre_generators being finite is "easy" and, if I remember correctly, already proven, in some form.)

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:01):

Finiteness of saturating elements is the "topological part of the proof: once you have the finitely many generators extremal rays, you are missing the elements inside the cone that are convex combinations of the generators of the extremal rays with non-negative and bounded above real coefficients.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:02):

Thus, these "new" elements are contained in a compact set (the real combinations) and in a discrete subset (they are in the integral subcone). Hence there are only finitely many of them.

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 17:13):

I'm still trying to get all this stuff straight.

It seems to me that sometimes people talk about real vector spaces and sometimes free Z-modules. As far as I can see we dont need real anything, we can stick to vector spaces over the rationals.

You say that pointed is supposed to be an octant, but you proved that {0} was pointed and in your definition an octant in a real vector space will always be a manifold with dimension the same as that of the underlying space.

Is your definition of extremal ray for Q-vector spaces or Z-modules? What is a "cone"? Are you using the word to mean both a f.g. Q_+-submodule of a Q-module and a f.g. N-submodule of a Z-module? I'm sorry for all the questions, I really think we need to be very precise about these things though. If sub-N-modules of Z-modules can be cones, are they all saturated or not?

"What should be proved is that the elements of the cone are in the convex hull of the extremal rays.." -- I don't even know now whether you're over Q or over Z.

Can you be more precise about all of this? I am still struggling to understand the precise definitions of everything.

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 17:14):

Can we prefix everything with Q- or Z-? Are Z-cones by definition finitely generated? Are they saturated?

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:15):

Ok, the reason I was being a little sloppy is that we definitely need to have these notions interacting nicely with nat- int- rat- and (to a much lesser extent) real.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:15):

Let me answer more in detail your questions.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:17):

First, "octant" is what I said before its Lean formalisation. As you remark, is always "of the top dimension". Cones inside an octant, though, need not have that dimension: as you say, 0 is a cone inside any octant and is therefore pointed.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:18):

The Lean formalization of pointed is more general. Since I want to be able to convert between various coefficients, let me give a few types, with their standard interpretation.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:19):

There are three main "coefficient" types: N, Z, Q. I will let you guess what they are in the standard application.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:19):

The only tricky one is that, at one point, we will want to allow Q to be the reals, but for the most part (and, really, even in the last step) we can always get away with the rationals.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:22):

The three types N, Z and Q are ordered semirings, they form a scalar_tower of algebras, the elements of N are "nonnegative" in Q and you can also assume that algebra_map R S is injective (cf is_inj_nonneg).

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:22):

Cones, refers to a submodule.span N s, where s is a subset of a Q-module.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:25):

Extremal rays are one-dimensional subcones of a pointed cone (not really sure whether we want the definition to also apply to non-pointed stuff). Thus, we reduce from a general cone (which could be the nat-span of 1, -1 inside rat, i.e. not a pointed cone), to a pointed cone, by "splitting in halfs and combining".

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:26):

Before I describe this process more in detail, let me explain how you "construct" cones.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:26):

This is via the dual_set process.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:28):

For duals, the setup is that there are two Q-modules M and N and a bilinear pairing, typically denoted by f, mapping M×NQM \times N \to Q.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:31):

A dual_set is "essentially" a cone: given a subset s of M, the corresponding dual_set is the set of all elements of N that have non-negative pairing with s.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:32):

A dual_set is automatically an N-submodule and it is also automatically saturated.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:32):

Thus, the statement of Gordan's lemma (if I have not missed anything) is as follows:

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:40):

(I noticed now the clash in notation N refers to the natural numbers look-alike as well as the Q-module: I will try to use latex font NN for the module.)

Let MM and NN be Q-modules, with a fixed finite basis. The basis is important, since we are going to talk about "integral" (resp. "non-negative") elements of NN and and they are the Z- (resp. N-)linear combinations of the elements of the basis.

Assume that the pairing f ⁣:M×NQf \colon M \times N \to \mathbb{Q} is "perfect" (what we really want is that every element of the linear dual of NN is represented by pairing with some element of MM).

Start with a finite set s of MM.
The dual_set of s is an N-submodule of NN. The "integer" elements of this submodule admit a finite generating set, of course as an N-module, which is the only thing that type-checks.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:41):

I hope that this clarifies a bit more your doubts. I might have missed some further confusion: please, ask again, if there are unclear points!!

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:44):

Ah, there was the issue of finite generation of cones: they need not be, and we are exactly trying to prove that some cones are finitely generated.

Also, cones are N-spans of stuff: they might be Z-spans, for instance if you use a ±\pm-symmetric generating set, but they need not be.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:44):

Cones need not be saturated, but the ones that arise from dual_set automatically are.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:45):

Also, cones with finitely many extremal rays need not be finitely generated: this is why the fact that the ones arising as dual_set are automatically saturated is important.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:47):

Finally, a comment about the reals: the whole proof can take place with rational coefficients. The only "real" input is in proving that the set of integral vectors inside the span of finitely many vectors with coefficients in [0, 1] is finite. The "easy" way is to use real coefficients, the set of linear combinations is compact, the set of integer vectors is discrete, hence the intersection is finite.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:48):

Of course, you do not "need" real combinations, but it is convenient to have them. Thus, working with a more "generic" type of coefficients is probably a better idea.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:53):

"What should be proved is that the elements of the cone are in the convex hull of the extremal rays.." -- I don't even know now whether you're over Q or over Z.

In the "maths world" we should prove that the elements of the dual_set that happen to have integer coordinates are non-negative rational linear combinations of elements of the extremal rays. Of course, such combinations will not all be integrals, but some will and all those that are rationals we want to take. Once we have this "non-negative rational generating set" for our dual cone, we start worrying about generating over the naturals. For that, we use the integral generators of the extremal rays as a first guess. These are finitely many, by some result that is "almost" formalized. Now the issue is just one of saturation: every integral element of the cone has a positive natural multiple that is a natural-linear combination of these generators of the extremal rays. Thus, we want to "divide" by these multiples.

view this post on Zulip Damiano Testa (Apr 10 2021 at 17:59):

An example to keep in mind is the cone generated by (1,0), (1,2). The background basis is the standard one (1,0), (0,1): integral refers to integral linear combinations of these last two elements.

The extremal rays are the non-negative (rational or natural, not especially important) multiples of the two given vectors (1,0), (1,2).

The non-negative rational linear combinations of the vectors (1,0), (1,2) contain the integer vector (1,1). However, all natural (or even integer) linear combinations of (1,0), (1,2) have even second coordinate and will therefore not equal (1,1): there is a hole.

However, 2(1, 1) = (1,0) + (1,2) is a non-negative integral combination of (1,0), (1,2). We need to saturate. In this case, it is enough to simply add this vector, to the set of generators of the extremal rays.

In general, we need to show that there are only finitely many holes that we need to take care of, and, after we add them, every remaining integer vector in the cone is also a non-negative integer combination of our finite set.

view this post on Zulip Filippo A. E. Nuccio (Apr 10 2021 at 18:04):

I have not really been working on anything related to Gordan's lemma, only the use of it to derive Lemma 9.7. I see Damiano jumped in, and he certainly has more to say.

view this post on Zulip Filippo A. E. Nuccio (Apr 10 2021 at 18:05):

(deleted)

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 22:00):

I still don't see the proof we're trying to formalise. You say "we should prove that the elements of SS^\vee (in the notation of my TeX file) are nonnegative rational linear combinations of elements of the extremal rays" -- but do you know or have a reference for the maths proof of this?

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 22:03):

I know all about the example you mention, I already put it in the TeX file. I am hoping that the TeX file can become a document which a mathematician can read, ie which I can read. Right now i can't understand the topological proof in Wikipedia and i can't see a proof in this thread or in the TeX file.

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 22:04):

My issue with the Wikipedia proof is that it seems to be assuming things about cones which i don't know.

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 22:07):

I don't know where the u_i are coming from in the Wikipedia proof and i don't see where (or if) they're showing up in your proof

view this post on Zulip Damiano Testa (Apr 11 2021 at 04:56):

Dear Kevin,

I am really sorry: I realise that I made the folder toric available too soon. I did not formalise all the statements that I mentioned above: they have to be formalised, of course, but I have not done it yet.

In particular, as you noticed, the statement that a pointed, closed convex cone is the convex hull of its extremal rays is still far from being formalised. The "pointer" to this is in the now flawed file dual_extremal_API:

/--  The rays of the dual of the set `s` are the duals of the subsets of `s` that happen to be
cyclic. -/
def dual_set_rays (s : set M) : set (submodule R N) :=
{ r | r.is_cyclic   s'  s, r = f.dual_set P₀ s' }

/-  We may need extra assumptions for this. -/
/--  The link between the rays of the dual and the extremal rays of the dual should be the
crucial finiteness step: if `s` is finite, there are only finitely many `dual_set_rays`, since
there are at most as many as there are subsets of `s`.  If the extremal rays generate
dual of `s`, then we are in a good position to prove Gordan's lemma! -/
lemma dual_set_rays_eq_extremal_rays (s : set M) :
  f.dual_set_rays P₀ s = (f.dual_set P₀ s).extremal_rays :=
sorry

view this post on Zulip Damiano Testa (Apr 11 2021 at 05:02):

This lemma, or a provable version of it, gives the conversion between extremal_rays and dual_set_rays.

I should also at least state that a cone is the span of its extremal_rays, but I have not done this. Part of the reason is that I would have liked there to be more API available, to make sure that I had not made silly mistakes in the definitions before, and I only wanted to build these lemmas on more solid foundations.

At the moment, I have actually proven too few lemmas about these definitions to be sure that I have not made a mistake. And, as you pointed out, I have made mistakes!

view this post on Zulip Johan Commelin (Apr 11 2021 at 10:17):

Note that I pushed Damiano a bit to merge toric into master. I think it makes it more visible. I'm sorry for the confusion it created.

view this post on Zulip Damiano Testa (Apr 11 2021 at 10:30):

I am going to write a more complete mathematical version of the proof, which is what I think that Kevin wanted all along: hopefully this will clear out most of the doubts!

view this post on Zulip Kevin Buzzard (Apr 11 2021 at 10:42):

We're talking privately, trying to put together a mathematical proof, so we can actually understand the magnitude of the task. It seems that the proof Damiano is suggesting right now needs stuff like the Hahn-Banach theorem, the Krein-Milman theorem etc. I am not yet convinced that this is the proof we should be formalising.

view this post on Zulip Kevin Buzzard (Apr 11 2021 at 10:43):

I think the next step is to establish full details of a mathematical proof, before we can even think about formalising anything.

view this post on Zulip Damiano Testa (Apr 11 2021 at 16:26):

I pushed a slightly more complete version of the Algebraic Wikipedia proof, expanding on what Kevin had written.

I would be happy to hear any comments, try to answer any questions, and clarify any hazy points, if I can!

view this post on Zulip Damiano Testa (Apr 11 2021 at 16:27):

You can find the "algebraic blueprint" in the toric branch, in src/toric/gordan_algebraic_blueprint.tex.

view this post on Zulip Damiano Testa (Apr 11 2021 at 16:27):

Ah, I forgot to update the pdf file: is there a way of doing it remotely, or should I push a compiled pdf version of the tex file?
I also pushed a version with the pdf file.

view this post on Zulip Riccardo Brasca (Apr 11 2021 at 19:30):

I am late to the party , I didn't had time this weekend. I didn't work a lot on this, I just killed two random sorry that seemed doable, without any global strategy. In any case now that my refactoring project is done I can help. I will try to have a close look at the blueprint tomorrow.

view this post on Zulip Damiano Testa (Apr 12 2021 at 04:35):

I pushed a newer version of the algebraic blueprint to the toric branch. There are no substantial changes, I simply tried to streamline the proof a little bit, and, hopefully, clarified it!

view this post on Zulip Damiano Testa (Apr 12 2021 at 04:36):

Comments are welcome!

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 14:38):

In the proof of Lemma 3, "...dual of a finite subset of kerφ\ker \varphi..." should be "...dual of a finite subset of (kerφ)(\ker \varphi)^\ast...", right?

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 15:04):

Also, is it clear that "the dual of kerφ\ker \varphi is the quotient of Λ\Lambda^\ast by the saturation of the additive subgroup generated by φ\varphi"?

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

kerφ\mathrm{ker}\varphi is a saturated submodule, and so a direct factor; hence dualization behaves well

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:12):

Does mathlib have the classification of f.g. modules over PIDs? I guess this is what's eventually used here...

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

Nope, not yet, unfortunately :sad:

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 15:13):

Not quite, but we know f.g. + torsion-free => free (and hence f.g. implies free + f.g. torsion); what we don't have right now is classification of f.g. torsion modules. I think what we have should be enough.

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:14):

Or at least that a f.g. torsion free is free

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 15:14):

I think Patrick finished this recently.

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 15:18):

We have docs#submodule.exists_is_basis. Everything here seems to be torsionfree, so it should be enough

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:19):

Nice!

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:24):

Wait, is this what you want? Seems to me that you want to see that the quotient by ker phi is free.

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:37):

(note that submodule.exists_is_basis is true even without the finite rank assumption)

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

You're right. I don't find that torsion free implies free, but maybe I didn't search enough

view this post on Zulip Patrick Massot (Apr 12 2021 at 16:44):

This is not yet in mathlib. I started to PR preliminaries with #7037 and #7040, and #7160 is currently under review. Maybe I should have done only one massive PR.

view this post on Zulip Patrick Massot (Apr 12 2021 at 16:45):

If there is a urgent need I can also create a file in the liquid repository.

view this post on Zulip Damiano Testa (Apr 12 2021 at 17:45):

With respect to the saturation of kernels, I think that this is already formalised. Ot at least it is close to being formalised and might be within easy reach in the case of Z\mathbb{Z}-/N\mathbb{N}-modules.

view this post on Zulip Damiano Testa (Apr 12 2021 at 17:46):

Patrick, I do not think that this is urgent. There is some more stuff that needs doing that does not depend on this, and we can always merge your unmerged branches into lean-liquid. It will probably be easy to adapt, should there be changes in the statements.

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 17:49):

@Damiano Testa I corrected some mini typos in the blueprint.

What is the status of Theorem 2 in Lean? If not already done it seems a good subproject, that can be done independently of Gordan's lemma

view this post on Zulip Damiano Testa (Apr 12 2021 at 17:52):

I will take a look now: I have been out all day and have a few things to catch up, so I may be a little slow in replying!

view this post on Zulip Damiano Testa (Apr 12 2021 at 17:54):

Riccardo, I do not know how much of Theorem 2 is already in mathlib. However, it will likely need some API developed around it.

view this post on Zulip Damiano Testa (Apr 12 2021 at 17:55):

Here is what I would ideally hope that the API would be able to do:

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 17:55):

We already have monoid_algebrawith an API

view this post on Zulip Damiano Testa (Apr 12 2021 at 17:56):

The ring R[M]R[M] is MM-graded, and later we will want to do a Noetherian induction on the Z\mathbb{Z}-graded ring AA. It would be awesome if we could use a common API for dealing with graded rings/algebra, where the grading is by a more or less arbitrary (abelian) group, additive of multiplicative.

view this post on Zulip Damiano Testa (Apr 12 2021 at 17:58):

Ok, monoid_algebra could work, though I have not worked with it. Most of the arguments involve decomposing a non-necessarily homogeneous element, into its homogeneous components. It would be great if the API could make it easy to do this.

view this post on Zulip Damiano Testa (Apr 12 2021 at 17:58):

Possibly in the form of an induction principle or something analogous-

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 18:01):

I have no idea about graded stuff in mathlib, but R[M]R[M] is in mathlib, and I don't see any problem to state Theorem 2, exactly as in the blueprint (so we don't need any graded ring).

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 18:02):

I mean, if we want to follow the algebraic proof there are no doubts that Theorem 2 is needed, exactly as it is in the blueprint, right?

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:07):

Yes, the point of the blueprint is that it is supposed to be spelling out exactly what we need to prove precisely the sorried statement in toric.lem97.

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:09):

I need to worry about other things today and tomorrow, but on Wednesday I will get back to this, and in my mind what we need to do with this proof is to pull out more sublemmas, because I think the main argument is too long to be formalised painlessly in Lean -- we will get to that stage where it takes 10 seconds to write every line and this is no fun at all. Right now the two things I can see that we can pull off are Theorem 2, which is already pulled off, and the statement that if Λ\Lambda is a finite free Z\Z-module then it has a well-defined rank r(Λ)r(\Lambda), and the theorem that if ϕ:ΛZ\phi:\Lambda\to\Z is non-zero then the kernel of ϕ\phi is also a finite free Z\Z-module, with strictly smaller rank.

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

I completely agree that we need to find as much subgoals as possible. I can work on theorem 2

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

Even using this last result in the main proof will be delicate, because the kernel of ϕ\phi is a submodule, which we then promote to a module Λ\Lambda', and we will have to move S0:=Sker(ϕ)S_0:=S\cap ker(\phi) into Λ\Lambda', prove finitely-generated there by induction, and then move the finite generation back to the submodule. This is just the sort of nonsense which is going to make the proof slightly delicate to formalise, but we have seen this kind of argument time and time again and we know it's possible. There is a risk it will make it long though, which is why I think we need to get as much stuff out of the main inductive step as we can.

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:13):

A formal proof of theorem 2 would be very helpful! Thanks!

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

I am also very much hoping that we can extract this argument about A0A_{\geq0} being finitely-generated over A0A_0 as a separate lemma, but one will have to be very careful here that the lemma one extracts will actually be applicable in the case that one needs. I would advocate a "top-down" approach here -- this is not particularly fashionable amongst the CS crowd (they are paranoid people) but Johan and I and Patrick and many other mathematicians have been using this approach for a while and as far as I can see it works fine. What I mean here is: just take that sorried Gordan's Lemma in toric.lem97 and start to prove it, but sorry everything along the way. For example, say that a free module has a rank, but sorry the definition. Claim that the submodule, when promoted to a module, is free of smaller rank, and sorry the proof. Then write down the grading, prove that A0A_0 is a subring, sorry the proof it's finitely-generated over the base field, sorry the proof that A0A_{\geq0} is finitely-generated over A0A_0, now see if you can use results in the library to prove A0A_{\geq0} is finitely-generated over the base field and check that you can now finish the proof with Theorem 2 (i.e. check that your choice of precise formalisation of Theorem 2 suffices to finish the job).

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:23):

This top-down approach now gives us a whole bunch of sorries (and already what I have said above might expand out into quite a long proof as well). Now we have to decide how to fill in those sorries, and the idea is to try and fill them in with new lemmas rather than solving these goals within this proof we've just written. Then one has to think about precisely the statement of the formalisation of the missing pieces, but because we have this top-down sorried proof, one can take one of the missing pieces (for example some statement that for a Z-graded Noetherian ring, A0A_{\geq0} is finitely-generated over A0A_0), attempt to formalise the statement, and before one even begins to prove it one can check to see if the statement is in the correct form to make it easy to fill in the sorry in the main proof. If it turns out that this makes the main proof even bigger, because there are issues switching from subtypes to types or problems checking that one grading matches with another, or problems because it turns out that there are two different notions of grading, then this is an indication that the formalised statement you have chosen might not be the best one. This way the top-down proof guides us and shows us how to formalise the intermediate statements, meaning that the end result won't have one horrible 300-line argument in it but will instead be a bunch of smaller results which it will be possible to glue together relatively painlessly.

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:26):

So in fact Riccardo, one answer to your "theorem 2 is needed, exactly as it is in the blueprint" would be this: the blueprint states a mathematical theorem, not a formal Lean theorem. It might be best to start with the big prize, namely the precise sorried statement in the lem97 file, and work down from there. You might find for example that ultimately we do not want a statement about monoid_algebra R M, but a statement about a ring which is canonically isomorphic to monoid_algebra R M. If you've gone ahead and formalised Theorem 2 but just for the "concrete" model of monoid_algebra R M in mathlib then you might find that your lemma will not "fill in the hole" that we need it to fill in. So I think that before anything is formalised, now we think we have a mathematical proof, it might be worth starting on the top-down approach.

view this post on Zulip Adam Topaz (Apr 12 2021 at 18:27):

I must be missing something.... what's theorem 2?

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:27):

It's in a pdf on the toric branch

view this post on Zulip Adam Topaz (Apr 12 2021 at 18:27):

Ah ok

view this post on Zulip Adam Topaz (Apr 12 2021 at 18:27):

(I thought it was theorem n.2 from the blueprint for some value of n...)

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:27):

It's in src/toric/gordan_algebraic_blueprint.tex.

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:28):

This is a mini-blueprint for Gordan's Lemma, because we realised that it was more complicated than we originally thought.

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:28):

It could easily be put into the lean-liquid blueprint, but it will not be difficult to do this later.

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 18:32):

It says that, for a commutative monoid MM and a nontrivial ring RR, the RR-algebra R[M]R[M] is finitely generated (as RR-algebra) if and only if MM is finitely generated as a monoid.

view this post on Zulip Adam Topaz (Apr 12 2021 at 18:32):

Yeah I'm looking at it now...

view this post on Zulip Adam Topaz (Apr 12 2021 at 18:32):

Oh this should totally be doable with current mathlib

view this post on Zulip Riccardo Brasca (Apr 12 2021 at 18:33):

That's why I am asking if we're sure it is the theorem we need :grinning:

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:44):

Yes I'm sure it's doable, but the big question is precisely how to formalise it. This is why I am suggesting that now we think we have a maths proof which should be possible to formalise reasonably (although I have not checked Damiano's argument about A0A_{\geq0} being finitely-generated over A0A_0 yet -- please someone else feel free to do this so we've had more than one pair of eyes on it!) the next step should be to start at the top and replace the one sorry in lem97 with a bunch of sorries, thus showing us precisely the form of the sublemmas which we will need. As I've already said, I am concerned that if we prove a result about monoid_algebra then this will not be applicable in the situation we're interested in, and the actual result we need might be a result about an algebra which satisfies the universal property of monoid_algebra. Whether it is easiest to prove monoid_algebra first and deduce the result for the ring isomorphic to monoid_algebra afterwards, or whether it's easier to work with the universal property directly, is something I am not yet clear on. However there is often more than one universal property! We need something which is not too hard to check in the application, but furthermore strong enough to relatively painlessly come up with a unique isomorphism to the concrete monoid_algebra if we decide to formalise the theorem using this concrete model. This is precisely the mistake we made with the first schemes formalisation you see -- we proved a very messy result which involved several rings of the form localisation R S and then we needed to apply it to rings which had the universal property of localisation R S but were not definitionally equal to it, and I had to spend about a week developing tools for diagram chasing along morphisms coming from universal properties and it was no fun at all.

view this post on Zulip Damiano Testa (Apr 12 2021 at 18:48):

If this is helpful, I think that I can extract smaller lemmas from the mathematical proof.

view this post on Zulip Damiano Testa (Apr 12 2021 at 18:49):

Would this be useful? There are several results that are mentioned as "mathematical one-liners" that I imagine would expand quite a bit when formalized. If this is helpful, I can start expanding the mathematical proof, by fracturing it more.

view this post on Zulip Damiano Testa (Apr 12 2021 at 18:49):

Also, I would very much welcome someone else looking at the proof!

view this post on Zulip Adam Topaz (Apr 12 2021 at 19:18):

We recently got docs#is_free_group

view this post on Zulip Adam Topaz (Apr 12 2021 at 19:18):

I feel like we should add similar classes for all such free constructions (including the monoid algebra)

view this post on Zulip Adam Topaz (Apr 12 2021 at 19:19):

(note the universe restrictions in the definition BTW, along with docs#is_free_group.unique_lift )

view this post on Zulip Riccardo Brasca (Apr 13 2021 at 09:54):

I started writing at least the statement of theorem 2, to check if there are results we are missing to prove it, in this form or another.

import algebra.monoid_algebra
import ring_theory.finiteness

variables {R : Type*} [comm_ring R] [nontrivial R]
variables {M : Type*} [add_comm_monoid M]

open algebra submodule

lemma monoid_alg_ft_iff : finite_type R (add_monoid_algebra R M)  ( : submodule  M).fg :=
begin
  sorry
end

Does someone see a way to use [comm_monoid M] instead of [add_comm_monoid M]? It seems much more natural to me, but then I don't know how to say (⊤ : submodule ℕ M).fg , since a multiplicative monoid is not a -semimodule, and all the theory of finitely generated stuff in mathlib is for subsemimodules.

view this post on Zulip Riccardo Brasca (Apr 13 2021 at 09:57):

Hmm, I can use additive Mbut maybe this will introduce other problems in the proof.

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

If we don't have stuff about finitely generated submonoids, then I don't think we can use multiplicative notation

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

Unless you want to do another huge refactor of mathlib (-;

view this post on Zulip Riccardo Brasca (Apr 13 2021 at 10:10):

No thanks :sweat_smile:

view this post on Zulip Riccardo Brasca (Apr 13 2021 at 12:37):

I am experimenting a little bit, but maybe the following statement is more reasonable

lemma monoid_alg_ft_iff : finite_type R (monoid_algebra R M) 
   S : finset M, submonoid.closure (S : set M) =  :=

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

I guess that works. But you run the risk that you will have to develop an API for submonoid.fg on the fly.

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 13:04):

Ok the big work thing I had to do is over and I will be looking at this starting in about an hour. Did anyone begin to flesh out the proof of the sorry in lem97? If not I'll start there. It's time we got Gordan out of the way.

view this post on Zulip Damiano Testa (Apr 13 2021 at 13:51):

I have not looked at the proof of explicit_gordan, but I still think that having graded rings/algebras could be useful for the proof. At least some primitive form of it.

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:05):

Yes we absolutely need an API for graded rings here, for example you use all over the place the fact that if A is graded by a cancellative monoid M and if i+j=k is an identity in M and a_i * r = a_k in A with a_i in A_i etc then there's some a_j with a_i * a_j = a_k. We don't want to have to stop what we're doing to justify this sort of stuff. What is the status of M-gradings on A, M a commutative monoid and A a commutative ring? This sounds like something fun to make

view this post on Zulip Johan Commelin (Apr 13 2021 at 14:06):

I think @Eric Wieser has/had some PRs on gradings on direct_sum _. But we don't have general gradings on general rings, afaik

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:07):

I agree that it would be fun to make, but I do not know what is available.

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:08):

My thinking was that a "grading on a ring" is just an isomorphism to a direct sum of submonoids

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:08):

I remember Eric had something about nat gradings (and I even remember arguing that nat gradings were the place to start) but we need int gradings

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:09):

and MM-gradings, where MM is an add_monoid, while we are at it?

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:10):

I am pushing for this, since two proofs in the blueprint would benefit from being able to use gradings: the one about the equivalence of fg for an add_monoid and the monoid_algebra, and the one about the Z-gradings

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:12):

docs#direct_sum.ring has gradings of by an arbitrary add_monoid

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:18):

What we're missing is something like the statement

A : ι → monoid R is a gradation of a ring R if complete_lattice.independent (set.range A) and there is a ring_equiv from R to ⨁ i, A i whose inverse is roughly direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i)

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:23):

I think that the two main properties that should be easily accessible are that

  • every element of the graded ring is a finite sum of homogeneous elements
  • product of homogeneous elements is homogeneous of degree the sum of the degrees.

I imagine that this should form part of the definitions, but I have been wrong about such things in the past!

Having this to hand already goes quite a long way into the proof of the first lemma about monoid generation.

If it is not already in mathlib, it would also be good to extract a lemma that says that if a ring is generated by some set s and some other set t generates the generators, then t also generates.

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:33):

@Eric Wieser what we need right now I think is something like

import ring_theory.subring
import data.finsupp

open_locale big_operators

structure grading (M : Type*) [comm_monoid M] (R : Type*) [comm_ring R] :=
(graded_piece : M  set R)
(independent :  f : M →₀ R, ( m : M, f m  graded_piece m) 
  f.sum (λ m r, r) = 0  f = 0)
(span :  r : R,  f : M →₀ R, ( m : M, f m  graded_piece m)  f.sum (λ m r, r) = r)

and also a variant for add_comm_monoid (in fact in our application we only need add_comm_monoid). Do we have anything like this? We don't need to build the ring we have it already, we want to impose the grading a posteriori.

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:35):

Kevin, maybe this is implicit, but don't we also want that multiplication between homogeneous pieces maps to the right homogeneous piece?

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:35):

Is it not a requirement for the graded pieces to be closed under addition?

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:36):

hmm :-)

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:39):

structure grading (M : Type*) [comm_monoid M] (R : Type*) [comm_ring R] :=
(graded_piece : M  add_subgroup R)
(grading_mul :  (m n : M) (r s : R),
  r  graded_piece m  s  graded_piece n  r * s  graded_piece (m * n))
(independent :  f : M →₀ R, ( m : M, f m  graded_piece m) 
  f.sum (λ m r, r) = 0  f = 0)
(span :  r : R,  f : M →₀ R, ( m : M, f m  graded_piece m)  f.sum (λ m r, r) = r)

?

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:40):

My attempt at my quoted description above is:

import order.complete_lattice
import algebra.direct_sum_graded
import algebra.direct_sum

open_locale direct_sum

def is_gradation {ι : Type*} {R : Type*} [decidable_eq ι] [add_monoid ι] [semiring R]
  (A : ι  add_submonoid R) : Prop :=
    complete_lattice.independent (set.range A) 
   hone hmul,
    let inst := direct_sum.gmonoid.of_add_submonoids A hone hmul in by exactI
     (e : R ≃+*  i, A i),
      -- this let is here to help the elaborator
      let f : ( i, A i) →+ ( i, A i) :=
        direct_sum.to_add_monoid (λ i : ι, (add_submonoid.inclusion (le_supr A i) : _)) in
      e.symm.to_add_equiv.to_add_monoid_hom = (add_submonoid.subtype _).comp f

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:41):

If the semiring mafia get to this definition then the graded pieces will end up being add_submonoids, but I suspect one can prove they're subgroups from the other axioms if R has subtraction.

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:42):

re syntax error: just end with := sorry

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:42):

Yeah, I worked that out eventually, but what I actually meant was : Prop :=

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:42):

... unless of course, the grading does not respect multiplication by -1, if it can! :upside_down:

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:44):

Damiano, the trick is that if r is in R_m then you write -r as a linear combination of stuff in graded pieces

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:46):

Kevin, is your independent equivalent to docs#complete_lattice.indepedent?

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:46):

Ah, I see that now the graded pieces are add_subgroups: I had missed that!

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:47):

so, yes, of course, the piece that contains 1 also contains -1!

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:48):

Eric Wieser said:

Kevin, is your independent equivalent to docs#complete_lattice.independent?

Yes.

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:49):

... and is that easy to prove?

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:49):

Oh -- at least in the add_subgroup case.

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:50):

In the add_subgroup case it's easy to prove on paper. Is that what you're asking?

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:50):

Actually, does it automatically follow that 1 is homogeneous? In my mind, I always think that the elements of degree 0 form a subring: they are clearly a subgroup that is closed under multiplication, but do they have a 1? Is the one of this piece the same as the 1 of the whole ring?

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:51):

I've just realized - your version is multiplicatively graded, but direct_sum.ring is additively graded

view this post on Zulip Damiano Testa (Apr 13 2021 at 14:51):

for safe measure, should we add the axiom that the degree 0 piece is a subring?

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:53):

I only care about the case of an add_comm_monoid grading, I went with comm_monoid believing that I could perhaps use to_additive to generate the API for the add_comm_monoid variant (I'm assuming it ignores rings)

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:53):

I was scared of that parenthesized assumption so decided to just focus on the additive case

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:54):

I guess it won't touch the rings but it could well touch the add_subgroup R's :-/

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:56):

Here's how to mesh Kevin's definition with my direct_sum stuff:

import algebra.direct_sum_graded

open_locale direct_sum

-- modified for additive grading, and a `one` axiom
structure add_grading (M : Type*) [add_comm_monoid M] (R : Type*) [comm_ring R] :=
(graded_piece : M  add_subgroup R)
(grading_one : (1 : R)  graded_piece 0)
(grading_mul :  (m n : M) (r s : R),
  r  graded_piece m  s  graded_piece n  r * s  graded_piece (m + n))
(independent :  f : M →₀ R, ( m : M, f m  graded_piece m) 
  f.sum (λ m r, r) = 0  f = 0)
(span :  r : R,  f : M →₀ R, ( m : M, f m  graded_piece m)  f.sum (λ m r, r) = r)

variables (M : Type*) [add_comm_monoid M] (R : Type*) [comm_ring R]

instance : has_coe_to_sort (add_grading M R) := _, λ g,  i, g.graded_piece i

instance grading.gmonoid [decidable_eq M] (g : add_grading M R) : direct_sum.gmonoid (λ i, g.graded_piece i) :=
direct_sum.gmonoid.of_add_subgroups (λ i, g.graded_piece i) g.grading_one g.grading_mul

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 14:56):

The reason my independent is the same as complete_lattice.independent is that Sups in the lattice of add_submonids is "add_submonoid generated by", and this is the same as "finite sums of elements in the union". Is that enough of a clue Eric or are you asking for something more formal?

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:57):

My question was less "why is that true" and more "how painful will it be to convince lean that is true"

view this post on Zulip Eric Wieser (Apr 13 2021 at 14:59):

Damiano Testa said:

for safe measure, should we add the axiom that the degree 0 piece is a subring?

This is proven by #6851 using the existing axioms

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 15:00):

Oh OK. Yeah it might be a bit painful -- we saw this recently with Patrick's challenge the other day. To say "this subgroup A_0 of A has trivial intersection with the subgroup generated by these subgroups A_1, A_2, A_3, ..." is the same as to say "if I have f : nat ->_0 A with f(i) in A_i and the sum of the f(i) is zero, then f(0) must be 0", because f(0) is in both A_0 and the subgroup generated by the A_i for a >= 1 which contains f(1)+f(2)+.... = -f(0). This is why I'm a bit worried about submonoids.

view this post on Zulip Eric Wieser (Apr 13 2021 at 15:01):

I think pretending the semiring mafia will never arrive and using subgroup instead of submonoid is an acceptable approach here

view this post on Zulip Eric Wieser (Apr 13 2021 at 15:06):

But as a wannabe member of the constructivist cartel, I feel like your definition should provide span constructively as

(span :  r : R, {f : M →₀ R // ( m : M, f m  graded_piece m)  f.sum (λ m r, r) = r})

or better

view this post on Zulip Damiano Testa (Apr 13 2021 at 15:08):

Eric, thanks! I am not able to follow quickly your argument, but it is great that the units line up!

view this post on Zulip Eric Wieser (Apr 13 2021 at 15:11):

By "units" you mean 1 or "pieces of code from Eric and Kevin"?

view this post on Zulip Damiano Testa (Apr 13 2021 at 15:14):

Eric, I meant the elements 1 in R and the element 1 in graded_piece (0 : M).

view this post on Zulip Eric Wieser (Apr 13 2021 at 15:28):

Note that even without the (1 : R) axiom you can still create an instance of docs#direct_sum.ghas_mul, which shortly after #6786 will result in a non_unital_semiring structure on add_grading M R

view this post on Zulip Damiano Testa (Apr 13 2021 at 15:34):

Ok, I am happy with that, thanks! Also, I wanted to make sure that we did not face non-unital rings (even in the degree 0 graded_piece`), hence my questions! I would not want to demote these graded rings to graded rngs!

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 16:52):

Aargh complete_lattice.independent is a statement about subsets and we have a map from a monoid, so for example if the monoid is nontrivial and the map sends every element of the monoid to the same nonzero add_subgroup then they won't be independent in the sense I wrote (and that we need) but they'll be independent in the sense that the range of the function has size 1.

view this post on Zulip Eric Wieser (Apr 13 2021 at 16:56):

Oh, nice catch

view this post on Zulip Adam Topaz (Apr 13 2021 at 16:57):

Just make the functiongraded_piece injective?

view this post on Zulip Riccardo Brasca (Apr 13 2021 at 16:58):

As sanity check I proved the easy implication of theorem 2 of the blueprint, here
https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/toric/theorem2.lean

view this post on Zulip Eric Wieser (Apr 13 2021 at 16:59):

Perhaps restating docs#complete_lattice.independent in terms of an indexed collection is a good idea anyway though

view this post on Zulip Adam Topaz (Apr 13 2021 at 16:59):

Eric Wieser said:

Perhaps restating docs#complete_lattice.independent in terms of an indexed collection is a good idea anyway though

How big of a refactor would this be?

view this post on Zulip Adam Topaz (Apr 13 2021 at 17:00):

BTW, the algebraic geometer in me wants a grading to be a coaction by the coordinate ring of Gm\mathbb{G}_m or something. (not a serious suggestion.)

view this post on Zulip Eric Wieser (Apr 13 2021 at 17:02):

I've no idea how big that refactor would be, but I don't think complete_lattice.independent is used in all that many places yet

view this post on Zulip Eric Wieser (Apr 13 2021 at 17:02):

Mainly just https://leanprover-community.github.io/mathlib_docs/order/compactly_generated.html I think

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 17:06):

I think the toric people want Z gradings, the projective scheme people want N gradings and in this proof we also want gradings by an arbitrary monoid

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 17:09):

span is just a statement about a Sup

view this post on Zulip Adam Topaz (Apr 13 2021 at 17:11):

Kevin Buzzard said:

I think the toric people want Z gradings, the projective scheme people want N gradings and in this proof we also want gradings by an arbitrary monoid

IIRC a grading by a monoid M on an R-algebra is "the same" as a coaction of R[M]?

view this post on Zulip Adam Topaz (Apr 13 2021 at 17:11):

Although this point of view would be hard to formalize for noncommutative monoids (since it involves a tensor product of bialgebras)

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 17:11):

Aha, this is some monoid scheme maybe

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 17:12):

Do people grade with noncommutative monoids ever? @Julian Külshammer ?

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 17:15):

So in terms of lattices this map from a monoid is like a basis -- the Sup of everything is top, and the inf of (one piece) and (the Sup of all the other pieces) is zero. Is that a thing in lattices with a Sup?

view this post on Zulip Eric Wieser (Apr 13 2021 at 17:15):

Do people grade with noncommutative monoids ever?

Based on what I found for docs#direct_sum.semiring (as opposed to docs#direct_sum.comm_semiring), if your ring is not commutative then you don't need your index set to be either.
Not that that answers the question of whether its useful, just that its easy to generalize to.

view this post on Zulip Adam Topaz (Apr 13 2021 at 17:17):

Kevin Buzzard said:

So in terms of lattices this map from a monoid is like a basis -- the Sup of everything is top, and the inf of (one piece) and (the Sup of all the other pieces) is zero. Is that a thing in lattices with a Sup?

This sounds like some general notion of independence that comes up in matroid theory.

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 17:18):

Maybe this should move to #maths, this feels much more mathlibby than liquidy

view this post on Zulip Filippo A. E. Nuccio (Apr 13 2021 at 18:14):

I have looked a bit into your discussion, seeing that you're going to attack Gordan. I won't be of great help with the grading mafia but I'd be help to adapt the current proof of lem97 to a new statement of explicit_gordan, if you come up with something different from what I used there.

view this post on Zulip Julian Külshammer (Apr 13 2021 at 18:14):

@Kevin Buzzard Is the emphasis on noncommutative or on monoids? There are articles written in my area of research about gradings by non-commutative groups and one definitely wants to consider \N-gradings as well, so grading by possibile non-commutative monoids seems like an obvious choice for me. In most examples people compute the grading is by \N^r or \Z^r or Z/2, but I also don't see why it should be more difficult to formalise a grading by a noncommutative monoid than a commutative monoid. Do you have an example of a basic result which fails?

view this post on Zulip Damiano Testa (Apr 13 2021 at 18:27):

There is also the case of the group algebra of a (finite) group, which is graded by the group itself.

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

I know that we are going to change the statement like 30 times, but I was having too much fun, and here is the proof of theorem2 of the blueprint

lemma monoid_alg_ft_iff_fg [nontrivial R] :
  ( : submodule  M).fg  finite_type R (add_monoid_algebra R M)

It is in https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/toric/theorem2.lean

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 21:23):

I think this might be fine -- we might later on need to apply it to something isomorphic to an add_monoid_algebra, but in this case we just will need to prove things like if A and B are isomorphic R-algebras and A is finite type then so is B.

view this post on Zulip Riccardo Brasca (Apr 14 2021 at 21:23):

We already have this!

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 21:26):

In which case I think you've done enough :-) I'm having a lot of fun with gradings, I have achieved far less today than I had hoped but it would still be wonderful to get Gordan done by the end of the week.

view this post on Zulip Damiano Testa (Apr 15 2021 at 05:21):

Kevin, is the definition of grading that you are using the one in
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Gradings.20on.20a.20ring/near/234389540

I would be happy to contribute!

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 06:19):

Right now the technical issue is that there are two ways of saying that R is the direct sum of R_m and these should probably be unified.

view this post on Zulip Damiano Testa (Apr 15 2021 at 06:20):

Ok, if you want, I can try taking care of that.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 06:21):

It's pretty gory. I need to do family stuff for another hour and then I'll have time for lean

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 07:55):

Ok so it looks like Sebastien is fixing the mathlib diamond so I can tell you about gradings. I was going to work on this stuff today (and tomorrow), by the way.

The mathlib branch independent2 (which I'm about to PR) contains a definition of what it means for a function f:I -> L (I an abstract type, L a complete lattice) to be "independent" -- it means that the inf of f(i) and (the Sup of the f(j) for j!=i) is bot. In applications, L will be the additive submonoids or subgroups of a ring or semiring, so this just says that f(i) intersect (subgroup generated by f(j) for j != i) is zero.

The mathlib branch gradingcontains independent2 (I merged the independent2 branch into it, even though the independent2 branch isn't in master) and also contains a recent PR of Eric's which defines add_submonoid_is_internal. This is a predicate on maps f : I -> add_submonoid M which says "the induced map from the direct sum of the f(i) to M is a bijection". I've been trying to work with this and it's quite tricky. You can see for example in ring_theory.grading that I have an unfinished proof that R[X] is graded by the naturals and it looks pretty scary to me. Right now I am wondering whether Eric's "the induced map from the direct sum is a bijection" would be easier to work with if we rewrote it in the following way. The bijection is an injection and a surjection. To say that a map from a direct sum of additive abelian submonoids of M to M is injective is, I think, the same as saying that that the function from I to the submonoids is injective as above. Conversely the claim that the map is surjective is just the statement that the Sup of the image is Top (a.k.a. "span"). So right now I was thinking of abandoning my proof and writing more API, saying that direct_sum.add_submonoid_is_internal graded_piece is equivalent to independent + span.

So right now as you can see it's all in quite a state, but I still feel confident that doing these examples (polynomials are graded by nat, monoid algebras are graded by the monoid) are the test cases which need to work before we can start on Gordan -- you can think of them as practice, if you like.

view this post on Zulip Damiano Testa (Apr 15 2021 at 08:00):

Kevin, thanks for the update! I will try to take a look at grading on polynomials, then!

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 08:13):

The question is whether we should be continuing to battle through this proof (I think we should not) or whether we should prove that the bijection is an injection and a surjection, and injection is equivalent to independent and surjection equivalent to span.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 08:16):

I'll formalise the statement of what I'm thinking of and then push to grading.

view this post on Zulip Damiano Testa (Apr 15 2021 at 08:17):

Ok, thanks a lot!

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 08:38):

OK I pushed. In the grading branch of mathlib there are a bunch of sorries. My guess is that direct_sum.add_submonoid_is_internal_iff_independent_and_span helps (although it should be broken into two lemmas) with the examples, but I don't know for sure.

Unfortunately, you might have to wait for the oleans, or make them yourself (this is what I have been doing -- I do leanproject get-cache --rev 07614552f6b7157fa5582a8f2a536b390715cb14 and then lean --make src/ring_theory/grading.lean on the command line and wait about 5 minutes). Alternatively you can wait a few hours and then leanproject get-cache should work fine.

view this post on Zulip Damiano Testa (Apr 15 2021 at 08:40):

Thanks a lot, Kevin, for grading and for the instructions!

view this post on Zulip Eric Wieser (Apr 15 2021 at 12:55):

You're describing branch#grading in mathlib not lean-liquid, right?

view this post on Zulip Damiano Testa (Apr 15 2021 at 12:57):

I certainly assumed so: I pulled grading from mathlib.

view this post on Zulip Eric Wieser (Apr 15 2021 at 13:12):

For polynomials i'd expect it's far easier to directly construct the inverse mapping to show bijectivity

view this post on Zulip Eric Wieser (Apr 15 2021 at 13:14):

Which is just "sum direct_sum.of I ⟨monomial i (p.coeff i), sorry⟩ over p.support"

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 14:04):

Can someone put me out of my misery?

import algebra.direct_sum
import data.polynomial.basic

open polynomial

def polynomial_equiv (R : Type*) [semiring R] :
  (polynomial R) 
  direct_sum  (λ i, add_monoid_hom.mrange (monomial i).to_add_monoid_hom) :=
sorry
-- error: don't know how to synthesize placeholder

I can't get the equiv to typecheck :-(

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 14:06):

Oh, I've got it: RHS doesn't know which poly ring. Sorry for the noise.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 14:51):

I am going nuts -- I have still not manage to state this equiv :-(

import algebra.direct_sum
import data.polynomial.basic

open polynomial

noncomputable example (R : Type) [semiring R] (i : ) :
  add_comm_monoid ((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange : Type) := infer_instance

noncomputable def foo (R : Type) [semiring R] :
  (direct_sum  (λ i, (monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange)) 
  polynomial R :=
  (direct_sum.to_add_monoid
    (λ i,
      ((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange.subtype :
        ((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange : Type) →+ polynomial R)))

/-
type mismatch at application
  direct_sum.to_add_monoid (λ (i : ℕ), (monomial i).to_add_monoid_hom.mrange.subtype)
term
  λ (i : ℕ), (monomial i).to_add_monoid_hom.mrange.subtype
has type
  Π (i : ℕ), ↥((monomial i).to_add_monoid_hom.mrange) →+ polynomial R : Type
but is expected to have type
  Π (i : ℕ), ?m_1 i →+ ?m_2 : Type (max ? ?)
-/

What am I doing wrong?

view this post on Zulip Eric Wieser (Apr 15 2021 at 14:58):

Man, the elaborator is really getting the upper hand on you today

view this post on Zulip Eric Wieser (Apr 15 2021 at 15:03):

My orange bars aren't cooperating so I can't help you yet

view this post on Zulip Eric Wieser (Apr 15 2021 at 15:18):

If you break it into tiny pieces it cooperates:

noncomputable def monomial_add_monoid_hom (R : Type) [semiring R] (n : ) : R →+ polynomial R :=
(monomial n).to_add_monoid_hom

def direct_sum.submonoids_to_add_monoid (ι R : Type) [decidable_eq ι] [semiring R]
  (A : ι  add_submonoid R) :
  (direct_sum ι (λ i, A i)) →+ R :=
direct_sum.to_add_monoid (λ i, (A i).subtype)

noncomputable def foo (R : Type) [semiring R] :
  (direct_sum  (λ i, (monomial_add_monoid_hom R i).mrange)) →+ polynomial R :=
direct_sum.submonoids_to_add_monoid  (polynomial R) (λ i, (monomial_add_monoid_hom R i).mrange)

view this post on Zulip Eric Wieser (Apr 15 2021 at 15:20):

Ah, this works:

noncomputable def foo (R : Type) [semiring R] :
  (direct_sum  (λ i, ((monomial i).to_add_monoid_hom : R →+ _).mrange)) →+ polynomial R :=
direct_sum.to_add_monoid (λ i, (monomial i).to_add_monoid_hom.mrange.subtype)

view this post on Zulip Eric Wieser (Apr 15 2021 at 15:21):

IN fact, it's the causing you all the pain in your example

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 15:34):

Thanks! I put the in because it wasn't working without it (indeed what I posted doesn't work without the either)

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 15:35):

Hmm, I see. This is supposed to be a field of an equiv. So I just tell it the type of the add_monoid_hom I guess.

view this post on Zulip Yakov Pechersky (Apr 15 2021 at 15:42):

My rule of thumb is that one should not put coercion arrows in lemma statements (or function coercion). If a coercion is necessary, it should be notated using typing syntax (_ : _), and if it is function coercion, just apply as normal

view this post on Zulip Eric Wieser (Apr 15 2021 at 15:59):

Kevin Buzzard said:

(indeed what I posted doesn't work without the either)

It does once you replace the with →+ I think

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 15:59):

But here's the actual problem:

import algebra.direct_sum
import data.polynomial.basic

open polynomial

def polynomial_equiv (R : Type) [semiring R] :
  polynomial R 
  direct_sum  (λ i, (monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange) :=
{ to_fun := sorry,
  inv_fun := (direct_sum.to_add_monoid
    (λ i,
      ((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange.subtype :
        ((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange : Type) →+ polynomial R))),
  left_inv := sorry,
  right_inv := sorry }

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 16:00):

type mismatch at application
  direct_sum.to_add_monoid (λ (i : ℕ), (monomial i).to_add_monoid_hom.mrange.subtype)
term
  λ (i : ℕ), (monomial i).to_add_monoid_hom.mrange.subtype
has type
  Π (i : ℕ), ↥((monomial i).to_add_monoid_hom.mrange) →+ polynomial R : Type
but is expected to have type
  Π (i : ℕ), ?m_1 i →+ ?m_2 : Type (max ? ?)

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 16:01):

I got so frustrated with this that I just decided to prove the mem_supr lemmas :-)

view this post on Zulip Eric Wieser (Apr 15 2021 at 16:17):

Why not define it as an add_equiv?

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 16:18):

all I want to do is to prove that a function is bijective. It seemed to me that defining it as an add_equiv just meant I'd have to prove more things for no reason.

view this post on Zulip Eric Wieser (Apr 15 2021 at 16:27):

Here you go:

import algebra.direct_sum
import data.polynomial.basic

open polynomial

open_locale direct_sum
noncomputable theory

abbreviation monomial.submonoid (R : Type) [semiring R] (i : ) : add_submonoid (polynomial R) :=
(monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange

def polynomial_equiv (R : Type) [semiring R] :
  ( i, monomial.submonoid R i) ≃+ polynomial R  :=
{ inv_fun := λ p, p.sum (λ n r, direct_sum.of _ n (by exact monomial n r, r, trivial, rfl⟩)),
  left_inv := λ d, sorry,
  right_inv := λ p, sorry,
  ..(direct_sum.to_add_monoid
    (λ i, (monomial.submonoid R i).subtype) : ( i, monomial.submonoid R i) →+ _) }

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 16:28):

Thanks! I might not get back to this until tomorrow now -- right now I'm struggling with stuff like ∏ᶠ (i_1 : ι), ite (i_1 = i) x 1 = x

view this post on Zulip Eric Wieser (Apr 15 2021 at 16:52):

Solved:

import algebra.direct_sum
import data.polynomial.basic
import data.polynomial

open polynomial

open_locale direct_sum
noncomputable theory

abbreviation monomial.submonoid (R : Type) [semiring R] (i : ) : add_submonoid (polynomial R) :=
(monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange

abbreviation monomial.to_submonoid (R : Type) [semiring R] (i : ) : R →+ monomial.submonoid R i :=
(monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange_restrict

def polynomial_equiv (R : Type) [semiring R] :
  ( i, monomial.submonoid R i) ≃+ polynomial R :=
add_monoid_hom.to_add_equiv
  (direct_sum.to_add_monoid $ λ i,
    (monomial.submonoid R i).subtype)
  (finsupp.lift_add_hom $ λ n,
    (direct_sum.of (λ i, monomial.submonoid R i) n).comp (monomial.to_submonoid R n))
  (begin
    ext i x, r, _, rfl : 2,
    dsimp,
    simp [monomial],
    refl,
  end)
  (begin
    ext i r : 2,
    dsimp,
    simp [monomial],
  end)

view this post on Zulip Yakov Pechersky (Apr 15 2021 at 16:52):

simp ..., refl also known as simpa

view this post on Zulip Eric Wieser (Apr 15 2021 at 16:52):

simp [monomial] is needed because you're not supposed to use finsupp.lift_add_hom on polynomials

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 17:13):

oh it doesn't compile for me :-(

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 17:22):

hmm, works on master, I'll have to merge into my branch.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 17:29):

OK great, it works on my branch, now I have to wait for several more hours and then pay some money to download oleans :-/ (my internet is broken right now)

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:06):

To be honest, I do not understand the proof, but is this the same as Eric's proof, except for an add_monoid_algebra?

variables (R ι : Type) [semiring R] (M : Type) [add_monoid M] [decidable_eq M] [decidable_eq ι]

open polynomial

open_locale direct_sum
noncomputable theory

section add_monoid_algebra

/-- `monomial s a` is the monomial `a * X^s` -/
noncomputable def Mm (i : M) : R →ₗ[R] add_monoid_algebra R M :=
finsupp.lsingle i

abbreviation monomial.submonoid (i : M) : add_submonoid (add_monoid_algebra R M) :=
(Mm R M i : R →ₗ add_monoid_algebra R M).to_add_monoid_hom.mrange

abbreviation monomial.to_submonoid (i : M) : R →+ monomial.submonoid R M i :=
(Mm R M i : R →ₗ add_monoid_algebra R M).to_add_monoid_hom.mrange_restrict

def polynomial_equiv :
  ( i, monomial.submonoid R M i) ≃+ add_monoid_algebra R M :=
add_monoid_hom.to_add_equiv
  (direct_sum.to_add_monoid $ λ i,
    (monomial.submonoid R M i).subtype)
  (finsupp.lift_add_hom $ λ n,
    (direct_sum.of (λ i, monomial.submonoid R M i) n).comp (monomial.to_submonoid R M n))
  (begin
    ext i x, r, _, rfl : 2,
    simpa [Mm],
  end)
  (begin
    ext i r : 2,
    simp [Mm],
  end)

end add_monoid_algebra

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:19):

Right, a monoid_algebra version is probably sensible

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:19):

You can use finsupp.single_add_hom instead of touching lsingle

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:24):

I have not managed to get finsupp.single_add_hom to work.

However, if I replace randomly add_monoid_algebra with monoid_algebra, not even everywhere, it seems to me that Lean does not complain: is this normal?

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:24):

Am I missing something?

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:29):

About the finsupp.single_add_hom: I should change the type of Mm (i : M) to be R →+ add_monoid_algebra R M, right?

If I do so, though, the abbreviations are not happy afterwards...

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:30):

I think actually we want the version relating dfinsupp and finsupp

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:30):

Got it!

/-- `monomial s a` is the monomial `a * X^s` -/
noncomputable def Mm (i : M) : R →+ add_monoid_algebra R M :=
finsupp.single_add_hom i

abbreviation monomial.submonoid (i : M) : add_submonoid (add_monoid_algebra R M) :=
(Mm R M i : R →+ add_monoid_algebra R M).mrange

abbreviation monomial.to_submonoid (i : M) : R →+ monomial.submonoid R M i :=
(Mm R M i : R →+ add_monoid_algebra R M).mrange_restrict

def polynomial_equiv :
  ( i, monomial.submonoid R M i) ≃+ add_monoid_algebra R M :=
add_monoid_hom.to_add_equiv
  (direct_sum.to_add_monoid $ λ i,
    (monomial.submonoid R M i).subtype)
  (finsupp.lift_add_hom $ λ n,
    (direct_sum.of (λ i, monomial.submonoid R M i) n).comp (monomial.to_submonoid R M n))
  (begin
    ext i x, r, _, rfl : 2,
    simpa only [Mm, set_like.coe_mk, finsupp.lift_add_hom_apply_single, direct_sum.to_add_monoid_of,
      add_monoid_hom.coe_comp, finsupp.single_add_hom_apply, function.comp_app,
      add_submonoid.coe_subtype],
  end)
  (begin
    ext i r : 2,
    simp only [Mm, finsupp.lift_add_hom_apply_single, direct_sum.to_add_monoid_of,
      add_monoid_hom.coe_mrange_restrict, add_monoid_hom.coe_comp, finsupp.single_add_hom_apply,
      function.comp_app, add_submonoid.coe_subtype, add_monoid_hom.id_apply],
  end)

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:31):

So replace add_monoid_algebra with finsupp, and direct_sum with dfinsupp

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:32):

In any case, I view this simply as a confirmation that your approach is very robust: I could adapt it to work for the (add_)monoid_graded case, from the polynomial case, without actually understanding how it was working!

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:32):

Well those types are defeq!

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:32):

I'll PR a dfinsupp / finsupp version tomorrow

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:33):

Well those types are defeq!

Aaah, that explains why Lean simply liked all of it!

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:35):

If you're looking for practice, we probably want a linear_equiv / submodule version of that def too

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:36):

I tried to do the replacement finsupp + dfinsupp, but I have failed. It is also getting late, so I may not give it a go tonight!

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:36):

The key trick in the proof was to phrase things in a way that ext could pick up

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:36):

Btw, what is the : 2 in ext?

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:36):

Ie, by solving f.comp f_inv = id

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:37):

"don't expand as far as p.coeff I"

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:37):

ah, like congr' 2?

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:37):

It means "apply ext twice"

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:37):

except with ext?

view this post on Zulip Eric Wieser (Apr 15 2021 at 19:37):

Yes

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:54):

I squeezed the the two simps to speed up the processing: there is quite a lot of lemmas that show up!

view this post on Zulip Damiano Testa (Apr 15 2021 at 19:54):

Anyway, I'm off for the day!

Kevin and Eric, thanks a lot for gradings!

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 21:53):

These isomorphisms aren't the end of it, but they're definitely the hardest part. One also needs to check that 1 and * are well-behaved.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 21:53):

For polynomials this was easy. So this looks like it's a workable definition.

view this post on Zulip Eric Wieser (Apr 16 2021 at 08:20):

#7217

view this post on Zulip Eric Wieser (Apr 16 2021 at 08:22):

Typeclass search really wasn't happy here

view this post on Zulip Eric Wieser (Apr 16 2021 at 08:46):

Frustratingly add_monoid_hom.range and add_monoid_hom.mrange are not defeq as types, so probably some refactoring to do before I can get the add_comm_group version easily

view this post on Zulip Kevin Buzzard (Apr 16 2021 at 09:54):

These two monoid range things can be a bit annoying to work with because the definition always involves having to prove mem_top. set.range does not have this problem.

view this post on Zulip Eric Wieser (Apr 16 2021 at 10:35):

Have a look at src#add_monoid_hom.range, it solves that problem

view this post on Zulip Eric Wieser (Apr 16 2021 at 10:37):

Once my other two cleanup PRs go though (#7218, #7220), I'll see what breaks if we do that everywhere

view this post on Zulip Kevin Buzzard (Apr 16 2021 at 10:41):

docs#subgroup.range ?

view this post on Zulip Eric Wieser (Apr 16 2021 at 10:44):

Oops, fixed

view this post on Zulip Eric Wieser (Apr 16 2021 at 10:44):

It uses docs#subgroup.copy to make it definitionally useful

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:17):

@Johan Commelin I need some API for finite_free. In polyhedral_lattice.basic you have a move_this section containing the definition. If I remove [semimodule ℤ A] from the definition (A is an add_comm_group) then the combinatorial_lemma file stops compiling: I get an error on line 378 with rw oops failing; oops is a proof of @polyhedral_lattice.int_semimodule Λ _ = @add_comm_group.int_module Λ _. If I remove the proof of oops and the rewrite, things work again. Is this what I'm supposed to be doing or are there reasons for me not to fiddle with this? The reason I ask is that my instinct is to set up finite_free for comm_groups as well as add_comm_groups and I'm not sure a comm_group can be a Z-module in Lean.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:25):

bleurgh I now get errors in polyhedral_lattice.finsupp. Maybe I'll leave this until after the int refactor, my guess is that I have clashing semimodule instances here.

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

@Kevin Buzzard All of this will be solved in 1 or 2 days, when @Sebastien Gouezel's gsmul PR is merged into mathlib.

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

So I would suggest to just add [semimodule int A] assumptions for now, and we'll remove them in two days.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 21:44):

The next problem I find I'm running into is that I'm reluctant to do anything involving is_basis now Anne has told us that they're bundling it. Right now I'm sorrying a bunch of basic algebra stuff and just trying to push on with the more serious stuff.

view this post on Zulip Eric Wieser (Apr 21 2021 at 18:32):

It seems that every time I try to generalize things about finsupp / add_monoid_algebra / dfinsupp / direct_sum, it makes things harder not easier for me... After making what I thought would be some handy API in #7217 and #7293, I had to fight an more-awful-than-before battle against the elaborator, and a similarly awful fight with ext. In the end I was able to construct:

/-- There is a ring equivalence between an `add_monoid_algebra` (e.g. a `polynomial`) and
the direct sum of `single_mrange k i` (e.g. the monomials of degree `i`). -/
def to_direct_sum_mrange : add_monoid_algebra k G ≃+*  i : G, single_mrange k i := _

view this post on Zulip Kevin Buzzard (Apr 21 2021 at 18:44):

But these feel to me like the things we need in the API, so it's great that you're managing to do them; hopefully users can just hide behind what you're doing. The maps are nice, the proofs are hard but hopefully people will only need the maps.

view this post on Zulip Eric Wieser (Apr 21 2021 at 18:50):

But even using the maps was hard

view this post on Zulip Eric Wieser (Apr 21 2021 at 18:50):

See my first link

view this post on Zulip Eric Wieser (Apr 21 2021 at 18:51):

@ and letI everywhere

view this post on Zulip Johan Commelin (Apr 21 2021 at 19:04):

It's great that you are working on this! I haven't had the time, energy, and guts to work on this so far.

view this post on Zulip Johan Commelin (Apr 21 2021 at 19:05):

But I'm wondering if things become easier when you try to do everything in terms of internal sums? So without dfinsupp.

view this post on Zulip Eric Wieser (Apr 21 2021 at 19:26):

By internal sum I assume you mean some subtype of finsupp?

view this post on Zulip Johan Commelin (Apr 21 2021 at 19:32):

Well, or maybe even submodules of add_monoid_algebra

view this post on Zulip Johan Commelin (Apr 21 2021 at 19:32):

Can we have an "intrinsic" definition of graded_ring?

view this post on Zulip Eric Wieser (Apr 21 2021 at 19:39):

Part of the motivation here was to enable a graded ring whose components are docs#pi_tensor_product

view this post on Zulip Eric Wieser (Apr 21 2021 at 19:39):

For which an external direct sum is easier

view this post on Zulip Eric Wieser (Apr 21 2021 at 20:07):

But I suppose you can always have an internal direct sum of a sigma type

view this post on Zulip Adam Topaz (Apr 21 2021 at 20:25):

Graded ring = monoid object in the category of graded abelian groups. Can we make such a definition useful?

view this post on Zulip Kevin Buzzard (Apr 21 2021 at 21:31):

Probably all the problems are there already in grading abelian groups?

view this post on Zulip Kevin Buzzard (Apr 25 2021 at 23:05):

Adam gave an update so I thought I'd give one too. I've had to made an API for gradings on rings and this has turned out to be delicate, just for stupid reasons: R=mRmR=\bigoplus_mR_m but the RmR_m are either additive subgroups of RR or abstract groups in their own right, so it seems that there are several ways of stating things, and I'm still not sure which is the most useful. For example I've managed to state in no fewer than four ways the fact that if rRmr\in R_m then the mth component of rr is rr. The main problem of course is that R=mRmR=\bigoplus_m R_m is not true in Lean -- instead RmRmR\cong \bigoplus_m R_m and neither map is remotely close to being the identity.

I've reduced Gordan's Lemma (modulo some easy sorrys which I'm reluctant to fill in because is_basis is being refactored) to this lemma in commutative algebra that if AA is Noetherian and Z\Z-graded then A0A_{\geq0} is finitely-generated over A0A_0, plus the assertion that if ϕ:ZnZ\phi:\Z^n\to\Z is non-zero then the kernel is finite free of rank less than nn. The former fact will be possible but of course we'll have the usual nonsense about how A0A_0 and A0A_{\geq0} are subrings but we want to consider them as rings and algebras etc etc; I've struggled through stuff like this before and I'm sure it will be possible. As for the subgroups of Zn\Z^n, I'm just hoping that we will have enough general machinery to make this not too hard.

view this post on Zulip Peter Scholze (May 03 2021 at 19:13):

It sounds like Coq may now have enough basics on polyhedral stuff for the "convex geometry" proof of Gordan's lemma https://arxiv.org/abs/2104.15021

view this post on Zulip Patrick Massot (May 03 2021 at 19:34):

Are you now following computer science and logic on arXiv? Johan, what have we done?

view this post on Zulip Peter Scholze (May 03 2021 at 19:39):

No I'm not, no worries

view this post on Zulip Kevin Buzzard (May 03 2021 at 19:50):

@Bhavik Mehta and @Yaël Dillies are developing a lot of convex geometry on the Discord.

view this post on Zulip Yaël Dillies (May 03 2021 at 19:51):

Oh hey yeah! Anything you need?

view this post on Zulip Johan Commelin (May 03 2021 at 19:52):

A port of that paper would be nice :stuck_out_tongue_wink:

view this post on Zulip Bhavik Mehta (May 03 2021 at 20:13):

I think we might have enough convex geometry to get close to the geometry proof of Gordan's lemma since we have Krein-Milman, HB and supporting/separating hyperplane lemmas

view this post on Zulip Bhavik Mehta (May 03 2021 at 20:15):

But from talking to @Kevin Buzzard I understand it might be better to get the algebraic proof so that the theory of graded rings gets developed better?

view this post on Zulip Johan Commelin (May 03 2021 at 20:15):

Well, we should have both, so that the theory of convex polyhedra and the theory of graded rings get developed better

view this post on Zulip Yaël Dillies (May 05 2021 at 16:00):

I read through the paper and all of this sounds very doable and interesting! I'm already PRing exposed faces, and then Krein-Milman. We shall see how far I get on the rest.

view this post on Zulip Yaël Dillies (May 05 2021 at 16:01):

Ah, and Bhavik seems to be already gone proving Gordan's lemma :sweat_smile:

view this post on Zulip Kevin Buzzard (May 05 2021 at 16:06):

Yes he's live streaming the topological proof on discord right now

view this post on Zulip Riccardo Brasca (May 07 2021 at 14:00):

If we are still interested in the algebraic proof add_monoid_algebra.finite_type_iff_fg is now in mathlib. I will add the easy (and I think useless for LTE) version for groups next week.

view this post on Zulip Johan Commelin (May 07 2021 at 15:05):

I think the algebraic proof is still the one we are aiming for.

view this post on Zulip Johan Commelin (May 07 2021 at 15:07):

Unless @Bhavik Mehta and @Yaël Dillies think they can prove explicit_gordan before Kevin is done with grading exams, of course.

view this post on Zulip Bhavik Mehta (May 07 2021 at 15:48):

That depends on whether Kevin finishes grading exams by Monday or not :wink:

view this post on Zulip Johan Commelin (May 07 2021 at 16:05):

Ha! You think you'll be done by Monday? Sounds great!

view this post on Zulip Kevin Buzzard (May 07 2021 at 19:09):

@Bhavik Mehta just to be clear, there are several "Gordan's Lemma"s in the literature -- the one we want is much stronger than the one we were talking about recently, it needs all that matrix elimination stuff. I pointed you to precisely the lemma we needed in the LTE IIRC

view this post on Zulip Bhavik Mehta (May 07 2021 at 19:45):

Kevin Buzzard said:

Bhavik Mehta just to be clear, there are several "Gordan's Lemma"s in the literature -- the one we want is much stronger than the one we were talking about recently, it needs all that matrix elimination stuff. I pointed you to precisely the lemma we needed in the LTE IIRC

In what sense is it much stronger? I think the only difference from the one we talked about (with finite intersections of rational hyperplanes) was that the version I was doing was for Z^n rather than any more general version

view this post on Zulip Kevin Buzzard (May 07 2021 at 20:30):

Bhavik, if you can prove the version in LTE that would be absolutely fabulous. I am just pointing out that you showed me a lemma in a book and the lemma was called Gordan's Lemma but it was not what we are calling Gordan's Lemma, and what we want is what we are calling Gordan's Lemma.

view this post on Zulip Kevin Buzzard (May 07 2021 at 20:34):

We were initially going to do the topological proof, but then I decided that the algebraic proof looked easier, so I started on this, but then internal grading turned out to be subtle (but do-able) so I'm persevering with it, but now the topological proof is looking easier again.

I just did rw submodule.smul_mem and it failed, so I did rw @submodule.smul_mem [fill in all the fields] and this happened. Note that pp.all was off, I just triggered the Lean "display more information if the pretty printer says that the terms match but I know they don't".

view this post on Zulip Kevin Buzzard (May 07 2021 at 20:38):

But my work will not be wasted because we have developed a grading API and I'm putting it through its paces (I suspect I know what I did wrong to get that error, by the way!)

view this post on Zulip Kevin Buzzard (May 07 2021 at 22:48):

If I use convert instead of refine then my 2000-line-long error turns into

grade_zero.has_scalar (λ (i : A), (G i)) a = smul_with_zero.to_has_scalar

Last updated: May 09 2021 at 23:10 UTC