toric

Stream: condensed mathematics

[Damiano Testa]

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!

[Damiano Testa]

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

[Johan Commelin]

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

[Johan Commelin]

Be sure to git pull before working on master

[Damiano Testa]

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

[Damiano Testa]

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.

[Riccardo Brasca]

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?

[Filippo A. E. Nuccio]

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?

[Damiano Testa]

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!

[Filippo A. E. Nuccio]

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?

[Damiano Testa]

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.

[Filippo A. E. Nuccio]

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.

[Damiano Testa]

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.

[Filippo A. E. Nuccio]

The statement I am using is

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

[Filippo A. E. Nuccio]

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

[Damiano Testa]

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.

[Damiano Testa]

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.

[Damiano Testa]

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.

[Damiano Testa]

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

[Riccardo Brasca]

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:

[Filippo A. E. Nuccio]

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.

[Damiano Testa]

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.

[Riccardo Brasca]

I will have a look at towards_Gordan, thank you!

[Damiano Testa]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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:

[Peter Scholze]

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?

[Damiano Testa]

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.

[Damiano Testa]

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.

[Damiano Testa]

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

[Peter Scholze]

@Damiano Testa OK, sounds great!

[Riccardo Brasca]

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.

[Bryan Gin-ge Chen]

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

[Riccardo Brasca]

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.

[Bryan Gin-ge Chen]

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

[Riccardo Brasca]

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

[Bryan Gin-ge Chen]

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

[Riccardo Brasca]

Let me see

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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.

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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.

[Johan Commelin]

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.

[Johan Commelin]

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

[Damiano Testa]

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?

[Yakov Pechersky]

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

[Damiano Testa]

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!

[Damiano Testa]

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.

[Yakov Pechersky]

Can you try int_module and semiring.to_semimodule instead?

[Damiano Testa]

with int_module I still get unknown identifier 'int_module'.

[Damiano Testa]

(however, lean recognized semiring.to_semimodule)

[Yakov Pechersky]

@add_comm_group.int_module \Z (by apply_instance)

[Damiano Testa]

Lean considers this a valid statement:

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

[Damiano Testa]

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

[Yakov Pechersky]

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.

[Johan Commelin]

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$-modules.

[Damiano Testa]

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!

[Damiano Testa]

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.

[Damiano Testa]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Damiano Testa]

Sorry, having breakfast!

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Damiano Testa]

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?

[Damiano Testa]

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

[Yakov Pechersky]

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

[Damiano Testa]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Consider this tactic step:

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

[Yakov Pechersky]

Switching it to just

  refine ⟨n, b, _⟩,

[Yakov Pechersky]

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

[Yakov Pechersky]

image.png

[Yakov Pechersky]

image.png

[Damiano Testa]

I see: ordered_ring vs domain.

[Yakov Pechersky]

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?

[Damiano Testa]

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!

[Yakov Pechersky]

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

[Damiano Testa]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Could be? I'm not sure yet.

[Damiano Testa]

Let me try to work this out.

[Damiano Testa]

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

[Damiano Testa]

I am tempted to say that it is this one:

submodule.restrict_scalars ℤ s

[Yakov Pechersky]

What about that submodule?

[Damiano Testa]

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

[Yakov Pechersky]

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

[Damiano Testa]

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!

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Riccardo Brasca]

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

[Damiano Testa]

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) _),

[Riccardo Brasca]

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.

[Damiano Testa]

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.

[Yakov Pechersky]

Ah there is another difference

[Damiano Testa]

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

[Yakov Pechersky]

Not sure if it is a meaningful one

[Yakov Pechersky]

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

[Yakov Pechersky]

Those are also rfl =/

[Damiano Testa]

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?

[Sebastien Gouezel]

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

[Yakov Pechersky]

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

[Damiano Testa]

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

[Sebastien Gouezel]

Thanks!

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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.

[Damiano Testa]

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

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

Minimal diamond:

import linear_algebra.free_module

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

both instances are registered in mathlib.

[Yakov Pechersky]

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

[Johan Commelin]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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!

[Eric Wieser]

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

[Sebastien Gouezel]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

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.

[Riccardo Brasca]

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

[Kevin Buzzard]

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?

[Yakov Pechersky]

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

[Yakov Pechersky]

Because you get noncomputable fintype from set.finite anyway

[Yakov Pechersky]

And then you don't have to juggle sort coercions

[Riccardo Brasca]

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

[Johan Commelin]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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!

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Yakov Pechersky]

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.

[Damiano Testa]

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

[Damiano Testa]

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

[Yakov Pechersky]

Yeah, possibly

[Damiano Testa]

Ok, I pushed the change.

Thanks!

[Damiano Testa]

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

[Yakov Pechersky]

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

[Damiano Testa]

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:

[Damiano Testa]

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

[Yakov Pechersky]

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

[Damiano Testa]

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

[Yakov Pechersky]

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

[Damiano Testa]

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

[Yakov Pechersky]

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

[Damiano Testa]

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

[Yakov Pechersky]

which branch are you on?

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Damiano Testa]

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!

[Riccardo Brasca]

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.

[Riccardo Brasca]

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.

[Sebastien Gouezel]

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

[Sebastien Gouezel]

Never mind, problem solved :-)

[Johan Commelin]

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

[Johan Commelin]

I feel somewhat responsible for maintaining Witt vectors (-;

[Damiano Testa]

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 $\phi (n)$ if it has $n$ 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!

[Sebastien Gouezel]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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$-module, andexplicit_dual_set l is the sub-$\mathbb{N}$-module of $\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 $\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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Damiano Testa]

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!

[Damiano Testa]

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!

[Damiano Testa]

This is an outline:

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Damiano Testa]

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.

[Damiano Testa]

Let me answer more in detail your questions.

[Damiano Testa]

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.

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

This is via the dual_set process.

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

(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 $N$ for the module.)

Let $M$ and $N$ 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 $N$ and and they are the Z- (resp. N-)linear combinations of the elements of the basis.

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

Start with a finite set s of $M$.
The dual_set of s is an N-submodule of $N$. 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.

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

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.

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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.

[Filippo A. E. Nuccio]

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.

[Filippo A. E. Nuccio]

(deleted)

[Kevin Buzzard]

I still don't see the proof we're trying to formalise. You say "we should prove that the elements of $S^\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?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Damiano Testa]

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!

[Johan Commelin]

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.

[Damiano Testa]

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!

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Damiano Testa]

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!

[Damiano Testa]

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

[Damiano Testa]

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.

[Riccardo Brasca]

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.

[Damiano Testa]

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!

[Damiano Testa]

Comments are welcome!

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Peter Scholze]

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

[Adam Topaz]

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

[Johan Commelin]

Nope, not yet, unfortunately :sad:

[Kevin Buzzard]

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.

[Adam Topaz]

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

[Kevin Buzzard]

I think Patrick finished this recently.

[Riccardo Brasca]

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

[Adam Topaz]

Nice!

[Adam Topaz]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Damiano Testa]

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 $\mathbb{Z}$-/$\mathbb{N}$-modules.

[Damiano Testa]

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.

[Riccardo Brasca]

@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

[Damiano Testa]

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!

[Damiano Testa]

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

[Damiano Testa]

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

[Riccardo Brasca]

We already have monoid_algebrawith an API

[Damiano Testa]

The ring $R[M]$ is $M$-graded, and later we will want to do a Noetherian induction on the $\mathbb{Z}$-graded ring $A$. 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.

[Damiano Testa]

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.

[Damiano Testa]

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

[Riccardo Brasca]

I have no idea about graded stuff in mathlib, but $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).

[Riccardo Brasca]

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?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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$-module then it has a well-defined rank $r(\Lambda)$, and the theorem that if $\phi:\Lambda\to\Z$ is non-zero then the kernel of $\phi$ is also a finite free $\Z$-module, with strictly smaller rank.

[Riccardo Brasca]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I am also very much hoping that we can extract this argument about $A_{\geq0}$ being finitely-generated over $A_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 $A_0$ is a subring, sorry the proof it's finitely-generated over the base field, sorry the proof that $A_{\geq0}$ is finitely-generated over $A_0$, now see if you can use results in the library to prove $A_{\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).

[Kevin Buzzard]

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, $A_{\geq0}$ is finitely-generated over $A_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.

[Kevin Buzzard]

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.

[Adam Topaz]

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

[Kevin Buzzard]

It's in a pdf on the toric branch

[Adam Topaz]

Ah ok

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Riccardo Brasca]

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

[Adam Topaz]

Yeah I'm looking at it now...

[Adam Topaz]

Oh this should totally be doable with current mathlib

[Riccardo Brasca]

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

[Kevin Buzzard]

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 $A_{\geq0}$ being finitely-generated over $A_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.

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Adam Topaz]

We recently got docs#is_free_group

[Adam Topaz]

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

[Adam Topaz]

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

[Riccardo Brasca]

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.

[Riccardo Brasca]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

No thanks :sweat_smile:

[Riccardo Brasca]

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) = ⊤ :=

[Johan Commelin]

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

[Kevin Buzzard]

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.

[Damiano Testa]

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.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Eric Wieser]

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)

[Damiano Testa]

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.

[Kevin Buzzard]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Kevin Buzzard]

hmm :-)

[Kevin Buzzard]

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)

?

[Eric Wieser]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

re syntax error: just end with := sorry

[Eric Wieser]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Kevin Buzzard]

Eric Wieser said:

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

Yes.

[Eric Wieser]

... and is that easy to prove?

[Kevin Buzzard]

Oh -- at least in the add_subgroup case.

[Kevin Buzzard]

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

[Damiano Testa]

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?

[Eric Wieser]

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

[Damiano Testa]

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

[Kevin Buzzard]

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)

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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?

[Eric Wieser]

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

[Eric Wieser]

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

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

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!

[Kevin Buzzard]

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.

[Eric Wieser]

Oh, nice catch

[Adam Topaz]

Just make the functiongraded_piece injective?

[Riccardo Brasca]

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

[Eric Wieser]

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

[Adam Topaz]

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?

[Adam Topaz]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

span is just a statement about a Sup

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

Aha, this is some monoid scheme maybe

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Eric Wieser]

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.

[Adam Topaz]

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.

[Kevin Buzzard]

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

[Filippo A. E. Nuccio]

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.

[Julian Külshammer]

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

[Damiano Testa]

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

[Riccardo Brasca]

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

[Kevin Buzzard]

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.

[Riccardo Brasca]

We already have this!

[Kevin Buzzard]

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.

[Damiano Testa]

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!

[Kevin Buzzard]

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.

[Damiano Testa]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Damiano Testa]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

I'll formalise the statement of what I'm thinking of and then push to grading.

[Damiano Testa]

Ok, thanks a lot!

[Kevin Buzzard]

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.

[Damiano Testa]

Thanks a lot, Kevin, for grading and for the instructions!

[Eric Wieser]

You're describing branch#grading in mathlib not lean-liquid, right?

[Damiano Testa]

I certainly assumed so: I pulled grading from mathlib.

[Eric Wieser]

For polynomials i'd expect it's far easier to directly construct the inverse mapping to show bijectivity

[Eric Wieser]

Which is just "sum direct_sum.of I ⟨monomial i (p.coeff i), sorry⟩ over p.support"

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh, I've got it: RHS doesn't know which poly ring. Sorry for the noise.

[Kevin Buzzard]

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?

[Eric Wieser]

Man, the elaborator is really getting the upper hand on you today

[Eric Wieser]

My orange bars aren't cooperating so I can't help you yet

[Eric Wieser]

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)

[Eric Wieser]

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)

[Eric Wieser]

IN fact, it's the ⇑ causing you all the pain in your example

[Kevin Buzzard]

Thanks! I put the ⇑ in because it wasn't working without it (indeed what I posted doesn't work without the ⇑ either)

[Kevin Buzzard]

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.

[Yakov Pechersky]

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

[Eric Wieser]

Kevin Buzzard said:

(indeed what I posted doesn't work without the ⇑ either)

It does once you replace the → with →+ I think

[Kevin Buzzard]

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 }

[Kevin Buzzard]

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

[Kevin Buzzard]

I got so frustrated with this that I just decided to prove the mem_supr lemmas :-)

[Eric Wieser]

Why not define it as an add_equiv?

[Kevin Buzzard]

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.

[Eric Wieser]

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) →+ _) }

[Kevin Buzzard]

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

[Eric Wieser]

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)

[Yakov Pechersky]

simp ..., refl also known as simpa

[Eric Wieser]

simp [monomial] is needed because you're not supposed to use finsupp.lift_add_hom on polynomials

[Kevin Buzzard]

oh it doesn't compile for me :-(

[Kevin Buzzard]

hmm, works on master, I'll have to merge into my branch.

[Kevin Buzzard]

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)

[Damiano Testa]

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

[Eric Wieser]

Right, a monoid_algebra version is probably sensible

[Eric Wieser]

You can use finsupp.single_add_hom instead of touching lsingle

[Damiano Testa]

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?

[Damiano Testa]

Am I missing something?

[Damiano Testa]

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

[Eric Wieser]

I think actually we want the version relating dfinsupp and finsupp

[Damiano Testa]

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)

[Eric Wieser]

So replace add_monoid_algebra with finsupp, and direct_sum with dfinsupp

[Damiano Testa]

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!

[Eric Wieser]

Well those types are defeq!

[Eric Wieser]

I'll PR a dfinsupp / finsupp version tomorrow

[Damiano Testa]

Well those types are defeq!

Aaah, that explains why Lean simply liked all of it!

[Eric Wieser]

If you're looking for practice, we probably want a linear_equiv / submodule version of that def too

[Damiano Testa]

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!

[Eric Wieser]

The key trick in the proof was to phrase things in a way that ext could pick up

[Damiano Testa]

Btw, what is the : 2 in ext?

[Eric Wieser]

Ie, by solving f.comp f_inv = id

[Eric Wieser]

"don't expand as far as p.coeff I"

[Damiano Testa]

ah, like congr' 2?

[Eric Wieser]

It means "apply ext twice"

[Damiano Testa]

except with ext?

[Eric Wieser]

Yes

[Damiano Testa]

I squeezed the the two simps to speed up the processing: there is quite a lot of lemmas that show up!

[Damiano Testa]

Anyway, I'm off for the day!

Kevin and Eric, thanks a lot for gradings!

[Kevin Buzzard]

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.

[Kevin Buzzard]

For polynomials this was easy. So this looks like it's a workable definition.

[Eric Wieser]

#7217

[Eric Wieser]

Typeclass search really wasn't happy here

[Eric Wieser]

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

[Kevin Buzzard]

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.

[Eric Wieser]

Have a look at src#add_monoid_hom.range, it solves that problem

[Eric Wieser]

Once my other two cleanup PRs go though (#7218, #7220), I'll see what breaks if we do that everywhere

[Kevin Buzzard]

docs#subgroup.range ?

[Eric Wieser]

Oops, fixed

[Eric Wieser]

It uses docs#subgroup.copy to make it definitionally useful

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Johan Commelin]

@Kevin Buzzard All of this will be solved in 1 or 2 days, when @Sebastien Gouezel's gsmul PR is merged into mathlib.

[Johan Commelin]

So I would suggest to just add [semimodule int A] assumptions for now, and we'll remove them in two days.

[Kevin Buzzard]

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.

[Eric Wieser]

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 := _

[Kevin Buzzard]

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.

[Eric Wieser]

But even using the maps was hard

[Eric Wieser]

See my first link

[Eric Wieser]

@ and letI everywhere

[Johan Commelin]

It's great that you are working on this! I haven't had the time, energy, and guts to work on this so far.

[Johan Commelin]

But I'm wondering if things become easier when you try to do everything in terms of internal sums? So without dfinsupp.

[Eric Wieser]

By internal sum I assume you mean some subtype of finsupp?

[Johan Commelin]

Well, or maybe even submodules of add_monoid_algebra

[Johan Commelin]

Can we have an "intrinsic" definition of graded_ring?

[Eric Wieser]

Part of the motivation here was to enable a graded ring whose components are docs#pi_tensor_product

[Eric Wieser]

For which an external direct sum is easier

[Eric Wieser]

But I suppose you can always have an internal direct sum of a sigma type

[Adam Topaz]

Graded ring = monoid object in the category of graded abelian groups. Can we make such a definition useful?

[Kevin Buzzard]

Probably all the problems are there already in grading abelian groups?

[Kevin Buzzard]

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=\bigoplus_mR_m$ but the $R_m$ are either additive subgroups of $R$ 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 $r\in R_m$ then the mth component of $r$ is $r$. The main problem of course is that $R=\bigoplus_m R_m$ is not true in Lean -- instead $R\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 $A$ is Noetherian and $\Z$-graded then $A_{\geq0}$ is finitely-generated over $A_0$, plus the assertion that if $\phi:\Z^n\to\Z$ is non-zero then the kernel is finite free of rank less than $n$. The former fact will be possible but of course we'll have the usual nonsense about how $A_0$ and $A_{\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 $\Z^n$, I'm just hoping that we will have enough general machinery to make this not too hard.

[Peter Scholze]

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

[Patrick Massot]

Are you now following computer science and logic on arXiv? Johan, what have we done?

[Peter Scholze]

No I'm not, no worries

[Kevin Buzzard]

@Bhavik Mehta and @Yaël Dillies are developing a lot of convex geometry on the Discord.

[Yaël Dillies]

Oh hey yeah! Anything you need?

[Johan Commelin]

A port of that paper would be nice :stuck_out_tongue_wink:

[Bhavik Mehta]

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

[Bhavik Mehta]

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?

[Johan Commelin]

Well, we should have both, so that the theory of convex polyhedra and the theory of graded rings get developed better

[Yaël Dillies]

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.

[Yaël Dillies]

Ah, and Bhavik seems to be already gone proving Gordan's lemma :sweat_smile:

[Kevin Buzzard]

Yes he's live streaming the topological proof on discord right now

[Riccardo Brasca]

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.

[Johan Commelin]

I think the algebraic proof is still the one we are aiming for.

[Johan Commelin]

Unless @Bhavik Mehta and @Yaël Dillies think they can prove explicit_gordan before Kevin is done with grading exams, of course.

[Bhavik Mehta]

That depends on whether Kevin finishes grading exams by Monday or not :wink:

[Johan Commelin]

Ha! You think you'll be done by Monday? Sounds great!

[Kevin Buzzard]

@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

[Bhavik Mehta]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Bhavik Mehta]

Johan Commelin said:

Ha! You think you'll be done by Monday? Sounds great!

A little late, but the gordan-bm branch of LTE now has an almost sorry-free proof of Gordan's lemma: the only sorry in the proof is showing that the dual of a finite free group is finite free; I'm pretty sure this is easy but I left it in case someone else was already doing it

[Adam Topaz]

This last fact is probably even in mathlib!

[Bhavik Mehta]

I think dual bases in mathlib are only for fields currently?

[Adam Topaz]

docs#basis.dual_basis

[Adam Topaz]

Ah yeah

[Bhavik Mehta]

Right, it requires K to be a field whereas here it's the integers

[Adam Topaz]

That's a shame

[Bhavik Mehta]

I think it should mostly work for rings still

[Adam Topaz]

If I have time I'll try to generalize that dual basis in mathlib.

[Adam Topaz]

I want to play with these bundled bases anyway

[Riccardo Brasca]

Mathlib probably needs a good API for free modules anyway. My plan for next week was to start working on the rank of the kernel of a non zero $\mathbf{Z}^n \to \mathbf{Z}$ and see what is missing.

[Adam Topaz]

Do we even have module.is_free or something like that?

[Riccardo Brasca]

I think Johan suggested to make a classe finite_free and build and API

[Riccardo Brasca]

I don't think we have module.is_free, at least looking at how docs#submodule.basis_of_pid is stated

[Kevin Buzzard]

So we have projective modules and flat modules but not free modules?? :-) PS @Jon Eugster you might like it over here.

[Adam Topaz]

FYI: The section involving docs#basis.dual_basis ccompiles just fine if one replaces [field K] with [comm_ring K], except for docs#basis.dual_dim_eq which relies on the definition of module.rank which requires a field. I guess doing this properly would require defining the rank of a module which has a basis and showing that it doesn't depend on the choice of basis, and I don't have the energy to do such a large refactor...

[Johan Commelin]

I think it's a good idea to generalize all the dual basis stuff. (And just leave dual_dim_eq for fields, for now.)

[Johan Commelin]

In a separate refactor module.rank can be generalized.

[Johan Commelin]

Note that @Markus Himmel added invariant_basis_number to mathlib some while ago, and I've already used it succesfully for some of the finite_free sorries in LTE.

[Johan Commelin]

I'm preparing a PR generalising dual basis

[Johan Commelin]

#7599

[Johan Commelin]

It's on the merge queue, so hopefully we will have a sorry-free gordan in a couple of hours

[Kevin Buzzard]

Well done to @Bhavik Mehta who pushed through the topological proof in the end. So what is the current status of the proof of 9.4 of Analytic.pdf?

[Kevin Buzzard]

Well done to @Bhavik Mehta who pushed through the topological proof in the end. So what is the current status of the proof of 9.4 of Analytic.pdf?

[Johan Commelin]

The current status is that Patrick is making good progress on 9.2.
And I want to define the Cech nerves that we need for col_exact pretty soon. But we need to find a timeslot where Adam and me are both available. And theres something like 8 hrs of timezone difference...

[Johan Commelin]

I also want to do some refactoring, to make things smoother.

[Patrick Massot]

So in the end this whole formalized maths thing has some connection to reality: each time topology and algebra can both be used, the topology proof is nicer!

[Johan Commelin]

For example, 9.2 is currently stated for arbitrary powers of M. But that is very unnatural.

[Patrick Massot]

Hopefully I'll have time to work on 9.2 today. Johan, did you read https://github.com/leanprover-community/lean-liquid/blob/master/src/prop_92/concrete.lean?

[Patrick Massot]

Reading it is not necessary, but I think you may find it interesting

[Johan Commelin]

I read it a while ago. Let me have another look.

[Johan Commelin]

I like the abstraction over Tinv. And doing the T_inv _ Tinv conjugation in the induction. It seems to work very well.

[Kevin Buzzard]

Here is an example of what was slowing me down with the algebraic proof. Say $R$ is a commutative ring and then later on you come up with a $\Z$-grading on $R$, so additive subgroups $R_n$ for $n\in\Z$ with $1\in R_0$ and $R_mR_n\subseteq R_{m+n}$ and such that $R=\bigoplus R_n$ (this is "=" in the obvious untrue sense). I proved that if $R$ was Noetherian then $R_n$ was a finitely-generated $R_0$-module generated by a finset $S_n\subseteq R_n$, and next I want to prove that $R_{\geq0}$ is a finitely-generated $R_0$-algebra, but now you have to move your finite generators of the promoted-to-type $R_n$ for $n\geq0$ into the also promoted-to-a-type $R_{\geq0}$, defined as the $r$ such that $r_z=0$ for $z<0$, and you have to move your theorem which says that an arbitrary $r\in R_n$ is spanned by $S_n$ to a theorem which says that the corresponding $r\in R_{\geq0}$ is in the $R_0$-span of the moved $S_n$ etc. Now I write I realise that I should write down an $R_0$-module morphism from $R_n$ to $R_{\geq0}$ if $n\geq0$. There were just tons of dumb things like this, as well as having to make the internal grading API from scratch, and I didn't have enough Lean time in the day to make progress at more than a snail's pace (when marking is over I should be in a much better state though).

We will need grading when we do Proj for schemes, so I've known for a while we need a good grading API, and I'm optimistic that ultimately the API I've made for internal gradings, when tidied up (my next job) will be helpful here.

[Bhavik Mehta]

By the way I did a lazy proof that the dual is finite free by hand just to be sure that my Gordan proof worked, so it's technically already sorry free! But of course the proof that should come from your PR is much better