# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: toric

#### Damiano Testa (Feb 28 2021 at 19:03):

An update from the `toric`

branch.

I just pushed the latest version of `toric`

: it has several `sorries`

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

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

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

#### Damiano Testa (Feb 28 2021 at 19:04):

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

#### Johan Commelin (Mar 09 2021 at 09:03):

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

#### Johan Commelin (Mar 09 2021 at 09:03):

Be sure to `git pull`

before working on master

#### Damiano Testa (Mar 30 2021 at 19:50):

I pushed a few more additions to the `toric`

branch: it is not yet ready for unguided `sorry`

-proving, but it is getting there!

#### Damiano Testa (Mar 30 2021 at 19:50):

I work more on it this week and hopefully soon I will be able to have `sorry`

s that can be proven with minimal insider knowledge.

#### Riccardo Brasca (Mar 30 2021 at 21:07):

I would like to help with Gordan's lemma! Do you think it's better to wait to have some more readable `sorry`

or should I try to read the code now?

#### Filippo A. E. Nuccio (Mar 31 2021 at 06:22):

I was thinking that the statement of Gordan's lemma should end up in some of the `toric`

file, and that it gets simply quoted in `lem97`

. I think this would make it easier to adapt the form you'll prove to the one that I'm using. Do you agree? And, if yes, where would you suggest that I insert it?

#### Damiano Testa (Mar 31 2021 at 07:35):

Dear All,

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

s 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 (Mar 31 2021 at 07:37):

And do you think `towards_Gordan`

will eventually become `Gordan`

(i.e. : I can insert the statement there and refer to it) or do you plan to have two files?

#### Damiano Testa (Mar 31 2021 at 07:38):

Filippo, I am now upgrading my branch to the current `master`

. I will check the exact statement of Lemma 9.7 and will see how to fit it with what I have.

#### Filippo A. E. Nuccio (Mar 31 2021 at 07:39):

Thanks, at any rate I find it most reasonable to put what I use in the `toric`

directory, and that I quote it from there. If the statement you end up with is not exactly the one I am using, we can write the bridge between the two there more easily, I guess.

#### Damiano Testa (Mar 31 2021 at 07:40):

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

#### Filippo A. E. Nuccio (Mar 31 2021 at 07:40):

The statement I am using is

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

#### Filippo A. E. Nuccio (Mar 31 2021 at 07:41):

where

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

#### Damiano Testa (Mar 31 2021 at 07:42):

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

folder.

I am building the `toric`

branch now, with the `master`

that I just merged.

#### Damiano Testa (Mar 31 2021 at 07:44):

Ok, I have not yet fixed the `nat_submodule`

issue, but, apart from that, I am getting close to having the function `l`

appearing in `explicit_dual_set`

defined.

#### Damiano Testa (Mar 31 2021 at 07:46):

Ok, `master`

merged with no issues into `toric`

, `leanproject build`

also only warned me about `sorry`

s 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 (Mar 31 2021 at 07:53):

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

#### Riccardo Brasca (Mar 31 2021 at 07:57):

I will try to read what you have done in the next days, so please don't hesitate to leave a lot of small `sorry`

(even inside proofs!)... killing them is my favorite way of getting used to new stuff :big_smile:

#### Filippo A. E. Nuccio (Mar 31 2021 at 08:01):

Damiano Testa said:

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

`toric`

folder.I am building the

`toric`

branch now, with the`master`

that I just merged.

Ok, are you going to put it somewhere and `push`

to `master`

? In that way, I can adapt my branch and when I'll `push`

to `master`

that part will be solid.

#### Damiano Testa (Mar 31 2021 at 08:01):

Riccardo, If you stick to the file `towards_Gordan`

, the `sorry`

s 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 `sorry`

s outside of `towards_Gordan`

are more of a playground, than actual steps in the formalization.

#### Riccardo Brasca (Mar 31 2021 at 08:03):

I will have a look at `towards_Gordan`

, thank you!

#### Damiano Testa (Mar 31 2021 at 08:12):

Filippo, maybe the best thing would be to simply move the file `lem97.lean`

into the `toric`

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

#### Johan Commelin (Mar 31 2021 at 08:15):

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

#### Johan Commelin (Mar 31 2021 at 08:16):

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

#### Filippo A. E. Nuccio (Mar 31 2021 at 08:20):

Oh I certainly agree it will be easy. OK, I will move`lem97 `

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 (Mar 31 2021 at 08:29):

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

#### Damiano Testa (Mar 31 2021 at 08:46):

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

Quickly, here is my strategy.

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

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

#### Damiano Testa (Mar 31 2021 at 08:47):

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

#### Damiano Testa (Mar 31 2021 at 08:49):

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

#### Peter Scholze (Mar 31 2021 at 09:22):

@Damiano Testa OK, sounds great!

#### Riccardo Brasca (Mar 31 2021 at 21:11):

I have proved `reduction_to_lattice`

here

https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/toric/towards_Gordan.lean

There is something I don't understand in the proof: I have the impression that the hypothesis I called `goal`

is exactly what we want to prove, but `exact goal`

doesn't work. If you try to play with it it's very easy to get to a point where you need to prove `foo`

and you have `foo`

in the local context, but there should be some problem with possibly different `ℤ`

-actions. If someone wants to play with it feel free to modify it... at the moment it is very ugly.

#### Bryan Gin-ge Chen (Mar 31 2021 at 21:17):

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

#### Riccardo Brasca (Mar 31 2021 at 21:21):

I did it, in line `80`

. The goal becomes

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

After `ext i`

the goal becomes

```
↑(g i • b i) = ↑(g i • b i)
```

I proved this by induction on `g i`

, that is an integer. The proof worked because essentially `zero_smul`

`add_smul`

,`sub_smul`

and `one_smul`

work for any `•`

, but I don't know how to do it better.

#### Bryan Gin-ge Chen (Mar 31 2021 at 21:23):

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

#### Riccardo Brasca (Mar 31 2021 at 21:25):

It must have something to to with coercion from `Λ₁`

to submodules of `V`

, or something like that.

#### Bryan Gin-ge Chen (Mar 31 2021 at 21:25):

Hmm, is it something that `norm_cast`

should be helping with?

#### Riccardo Brasca (Mar 31 2021 at 21:26):

Let me see

#### Riccardo Brasca (Mar 31 2021 at 21:36):

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

#### Riccardo Brasca (Mar 31 2021 at 21:46):

Ah! A combination of `norm_cast`

and `congr`

simplified the proof quite a lot

#### Riccardo Brasca (Mar 31 2021 at 22:36):

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

.

#### Damiano Testa (Apr 01 2021 at 03:19):

@Riccardo Brasca thank you very much for your help!

Feel free to push your proof to `toric`

!

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

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

#### Damiano Testa (Apr 01 2021 at 04:27):

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

```
-- general fact, also asked in mathlib
lemma algebra_map.injective.linear_independent {R S M ι : Type*} [comm_semiring R] [semiring S]
[add_comm_monoid M] [algebra R S] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
(hinj : function.injective (algebra_map R S)) {v : ι → M} (li : linear_independent S v) :
linear_independent R v :=
begin
refine linear_independent_iff'.mpr (λ s g hg i hi, hinj (eq.trans _ (ring_hom.map_zero _).symm)),
refine (((@linear_independent_iff' _ _ _ v _ _ _).mp li) _ _ _) i hi,
simp_rw algebra_map_smul,
exact hg,
end
-- marginally shorter proof
lemma reduction_to_lattice (s : submodule ℚ V) (bv : is_basis ℚ v) :
∃ (n : ℕ) (vn : fin n → s.restrict_scalars ℤ ⊓ submodule.span ℤ (set.range v)),
is_basis ℤ vn :=
begin
obtain ⟨n, b, hb⟩ :=
submodule.exists_is_basis_of_le_span (_ : linear_independent ℤ v) inf_le_right,
{ refine ⟨n, b, ⟨_, by convert hb.2⟩⟩,
replace hb := hb.1,
rw [linear_independent_iff'] at ⊢ hb,
intros t g hg i hi,
refine hb t g _ i hi,
convert hg,
ext i,
erw [submodule.coe_smul_of_tower, submodule.coe_smul_of_tower, algebra_map_smul] },
{ refine algebra_map.injective.linear_independent _ bv.1,
exact λ a b ab, int.cast_inj.mp ab }
end
```

#### Damiano Testa (Apr 01 2021 at 04:29):

It may be that the main weirdness in the proof is that `is_scalar_tower ℤ ℚ V`

and the coercion from ℤ to ℚ do not recognize each other.... maybe.

#### Johan Commelin (Apr 01 2021 at 05:04):

I think that sometimes you can `have aux : int.module \Z = ring.to_module \Z`

(or something like that). The proof of that `have`

will be `subsingleton.elim`

. And after that, you can `rw aux`

so that all the scalar multiplications are now really the same.

#### Johan Commelin (Apr 01 2021 at 05:04):

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

#### Damiano Testa (Apr 01 2021 at 05:08):

Ok, analyzing this further, in the `erw`

step there are two `submodule.coe_smul_of_tower`

: the first one, changes

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

but the second one, changes

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

maybe this is the issue?

#### Yakov Pechersky (Apr 01 2021 at 05:11):

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

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

#### Damiano Testa (Apr 01 2021 at 05:12):

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

nor `ring.to_module`

!

#### Damiano Testa (Apr 01 2021 at 05:13):

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

#### Yakov Pechersky (Apr 01 2021 at 05:14):

Can you try `int_module`

and `semiring.to_semimodule`

instead?

#### Damiano Testa (Apr 01 2021 at 05:14):

with `int_module`

I still get `unknown identifier 'int_module'`

.

#### Damiano Testa (Apr 01 2021 at 05:15):

(however, lean recognized `semiring.to_semimodule`

)

#### Yakov Pechersky (Apr 01 2021 at 05:16):

`@add_comm_group.int_module \Z (by apply_instance)`

#### Damiano Testa (Apr 01 2021 at 05:18):

Lean considers this a valid statement:

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

#### Damiano Testa (Apr 01 2021 at 05:19):

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

Johan did say how to prove it:

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

#### Yakov Pechersky (Apr 01 2021 at 05:21):

When you get to your seemingly identical goal, `convert rfl`

should work now, hopefully with `convert`

pulling in this hypothesis. Or try `simp_rw aux`

as Johan suggested above.

#### Johan Commelin (Apr 01 2021 at 05:23):

In several files on polyhedral lattices, I disabled the `add_comm_group.int_module`

instance at the top of the file, forcing Lean (and myself) to work explicitly with $\Z$-modules.

#### Damiano Testa (Apr 01 2021 at 05:25):

I tried `simp_rw at *`

at each line in the proof, followed by `assumption`

, `solve_by_elim`

or `exact ...`

and it did not seem to work. I will try with `convert rfl`

now!

#### Damiano Testa (Apr 01 2021 at 05:27):

`convert rfl`

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

.

#### Damiano Testa (Apr 01 2021 at 05:30):

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

#### Yakov Pechersky (Apr 01 2021 at 05:34):

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

#### Yakov Pechersky (Apr 01 2021 at 05:46):

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

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

#### Damiano Testa (Apr 01 2021 at 05:48):

Sorry, having breakfast!

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

#### Yakov Pechersky (Apr 01 2021 at 06:37):

The issue isn't in the `int_module`

but rather `int.semiring`

vs

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

and related

#### Yakov Pechersky (Apr 01 2021 at 06:41):

Doing `local attribute [-instance] int.semiring int.ring int.comm_semiring`

results in the following diamond as an issue:

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

vs

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

#### Damiano Testa (Apr 01 2021 at 06:41):

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

#### Damiano Testa (Apr 01 2021 at 06:44):

So, should Lean be forbidden to use that `int`

is an integral domain?

#### Yakov Pechersky (Apr 01 2021 at 06:44):

Although in a mathlib repo I have, it seems

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

works fine

#### Damiano Testa (Apr 01 2021 at 06:46):

I copy pasted your `example`

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

#### Yakov Pechersky (Apr 01 2021 at 06:47):

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

#### Yakov Pechersky (Apr 01 2021 at 06:47):

Consider this tactic step:

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

#### Yakov Pechersky (Apr 01 2021 at 06:47):

Switching it to just

```
refine ⟨n, b, _⟩,
```

#### Yakov Pechersky (Apr 01 2021 at 06:47):

We can see a difference between the hypothesis `hb`

and the goal

#### Yakov Pechersky (Apr 01 2021 at 06:47):

#### Yakov Pechersky (Apr 01 2021 at 06:48):

#### Damiano Testa (Apr 01 2021 at 06:48):

I see: `ordered_ring`

vs `domain`

.

#### Yakov Pechersky (Apr 01 2021 at 06:49):

Right. So why is it unhappy? And, even though it is unhappy, is there a way to get the `exists_is_basis_of_le_span`

to use the "correct" `ring`

as a workaround?

#### Damiano Testa (Apr 01 2021 at 06:49):

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

- one to work with
`regular`

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

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

#### Yakov Pechersky (Apr 01 2021 at 06:50):

One issue with `exists_is_basis_of_le_span`

as it is right now is there is a free metavariable

#### Damiano Testa (Apr 01 2021 at 06:51):

So, are you suggesting that an `@`

and underscore-fest might solve this?

#### Yakov Pechersky (Apr 01 2021 at 06:51):

Specifically, which `submodule \Z V`

is on the left of the `\inf`

.

#### Yakov Pechersky (Apr 01 2021 at 06:51):

Could be? I'm not sure yet.

#### Damiano Testa (Apr 01 2021 at 06:53):

Let me try to work this out.

#### Damiano Testa (Apr 01 2021 at 06:54):

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

!)

#### Damiano Testa (Apr 01 2021 at 06:57):

I am tempted to say that it is this one:

```
submodule.restrict_scalars ℤ s
```

#### Yakov Pechersky (Apr 01 2021 at 06:58):

What about that submodule?

#### Damiano Testa (Apr 01 2021 at 06:58):

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

#### Yakov Pechersky (Apr 01 2021 at 06:59):

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

#### Damiano Testa (Apr 01 2021 at 07:01):

There is indeed a hidden goal, after the `obtain`

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

#### Yakov Pechersky (Apr 01 2021 at 07:02):

Yes, agreed. I am still not sure why the `integral_domain > domain > ring < comm_ring < integral_domain`

diamond seems to be getting in the way

#### Yakov Pechersky (Apr 01 2021 at 07:03):

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

#### Riccardo Brasca (Apr 01 2021 at 07:18):

I see that you are playing with more or less what I did yesterday (with a far better understanding :)

I don't know if this is relevant, but my first attempt to prove the proposition was to start like this (before realizing there is `submodule.exists_is_basis_of_le_span`

)

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

#### Damiano Testa (Apr 01 2021 at 07:19):

Actually, the proof feels like it could be simply:

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

#### Riccardo Brasca (Apr 01 2021 at 07:20):

So my idea was to prove that `Λ`

is free, the basis should of course be `w`

. Now, proving that `w`

is linear independent is easy... but I wasn't able to prove that it is a spanning set, and if you try you see immediately what goes wrong.

#### Damiano Testa (Apr 01 2021 at 07:21):

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

variable.

#### Yakov Pechersky (Apr 01 2021 at 07:23):

Ah there is another difference

#### Damiano Testa (Apr 01 2021 at 07:23):

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

#### Yakov Pechersky (Apr 01 2021 at 07:23):

Not sure if it is a meaningful one

#### Yakov Pechersky (Apr 01 2021 at 07:24):

`submodule.has_inf`

vs `semilattice_inf.to_has_inf (submodule ℤ V)`

#### Yakov Pechersky (Apr 01 2021 at 07:29):

Those are also `rfl`

=/

#### Damiano Testa (Apr 01 2021 at 07:31):

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

#### Sebastien Gouezel (Apr 01 2021 at 07:39):

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

#### Yakov Pechersky (Apr 01 2021 at 07:42):

```
import linear_algebra.free_module
lemma algebra_map.injective.linear_independent {R S M ι : Type*} [comm_semiring R] [semiring S]
[add_comm_monoid M] [algebra R S] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
(hinj : function.injective (algebra_map R S)) {v : ι → M} (li : linear_independent S v) :
linear_independent R v :=
begin
refine linear_independent_iff'.mpr (λ s g hg i hi, hinj (eq.trans _ (ring_hom.map_zero _).symm)),
refine (((@linear_independent_iff' _ _ _ v _ _ _).mp li) _ _ _) i hi,
simp_rw algebra_map_smul,
exact hg,
end
variables {V ι : Type*} [add_comm_group V] [semimodule ℚ V] [fintype ι] {v : ι → V}
(bv : is_basis ℚ v)
include bv
lemma reduction_to_lattice (s : submodule ℚ V) :
∃ (n : ℕ) (vn : fin n → s.restrict_scalars ℤ ⊓ submodule.span ℤ (set.range v)),
is_basis ℤ vn :=
begin
obtain ⟨n, b, hb⟩ := submodule.exists_is_basis_of_le_span
((by { refine algebra_map.injective.linear_independent _ bv.1, exact λ a b ab, int.cast_inj.mp ab }))
(@inf_le_right _ _ (submodule.restrict_scalars ℤ s) _),
refine ⟨n, b, _⟩,
exact hb -- :C
end
```

#### Damiano Testa (Apr 01 2021 at 07:43):

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

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

#### Sebastien Gouezel (Apr 01 2021 at 07:45):

Thanks!

#### Sebastien Gouezel (Apr 01 2021 at 07:49):

First comment: it's probably coming from `add_comm_group.int_module`

, which is not defeq to other int actions. Indeed, if you disable it with

```
local attribute [-instance] add_comm_group.int_module
```

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

#### Sebastien Gouezel (Apr 01 2021 at 08:24):

Here is a working proof:

```
import linear_algebra.free_module
local attribute [-instance] add_comm_group.int_module
lemma algebra_map.injective.linear_independent {R S M ι : Type*} [comm_semiring R] [semiring S]
[add_comm_monoid M] [algebra R S] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
(hinj : function.injective (algebra_map R S)) {v : ι → M} (li : linear_independent S v) :
linear_independent R v :=
begin
refine linear_independent_iff'.mpr (λ s g hg i hi, hinj (eq.trans _ (ring_hom.map_zero _).symm)),
refine (((@linear_independent_iff' _ _ _ v _ _ _).mp li) _ _ _) i hi,
simp_rw algebra_map_smul,
exact hg,
end
variables {V ι : Type*} [add_comm_group V] [semimodule ℚ V] [semimodule ℤ V]
[is_scalar_tower ℤ ℚ V] [fintype ι] {v : ι → V}
(bv : is_basis ℚ v)
include bv
set_option profiler true
lemma reduction_to_lattice (s : submodule ℚ V) :
∃ (n : ℕ) (vn : fin n → s.restrict_scalars ℤ ⊓ submodule.span ℤ (set.range v)),
is_basis ℤ vn :=
begin
have A : function.injective (algebra_map ℤ ℚ) := λ a b ab, int.cast_inj.mp ab,
have B := algebra_map.injective.linear_independent A bv.1,
obtain ⟨n, b, hb⟩ :=
submodule.exists_is_basis_of_le_span B (@inf_le_right _ _ (submodule.restrict_scalars ℤ s) _),
refine ⟨n, b, _⟩,
convert hb,
end
```

I disabled `add_comm_group.int_module`

, and instead assumed ```
[semimodule ℤ V]
[is_scalar_tower ℤ ℚ V]
```

to make sure that we did not use the bad int module structure, and instead used a generic one.

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

#### Damiano Testa (Apr 01 2021 at 08:27):

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

While we are at it, I wanted your `A`

statement to be already in mathlib, but I could not find it: is it hiding in there somewhere?

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

#### Sebastien Gouezel (Apr 01 2021 at 08:37):

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

#### Kevin Buzzard (Apr 01 2021 at 08:44):

Even `convert hb using 1`

takes time (essentially the same amount of time as far as I can see).

#### Sebastien Gouezel (Apr 01 2021 at 08:55):

Minimal diamond:

```
import linear_algebra.free_module
lemma foo : algebra.id ℤ = algebra_int ℤ := rfl -- fails
```

both instances are registered in mathlib.

#### Yakov Pechersky (Apr 01 2021 at 08:56):

I tried turning `-instance algebra_int`

off but that hadn't helped in my experiments.

#### Johan Commelin (Apr 01 2021 at 09:03):

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

#### Sebastien Gouezel (Apr 01 2021 at 09:03):

The thing is that these instances are used in other files when defining various objects, so it is already too late. Maybe changing `algebra.id`

to something nicer would help (expanding the fields instead of relying on an abstract construction).

#### Sebastien Gouezel (Apr 01 2021 at 17:47):

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

As @Eric Wieser has pointed out several times, we are exactly in this situation here. For instance, if `E`

and `F`

are two `add_comm_group`

, then they are both `ℤ`

-modules, and then you get two non-defeq `ℤ`

module instances on `E x F`

, the one coming from the `add_comm_group`

instance and the one coming from the module product instance. And there is no way to make these defeq.

A solution is to *not* register `add_comm_group.nat_semimodule`

as a global instance, and only use it when needed in proofs, and use suitable typeclass assumptions in statements. (Or register it as a global instance, but only once we are sure that it's not used in statements, and only to make it available for proofs -- this could probably be enforced by a linter). I had a go at refactoring mathlib along these lines, to see how things go. The good news is that, with this refactor, the above problem in this thread completely disappears, i.e., no need for `convert`

or whatever. And a few proofs that were painful because of instance mismatch become smoother. The bad news is that I'm not done fixing it, because there are many places where the previous instance is used. My work in progress is in the branch branch#gsmul_instance, if anyone wants to have a look/fix a few proofs.

#### Johan Commelin (Apr 01 2021 at 18:06):

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

#### Johan Commelin (Apr 01 2021 at 18:06):

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

#### Damiano Testa (Apr 01 2021 at 18:09):

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

#### Eric Wieser (Apr 01 2021 at 18:38):

Another option would be to use `gsmul`

and `nsmul`

in lemma statements, and convert to smul and back inside the lemma

#### Sebastien Gouezel (Apr 01 2021 at 18:41):

The problem with `gsmul`

and `nsmul`

is that all the linear algebra lemmas do not apply (for instance, when you want to use the fact that a linear map satisfies `f (c • v) = c • f v`

, this won't work out of the box for `gsmul`

). So they are really a pain to use together with linear algebra.

#### Johan Commelin (Apr 01 2021 at 19:04):

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

#### Johan Commelin (Apr 01 2021 at 19:05):

And one of my reasons is extremely mundane: the notation for scalar multiplication is just nicer than `gsmul/nsmul`

. And at the same time the notation for group homs looks better than that for linear maps (especially if you are just working with `Z`

-modules anyway).

#### Riccardo Brasca (Apr 01 2021 at 20:41):

I've uploaded here

https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/toric/towards_Gordan.lean

a proof of `pre_generators_finite`

. I am little tired to golf it, but as usual if someone wants to play with it no problem.

The idea of the proof is very simple: the function `i`

takes a pre_generator `g`

and sends it to the set `t`

of the definition. Since `t ⊆ s`

and `s`

is finite, it is enough to prove that `i`

is injective. The mathematical proof is between the lines `197`

and `218`

. The rest of the proof is me fighting against `classical.some`

and the fact that to use `fintype.of_injective`

the codomain of `i`

must be `set s`

, but morally the "true" codomain, where it's easier to work, is `set M`

.

#### Riccardo Brasca (Apr 01 2021 at 20:43):

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

#### Kevin Buzzard (Apr 01 2021 at 21:29):

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

#### Yakov Pechersky (Apr 01 2021 at 22:04):

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

#### Yakov Pechersky (Apr 01 2021 at 22:05):

Because you get noncomputable fintype from set.finite anyway

#### Yakov Pechersky (Apr 01 2021 at 22:05):

And then you don't have to juggle sort coercions

#### Riccardo Brasca (Apr 01 2021 at 22:11):

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

#### Johan Commelin (Apr 02 2021 at 04:35):

Yakov Pechersky said:

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

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

#### Damiano Testa (Apr 02 2021 at 05:23):

I have not finished writing a full proof, so the stuff in `towards_Gordan`

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

Some of these statements might have to be changed anyways, since I decided to go for a full `sorry`

-explosion, rather than figuring out what the best way of doing things is step-by-step.

#### Damiano Testa (Apr 02 2021 at 05:24):

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

#### Damiano Testa (Apr 02 2021 at 06:02):

Also, the reason I used `fintype`

is because I read somewhere that `fintype`

s were easier than `finset`

s. If `set.finite`

is even easier, then I would probably change finiteness assumptions everywhere to `set.finite`

!

#### Yakov Pechersky (Apr 02 2021 at 06:11):

My understanding is that the power of `finset`

and `fintype`

is their computability. If you're going to already mark it as `noncomputable`

, then you can make your statements be about `set.finite`

because of docs#set.finite.fintype, which will give you a noncomputable fintype anyway

#### Yakov Pechersky (Apr 02 2021 at 06:12):

Because `set.finite s`

is just `nonempty (fintype s)`

#### Damiano Testa (Apr 02 2021 at 06:18):

Ok, from `nonempty (fintype s)`

I would deduce that `s`

is going to be `non-empty`

? I am not sure if I like this: I am usually careful about including the empty set in my statements, excluding it only when the statement is false for the empty set. The possibility of having an empty set is often simplifying for proofs.

#### Damiano Testa (Apr 02 2021 at 06:19):

Ah, maybe the `nonempty`

is simply the assertion that there is a `fintype`

structure on `s`

, possibly with `s`

being the empty `finset`

?

#### Yakov Pechersky (Apr 02 2021 at 06:24):

You don't have to unfold what `set.finite`

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

#### Damiano Testa (Apr 02 2021 at 06:33):

Ok, I will try to replace `fintype`

with `set.finite`

!

#### Damiano Testa (Apr 02 2021 at 06:38):

So, the expectation is that this statement

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

should be easier than

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

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

.)

#### Yakov Pechersky (Apr 02 2021 at 06:39):

Yeah, possibly

#### Damiano Testa (Apr 02 2021 at 06:40):

Ok, I pushed the change.

Thanks!

#### Damiano Testa (Apr 02 2021 at 06:40):

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

#### Yakov Pechersky (Apr 02 2021 at 06:40):

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

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

#### Damiano Testa (Apr 02 2021 at 06:41):

Ah, I used

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

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

#### Damiano Testa (Apr 02 2021 at 06:42):

(There is an `include bv`

in the file that I am using.)

#### Yakov Pechersky (Apr 02 2021 at 06:42):

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

#### Damiano Testa (Apr 02 2021 at 06:43):

(However, I suspect that `bv`

plays no role in the proof.)

#### Yakov Pechersky (Apr 02 2021 at 06:43):

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

#### Damiano Testa (Apr 02 2021 at 06:44):

In my version, the `simp_rw submodule.ext'_iff`

does not work:

#### Yakov Pechersky (Apr 02 2021 at 06:45):

Then you can use things like

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

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

#### Damiano Testa (Apr 02 2021 at 06:45):

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

#### Yakov Pechersky (Apr 02 2021 at 06:45):

which branch are you on?

#### Damiano Testa (Apr 02 2021 at 06:46):

I am on `toric`

, the one that I just pushed.

#### Damiano Testa (Apr 02 2021 at 06:51):

Ok, looking at the proof that Riccardo wrote, I think that it should make use of `is_cyclic`

. This probably means that I should change the definition of pre_generators. This will probably make the coercion to type of a set simpler, by going via a subtype instead.

#### Damiano Testa (Apr 02 2021 at 06:52):

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

#### Damiano Testa (Apr 02 2021 at 06:53):

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

#### Yakov Pechersky (Apr 02 2021 at 06:57):

The `ext'_iff`

lemma is now a part of `set_like`

after a refactor

#### Yakov Pechersky (Apr 02 2021 at 06:59):

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

#### Riccardo Brasca (Apr 02 2021 at 07:58):

@Damiano Testa If you happy with `set.finite`

I can do it.

#### Riccardo Brasca (Apr 02 2021 at 07:59):

BTW I use `bv`

to prove that `M`

is torsion free.

#### Damiano Testa (Apr 02 2021 at 09:07):

I think that the version that I pushed to `toric`

has `set.finite`

and also your proof of the reduction to Z.

I need to think about `bv`

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

#### Riccardo Brasca (Apr 02 2021 at 09:22):

My mathematical proof is the following: I have to prove that a pre_generator `g`

is determined by the subset `t`

of the definition. If `g₁`

and `g₂`

are associated to the same subset, then `submodule.span ℕ {g₁} = submodule.span ℕ {g₂}`

, by definition. So there are `a b : ℕ`

such that `g₁ = a • g₂`

and `g₂ = b • g₁`

so `g₁ = a • b • g₁ = (a * b) • g₁`

. Now I want `a * b = 1`

(or `g₁ = 0`

), and here is where I used torsion freeness.

#### Riccardo Brasca (Apr 02 2021 at 10:43):

I pushed to `toric`

the new proof of `pre_generators_finite`

. It is indeed better then before. For some reason I am not able to define `i`

using `if`

`then`

`else`

and so I did it in tactic mode.

#### Sebastien Gouezel (Apr 02 2021 at 14:18):

Sebastien Gouezel said:

A solution is to

notregister`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 (Apr 02 2021 at 15:04):

Never mind, problem solved :-)

#### Johan Commelin (Apr 02 2021 at 18:46):

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

#### Johan Commelin (Apr 02 2021 at 18:46):

I feel somewhat responsible for maintaining Witt vectors (-;

#### Damiano Testa (Apr 02 2021 at 19:57):

Riccardo, this is also more or less what I had in mind and it is certain sufficient for the application to Gordan's lemma. You could probably get away without `bv`

, observing that a cyclic `nat`

module has finitely many generators (1, if it is infinite and $\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 (Apr 02 2021 at 19:57):

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

#### Johan Commelin (Apr 03 2021 at 05:44):

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

#### Johan Commelin (Apr 03 2021 at 05:44):

You need an extra `intro`

to take care of the `algebra`

instance.

#### Johan Commelin (Apr 03 2021 at 06:01):

I've pushed a bunch of fixes. We need to add an instance `algebra int (zmod n)`

. I haven't done that yet, but it should fix the remaining problems (I hope!)

#### Johan Commelin (Apr 03 2021 at 06:08):

Pushed that instance for `zmod`

, let's see what CI thinks of it.

#### Kevin Buzzard (Apr 10 2021 at 15:58):

OK I am trying to get on top of this Gordan's Lemma thing. As far as I can see, in `master`

we have a file `toric/lem97.lean`

which contains a complete proof of Lemma 9.7 of `analytic.pdf`

modulo

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

Here $\Lambda$ is a finite free $\Z$-module, and`explicit_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 (Apr 10 2021 at 16:06):

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

#### Kevin Buzzard (Apr 10 2021 at 16:44):

I'm not entirely sure I understand the Wikipedia proof right now. Is it using some result of the form "double dual of a fg cone (:= `nnreal`

-submodule) in a real vector space is itself? Or maybe "dual of an fg cone is fg"? Are these things obvious?

#### Damiano Testa (Apr 10 2021 at 16:45):

Dear Kevin,

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

I have been making PRs to mathlib as I was going along, to move the more "stable" part. For this reason, the stuff left in `toric`

is less coherent. I have started making the file `towards_Gordan`

with the idea of making it a path towards a proof of Gordan's lemma, but I feel that it became "public" a little too early.

I have had conversations with Johan about the "glue" and he also agreed that what will come out of the `toric`

branch should be easily converted to what is the explicit Gordan statement. I was trying to prepare the `towards_Gordan`

file to a level that was usable to someone who did not know the proof of Gordan's lemma, but, given Kevin's unsuccessful effort, I am not done doing it!

#### Damiano Testa (Apr 10 2021 at 16:46):

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

#### Damiano Testa (Apr 10 2021 at 16:47):

This is an outline:

#### Kevin Buzzard (Apr 10 2021 at 16:54):

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

#### Damiano Testa (Apr 10 2021 at 16:54):

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

#### Damiano Testa (Apr 10 2021 at 16:56):

In the Lean formalization is what I would have called `pointed`

, except that you noticed that the definition was not correct. Luckily, I had not started using this. The good thing about "octants" (or `nat`

-submodules of octants), is that they have finitely many extremal rays. (Which I am now going to define.)

#### Damiano Testa (Apr 10 2021 at 16:56):

An extremal ray is a one-dimensional subcone of a cone with the property that is `c d`

are in the cone and `c + d`

is in the extremal ray, then `c`

and `d`

are actually already in the extremal ray.

#### Damiano Testa (Apr 10 2021 at 16:58):

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

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

#### Damiano Testa (Apr 10 2021 at 16:59):

Finite generation of extremal rays follows from the fact that extremal rays are correspond to what is called, I think, pre_generators in `toric`

(the relationship between extremal rays and pre_generators needs to be proven).

#### Damiano Testa (Apr 10 2021 at 16:59):

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

#### Damiano Testa (Apr 10 2021 at 17:01):

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

#### Damiano Testa (Apr 10 2021 at 17:02):

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

#### Kevin Buzzard (Apr 10 2021 at 17:13):

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

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

You say that `pointed`

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

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

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

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

#### Kevin Buzzard (Apr 10 2021 at 17:14):

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

#### Damiano Testa (Apr 10 2021 at 17:15):

Ok, the reason I was being a little sloppy is that we definitely need to have these notions interacting nicely with `nat`

- `int`

- `rat`

- and (to a *much* lesser extent) `real`

.

#### Damiano Testa (Apr 10 2021 at 17:15):

Let me answer more in detail your questions.

#### Damiano Testa (Apr 10 2021 at 17:17):

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

is a cone inside any octant and is therefore pointed.

#### Damiano Testa (Apr 10 2021 at 17:18):

The Lean formalization of `pointed`

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

#### Damiano Testa (Apr 10 2021 at 17:19):

There are three main "coefficient" types: `N`

, `Z`

, `Q`

. I will let you guess what they are in the standard application.

#### Damiano Testa (Apr 10 2021 at 17:19):

The only tricky one is that, at one point, we will want to allow `Q`

to be the reals, but for the most part (and, really, even in the last step) we can always get away with the rationals.

#### Damiano Testa (Apr 10 2021 at 17:22):

The three types `N`

, `Z`

and `Q`

are ordered semirings, they form a `scalar_tower`

of `algebra`

s, 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 (Apr 10 2021 at 17:22):

Cones, refers to a `submodule.span N s`

, where `s`

is a subset of a `Q`

-module.

#### Damiano Testa (Apr 10 2021 at 17:25):

Extremal rays are one-dimensional subcones of a `pointed`

cone (not really sure whether we want the definition to also apply to non-pointed stuff). Thus, we reduce from a general cone (which could be the `nat`

-span of `1, -1`

inside `rat`

, i.e. *not* a `pointed`

cone), to a `pointed`

cone, by "splitting in halfs and combining".

#### Damiano Testa (Apr 10 2021 at 17:26):

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

#### Damiano Testa (Apr 10 2021 at 17:26):

This is via the `dual_set`

process.

#### Damiano Testa (Apr 10 2021 at 17:28):

For duals, the setup is that there are two `Q`

-modules `M`

and `N`

and a bilinear `pairing`

, typically denoted by `f`

, mapping $M \times N \to Q$.

#### Damiano Testa (Apr 10 2021 at 17:31):

A `dual_set`

is "essentially" a cone: given a subset `s`

of `M`

, the corresponding `dual_set`

is the set of all elements of `N`

that have non-negative pairing with `s`

.

#### Damiano Testa (Apr 10 2021 at 17:32):

A `dual_set`

is automatically an `N`

-submodule and it is also automatically saturated.

#### Damiano Testa (Apr 10 2021 at 17:32):

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

#### Damiano Testa (Apr 10 2021 at 17:40):

(I noticed now the clash in notation `N`

refers to the natural numbers look-alike as well as the `Q`

-module: I will try to use latex font $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 (Apr 10 2021 at 17:41):

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

#### Damiano Testa (Apr 10 2021 at 17:44):

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

Also, cones are `N`

-spans of stuff: they might be `Z`

-spans, for instance if you use a $\pm$-symmetric generating set, but they need not be.

#### Damiano Testa (Apr 10 2021 at 17:44):

Cones need not be saturated, but the ones that arise from `dual_set`

automatically are.

#### Damiano Testa (Apr 10 2021 at 17:45):

Also, cones with finitely many extremal rays *need not* be finitely generated: this is why the fact that the ones arising as `dual_set`

are *automatically saturated* is important.

#### Damiano Testa (Apr 10 2021 at 17:47):

Finally, a comment about the reals: the whole proof can take place with rational coefficients. The only "real" input is in proving that the set of integral vectors inside the span of finitely many vectors with coefficients in `[0, 1]`

is finite. The "easy" way is to use real coefficients, the set of linear combinations is compact, the set of integer vectors is discrete, hence the intersection is finite.

#### Damiano Testa (Apr 10 2021 at 17:48):

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

#### Damiano Testa (Apr 10 2021 at 17:53):

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

In the "maths world" we should prove that the elements of the `dual_set`

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

#### Damiano Testa (Apr 10 2021 at 17:59):

An example to keep in mind is the cone generated by `(1,0), (1,2)`

. The background basis is the standard one `(1,0), (0,1)`

: integral refers to integral linear combinations of these last two elements.

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

.

The non-negative rational linear combinations of the vectors `(1,0), (1,2)`

contain the integer vector `(1,1)`

. However, all natural (or even integer) linear combinations of `(1,0), (1,2)`

have *even* second coordinate and will therefore not equal `(1,1)`

: there is a hole.

However, `2(1, 1) = (1,0) + (1,2)`

*is* a non-negative integral combination of `(1,0), (1,2)`

. We need to saturate. In this case, it is enough to simply add this vector, to the set of generators of the extremal rays.

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

#### Filippo A. E. Nuccio (Apr 10 2021 at 18:04):

I have not really been working on anything related to Gordan's lemma, only the use of it to derive `Lemma 9.7`

. I see Damiano jumped in, and he certainly has more to say.

#### Filippo A. E. Nuccio (Apr 10 2021 at 18:05):

(deleted)

#### Kevin Buzzard (Apr 10 2021 at 22:00):

I still don't see the proof we're trying to formalise. You say "we should prove that the elements of $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 (Apr 10 2021 at 22:03):

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

#### Kevin Buzzard (Apr 10 2021 at 22:04):

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

#### Kevin Buzzard (Apr 10 2021 at 22:07):

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

#### Damiano Testa (Apr 11 2021 at 04:56):

Dear Kevin,

I am really sorry: I realise that I made the folder `toric`

available too soon. I did not formalise all the statements that I mentioned above: they have to be formalised, of course, but I have not done it yet.

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

:

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

#### Damiano Testa (Apr 11 2021 at 05:02):

This lemma, or a provable version of it, gives the conversion between `extremal_rays`

and `dual_set_rays`

.

I should also at least state that a cone is the span of its `extremal_rays`

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

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

#### Johan Commelin (Apr 11 2021 at 10:17):

Note that I pushed Damiano a bit to merge `toric`

into master. I think it makes it more visible. I'm sorry for the confusion it created.

#### Damiano Testa (Apr 11 2021 at 10:30):

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

#### Kevin Buzzard (Apr 11 2021 at 10:42):

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

#### Kevin Buzzard (Apr 11 2021 at 10:43):

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

#### Damiano Testa (Apr 11 2021 at 16:26):

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

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

#### Damiano Testa (Apr 11 2021 at 16:27):

You can find the "algebraic blueprint" in the `toric`

branch, in `src/toric/gordan_algebraic_blueprint.tex`

.

#### Damiano Testa (Apr 11 2021 at 16:27):

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

I also pushed a version with the pdf file.

#### Riccardo Brasca (Apr 11 2021 at 19:30):

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

#### Damiano Testa (Apr 12 2021 at 04:35):

I pushed a newer version of the `algebraic`

blueprint to the `toric`

branch. There are no substantial changes, I simply tried to streamline the proof a little bit, and, hopefully, clarified it!

#### Damiano Testa (Apr 12 2021 at 04:36):

Comments are welcome!

#### Riccardo Brasca (Apr 12 2021 at 14:38):

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 (Apr 12 2021 at 15:04):

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 (Apr 12 2021 at 15:09):

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

#### Adam Topaz (Apr 12 2021 at 15:12):

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

#### Johan Commelin (Apr 12 2021 at 15:13):

Nope, not yet, unfortunately :sad:

#### Kevin Buzzard (Apr 12 2021 at 15:13):

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

#### Adam Topaz (Apr 12 2021 at 15:14):

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

#### Kevin Buzzard (Apr 12 2021 at 15:14):

I think Patrick finished this recently.

#### Riccardo Brasca (Apr 12 2021 at 15:18):

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

#### Adam Topaz (Apr 12 2021 at 15:19):

Nice!

#### Adam Topaz (Apr 12 2021 at 15:24):

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

is free.

#### Adam Topaz (Apr 12 2021 at 15:37):

(note that `submodule.exists_is_basis`

is true even without the finite rank assumption)

#### Riccardo Brasca (Apr 12 2021 at 15:44):

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

#### Patrick Massot (Apr 12 2021 at 16:44):

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

#### Patrick Massot (Apr 12 2021 at 16:45):

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

#### Damiano Testa (Apr 12 2021 at 17:45):

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

#### Damiano Testa (Apr 12 2021 at 17:46):

Patrick, I do not think that this is urgent. There is some more stuff that needs doing that does not depend on this, and we can always merge your unmerged branches into `lean-liquid`

. It will probably be easy to adapt, should there be changes in the statements.

#### Riccardo Brasca (Apr 12 2021 at 17:49):

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

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

#### Damiano Testa (Apr 12 2021 at 17:52):

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

#### Damiano Testa (Apr 12 2021 at 17:54):

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

#### Damiano Testa (Apr 12 2021 at 17:55):

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

#### Riccardo Brasca (Apr 12 2021 at 17:55):

We already have `monoid_algebra`

with an API

#### Damiano Testa (Apr 12 2021 at 17:56):

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 (Apr 12 2021 at 17:58):

Ok, `monoid_algebra`

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

#### Damiano Testa (Apr 12 2021 at 17:58):

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

#### Riccardo Brasca (Apr 12 2021 at 18:01):

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 (Apr 12 2021 at 18:02):

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

#### Kevin Buzzard (Apr 12 2021 at 18:07):

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

.

#### Kevin Buzzard (Apr 12 2021 at 18:09):

I need to worry about other things today and tomorrow, but on Wednesday I will get back to this, and in my mind what we need to do with this proof is to pull out more sublemmas, because I think the main argument is too long to be formalised painlessly in Lean -- we will get to that stage where it takes 10 seconds to write every line and this is no fun at all. Right now the two things I can see that we can pull off are Theorem 2, which is already pulled off, and the statement that if $\Lambda$ is a finite free $\Z$-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 (Apr 12 2021 at 18:12):

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

#### Kevin Buzzard (Apr 12 2021 at 18:12):

Even using this last result in the main proof will be delicate, because the kernel of $\phi$ is a submodule, which we then promote to a module $\Lambda'$, and we will have to move $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 (Apr 12 2021 at 18:13):

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

#### Kevin Buzzard (Apr 12 2021 at 18:18):

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 (Apr 12 2021 at 18:23):

This top-down approach now gives us a whole bunch of sorries (and already what I have said above might expand out into quite a long proof as well). Now we have to decide how to fill in those sorries, and the idea is to try and fill them in with new lemmas rather than solving these goals within this proof we've just written. Then one has to think about precisely the statement of the formalisation of the missing pieces, but because we have this top-down sorried proof, one can take one of the missing pieces (for example some statement that for a Z-graded Noetherian ring, $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 (Apr 12 2021 at 18:26):

So in fact Riccardo, one answer to your "theorem 2 is needed, exactly as it is in the blueprint" would be this: the blueprint states a mathematical theorem, not a formal Lean theorem. It might be best to start with the big prize, namely the precise sorried statement in the `lem97`

file, and work down from there. You might find for example that ultimately we do not want a statement about `monoid_algebra R M`

, but a statement about a ring which is canonically isomorphic to `monoid_algebra R M`

. If you've gone ahead and formalised Theorem 2 but just for the "concrete" model of `monoid_algebra R M`

in mathlib then you might find that your lemma will not "fill in the hole" that we need it to fill in. So I think that before anything is formalised, now we think we have a mathematical proof, it might be worth starting on the top-down approach.

#### Adam Topaz (Apr 12 2021 at 18:27):

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

#### Kevin Buzzard (Apr 12 2021 at 18:27):

It's in a pdf on the toric branch

#### Adam Topaz (Apr 12 2021 at 18:27):

Ah ok

#### Adam Topaz (Apr 12 2021 at 18:27):

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

#### Kevin Buzzard (Apr 12 2021 at 18:27):

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

.

#### Kevin Buzzard (Apr 12 2021 at 18:28):

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

#### Kevin Buzzard (Apr 12 2021 at 18:28):

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

#### Riccardo Brasca (Apr 12 2021 at 18:32):

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 (Apr 12 2021 at 18:32):

Yeah I'm looking at it now...

#### Adam Topaz (Apr 12 2021 at 18:32):

Oh this should totally be doable with current mathlib

#### Riccardo Brasca (Apr 12 2021 at 18:33):

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

#### Kevin Buzzard (Apr 12 2021 at 18:44):

Yes I'm sure it's doable, but the big question is precisely how to formalise it. This is why I am suggesting that now we think we have a maths proof which should be possible to formalise reasonably (although I have not checked Damiano's argument about $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 (Apr 12 2021 at 18:48):

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

#### Damiano Testa (Apr 12 2021 at 18:49):

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

#### Damiano Testa (Apr 12 2021 at 18:49):

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

#### Adam Topaz (Apr 12 2021 at 19:18):

We recently got docs#is_free_group

#### Adam Topaz (Apr 12 2021 at 19:18):

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

#### Adam Topaz (Apr 12 2021 at 19:19):

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

#### Riccardo Brasca (Apr 13 2021 at 09:54):

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

```
import algebra.monoid_algebra
import ring_theory.finiteness
variables {R : Type*} [comm_ring R] [nontrivial R]
variables {M : Type*} [add_comm_monoid M]
open algebra submodule
lemma monoid_alg_ft_iff : finite_type R (add_monoid_algebra R M) ↔ (⊤ : submodule ℕ M).fg :=
begin
sorry
end
```

Does someone see a way to use ` [comm_monoid M]`

instead of ` [add_comm_monoid M]`

? It seems much more natural to me, but then I don't know how to say `(⊤ : submodule ℕ M).fg `

, since a multiplicative monoid is not a `ℕ`

-semimodule, and all the theory of finitely generated stuff in mathlib is for subsemimodules.

#### Riccardo Brasca (Apr 13 2021 at 09:57):

Hmm, I can use `additive M`

but maybe this will introduce other problems in the proof.

#### Johan Commelin (Apr 13 2021 at 10:05):

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

#### Johan Commelin (Apr 13 2021 at 10:05):

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

#### Riccardo Brasca (Apr 13 2021 at 10:10):

No thanks :sweat_smile:

#### Riccardo Brasca (Apr 13 2021 at 12:37):

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

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

#### Johan Commelin (Apr 13 2021 at 12:40):

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

on the fly.

#### Kevin Buzzard (Apr 13 2021 at 13:04):

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

#### Damiano Testa (Apr 13 2021 at 13:51):

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

#### Kevin Buzzard (Apr 13 2021 at 14:05):

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

#### Johan Commelin (Apr 13 2021 at 14:06):

I think @Eric Wieser has/had some PRs on gradings on `direct_sum _`

. But we don't have general gradings on general rings, afaik

#### Damiano Testa (Apr 13 2021 at 14:07):

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

#### Eric Wieser (Apr 13 2021 at 14:08):

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

#### Kevin Buzzard (Apr 13 2021 at 14:08):

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

#### Damiano Testa (Apr 13 2021 at 14:09):

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

#### Damiano Testa (Apr 13 2021 at 14:10):

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

#### Eric Wieser (Apr 13 2021 at 14:12):

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

#### Eric Wieser (Apr 13 2021 at 14:18):

What we're missing is something like the statement

`A : ι → monoid R`

is a gradation of a ring`R`

if`complete_lattice.independent (set.range A)`

and there is a ring_equiv from`R`

to`⨁ i, A i`

whose inverse is roughly`direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i)`

#### Damiano Testa (Apr 13 2021 at 14:23):

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

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

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

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

If it is not already in mathlib, it would also be good to extract a lemma that says that if a ring is generated by some set `s`

and some other set `t`

generates the generators, then `t`

also generates.

#### Kevin Buzzard (Apr 13 2021 at 14:33):

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

```
import ring_theory.subring
import data.finsupp
open_locale big_operators
structure grading (M : Type*) [comm_monoid M] (R : Type*) [comm_ring R] :=
(graded_piece : M → set R)
(independent : ∀ f : M →₀ R, (∀ m : M, f m ∈ graded_piece m) →
f.sum (λ m r, r) = 0 → f = 0)
(span : ∀ r : R, ∃ f : M →₀ R, (∀ m : M, f m ∈ graded_piece m) ∧ f.sum (λ m r, r) = r)
```

and also a variant for `add_comm_monoid`

(in fact in our application we only need `add_comm_monoid`

). Do we have anything like this? We don't need to build the ring we have it already, we want to impose the grading a posteriori.

#### Damiano Testa (Apr 13 2021 at 14:35):

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

#### Eric Wieser (Apr 13 2021 at 14:35):

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

#### Kevin Buzzard (Apr 13 2021 at 14:36):

hmm :-)

#### Kevin Buzzard (Apr 13 2021 at 14:39):

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

?

#### Eric Wieser (Apr 13 2021 at 14:40):

My attempt at my quoted description above is:

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

#### Kevin Buzzard (Apr 13 2021 at 14:41):

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

#### Kevin Buzzard (Apr 13 2021 at 14:42):

re syntax error: just end with `:= sorry`

#### Eric Wieser (Apr 13 2021 at 14:42):

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

#### Damiano Testa (Apr 13 2021 at 14:42):

... unless of course, the grading does not respect multiplication by `-1`

, if it can! :upside_down:

#### Kevin Buzzard (Apr 13 2021 at 14:44):

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

#### Eric Wieser (Apr 13 2021 at 14:46):

Kevin, is your `independent`

equivalent to docs#complete_lattice.indepedent?

#### Damiano Testa (Apr 13 2021 at 14:46):

Ah, I see that now the graded pieces are `add_subgroup`

s: I had missed that!

#### Damiano Testa (Apr 13 2021 at 14:47):

so, yes, of course, the piece that contains `1`

also contains `-1`

!

#### Kevin Buzzard (Apr 13 2021 at 14:48):

Eric Wieser said:

Kevin, is your

`independent`

equivalent to docs#complete_lattice.independent?

Yes.

#### Eric Wieser (Apr 13 2021 at 14:49):

... and is that easy to prove?

#### Kevin Buzzard (Apr 13 2021 at 14:49):

Oh -- at least in the add_subgroup case.

#### Kevin Buzzard (Apr 13 2021 at 14:50):

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

#### Damiano Testa (Apr 13 2021 at 14:50):

Actually, does it automatically follow that `1`

is homogeneous? In my mind, I always think that the elements of degree `0`

form a subring: they are clearly a subgroup that is closed under multiplication, but do they have a `1`

? Is the one of this piece the same as the `1`

of the whole ring?

#### Eric Wieser (Apr 13 2021 at 14:51):

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

is additively graded

#### Damiano Testa (Apr 13 2021 at 14:51):

for safe measure, should we add the axiom that the degree `0`

piece is a subring?

#### Kevin Buzzard (Apr 13 2021 at 14:53):

I only care about the case of an `add_comm_monoid`

grading, I went with `comm_monoid`

believing that I could perhaps use `to_additive`

to generate the API for the `add_comm_monoid`

variant (I'm assuming it ignores rings)

#### Eric Wieser (Apr 13 2021 at 14:53):

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

#### Kevin Buzzard (Apr 13 2021 at 14:54):

I guess it won't touch the rings but it could well touch the `add_subgroup R`

's :-/

#### Eric Wieser (Apr 13 2021 at 14:56):

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

```
import algebra.direct_sum_graded
open_locale direct_sum
-- modified for additive grading, and a `one` axiom
structure add_grading (M : Type*) [add_comm_monoid M] (R : Type*) [comm_ring R] :=
(graded_piece : M → add_subgroup R)
(grading_one : (1 : R) ∈ graded_piece 0)
(grading_mul : ∀ (m n : M) (r s : R),
r ∈ graded_piece m → s ∈ graded_piece n → r * s ∈ graded_piece (m + n))
(independent : ∀ f : M →₀ R, (∀ m : M, f m ∈ graded_piece m) →
f.sum (λ m r, r) = 0 → f = 0)
(span : ∀ r : R, ∃ f : M →₀ R, (∀ m : M, f m ∈ graded_piece m) ∧ f.sum (λ m r, r) = r)
variables (M : Type*) [add_comm_monoid M] (R : Type*) [comm_ring R]
instance : has_coe_to_sort (add_grading M R) := ⟨_, λ g, ⨁ i, g.graded_piece i⟩
instance grading.gmonoid [decidable_eq M] (g : add_grading M R) : direct_sum.gmonoid (λ i, g.graded_piece i) :=
direct_sum.gmonoid.of_add_subgroups (λ i, g.graded_piece i) g.grading_one g.grading_mul
```

#### Kevin Buzzard (Apr 13 2021 at 14:56):

The reason my `independent`

is the same as `complete_lattice.independent`

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

#### Eric Wieser (Apr 13 2021 at 14:57):

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

#### Eric Wieser (Apr 13 2021 at 14:59):

Damiano Testa said:

for safe measure, should we add the axiom that the degree

`0`

piece is a subring?

This is proven by #6851 using the existing axioms

#### Kevin Buzzard (Apr 13 2021 at 15:00):

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

#### Eric Wieser (Apr 13 2021 at 15:01):

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

#### Eric Wieser (Apr 13 2021 at 15:06):

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

constructively as

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

or better

#### Damiano Testa (Apr 13 2021 at 15:08):

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

#### Eric Wieser (Apr 13 2021 at 15:11):

By "units" you mean `1`

or "pieces of code from Eric and Kevin"?

#### Damiano Testa (Apr 13 2021 at 15:14):

Eric, I meant the elements `1`

in `R`

and the element `1`

in `graded_piece (0 : M)`

.

#### Eric Wieser (Apr 13 2021 at 15:28):

Note that even without the `(1 : R)`

axiom you can still create an instance of docs#direct_sum.ghas_mul, which shortly after #6786 will result in a `non_unital_semiring`

structure on `add_grading M R`

#### Damiano Testa (Apr 13 2021 at 15:34):

Ok, I am happy with that, thanks! Also, I wanted to make sure that we *did not* face non-unital rings (even in the degree `0`

graded_piece`), hence my questions! I would not want to demote these graded rings to graded rngs!

#### Kevin Buzzard (Apr 13 2021 at 16:52):

Aargh `complete_lattice.independent`

is a statement about subsets and we have a map from a monoid, so for example if the monoid is nontrivial and the map sends every element of the monoid to the same nonzero `add_subgroup`

then they won't be independent in the sense I wrote (and that we need) but they'll be independent in the sense that the range of the function has size 1.

#### Eric Wieser (Apr 13 2021 at 16:56):

Oh, nice catch

#### Adam Topaz (Apr 13 2021 at 16:57):

Just make the function`graded_piece`

injective?

#### Riccardo Brasca (Apr 13 2021 at 16:58):

As sanity check I proved the easy implication of theorem 2 of the blueprint, here

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

#### Eric Wieser (Apr 13 2021 at 16:59):

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

#### Adam Topaz (Apr 13 2021 at 16:59):

Eric Wieser said:

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

How big of a refactor would this be?

#### Adam Topaz (Apr 13 2021 at 17:00):

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

#### Eric Wieser (Apr 13 2021 at 17:02):

I've no idea how big that refactor would be, but I don't think `complete_lattice.independent`

is used in all that many places yet

#### Eric Wieser (Apr 13 2021 at 17:02):

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

#### Kevin Buzzard (Apr 13 2021 at 17:06):

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

#### Kevin Buzzard (Apr 13 2021 at 17:09):

`span`

is just a statement about a Sup

#### Adam Topaz (Apr 13 2021 at 17:11):

Kevin Buzzard said:

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

IIRC a grading by a monoid M on an `R`

-algebra is "the same" as a coaction of `R[M]`

?

#### Adam Topaz (Apr 13 2021 at 17:11):

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

#### Kevin Buzzard (Apr 13 2021 at 17:11):

Aha, this is some monoid scheme maybe

#### Kevin Buzzard (Apr 13 2021 at 17:12):

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

#### Kevin Buzzard (Apr 13 2021 at 17:15):

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

#### Eric Wieser (Apr 13 2021 at 17:15):

Do people grade with noncommutative monoids ever?

Based on what I found for docs#direct_sum.semiring (as opposed to docs#direct_sum.comm_semiring), if your ring is not commutative then you don't need your index set to be either.

Not that that answers the question of whether its useful, just that its easy to generalize to.

#### Adam Topaz (Apr 13 2021 at 17:17):

Kevin Buzzard said:

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

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

#### Kevin Buzzard (Apr 13 2021 at 17:18):

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

#### Filippo A. E. Nuccio (Apr 13 2021 at 18:14):

I have looked a bit into your discussion, seeing that you're going to attack Gordan. I won't be of great help with the grading mafia but I'd be help to adapt the current proof of `lem97`

to a new statement of `explicit_gordan`

, if you come up with something different from what I used there.

#### Julian Külshammer (Apr 13 2021 at 18:14):

@Kevin Buzzard Is the emphasis on noncommutative or on monoids? There are articles written in my area of research about gradings by non-commutative groups and one definitely wants to consider `\N`

-gradings as well, so grading by possibile non-commutative monoids seems like an obvious choice for me. In most examples people compute the grading is by `\N^r`

or `\Z^r`

or `Z/2`

, but I also don't see why it should be more difficult to formalise a grading by a noncommutative monoid than a commutative monoid. Do you have an example of a basic result which fails?

#### Damiano Testa (Apr 13 2021 at 18:27):

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

#### Riccardo Brasca (Apr 14 2021 at 21:21):

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

```
lemma monoid_alg_ft_iff_fg [nontrivial R] :
(⊤ : submodule ℕ M).fg ↔ finite_type R (add_monoid_algebra R M)
```

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

#### Kevin Buzzard (Apr 14 2021 at 21:23):

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

#### Riccardo Brasca (Apr 14 2021 at 21:23):

We already have this!

#### Kevin Buzzard (Apr 14 2021 at 21:26):

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

#### Damiano Testa (Apr 15 2021 at 05:21):

Kevin, is the definition of grading that you are using the one in

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Gradings.20on.20a.20ring/near/234389540

I would be happy to contribute!

#### Kevin Buzzard (Apr 15 2021 at 06:19):

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

#### Damiano Testa (Apr 15 2021 at 06:20):

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

#### Kevin Buzzard (Apr 15 2021 at 06:21):

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

#### Kevin Buzzard (Apr 15 2021 at 07:55):

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

The mathlib branch `independent2`

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

The mathlib branch `grading`

contains `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 (Apr 15 2021 at 08:00):

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

#### Kevin Buzzard (Apr 15 2021 at 08:13):

The question is whether we should be continuing to battle through this proof (I think we should *not*) or whether we should prove that the bijection is an injection and a surjection, and injection is equivalent to `independent`

and surjection equivalent to `span`

.

#### Kevin Buzzard (Apr 15 2021 at 08:16):

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

.

#### Damiano Testa (Apr 15 2021 at 08:17):

Ok, thanks a lot!

#### Kevin Buzzard (Apr 15 2021 at 08:38):

OK I pushed. In the `grading`

branch of mathlib there are a bunch of sorries. My guess is that `direct_sum.add_submonoid_is_internal_iff_independent_and_span`

helps (although it should be broken into two lemmas) with the examples, but I don't know for sure.

Unfortunately, you might have to wait for the oleans, or make them yourself (this is what I have been doing -- I do `leanproject get-cache --rev 07614552f6b7157fa5582a8f2a536b390715cb14`

and then `lean --make src/ring_theory/grading.lean`

on the command line and wait about 5 minutes). Alternatively you can wait a few hours and then `leanproject get-cache`

should work fine.

#### Damiano Testa (Apr 15 2021 at 08:40):

Thanks a lot, Kevin, for `grading`

and for the instructions!

#### Eric Wieser (Apr 15 2021 at 12:55):

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

#### Damiano Testa (Apr 15 2021 at 12:57):

I certainly assumed so: I pulled `grading`

from mathlib.

#### Eric Wieser (Apr 15 2021 at 13:12):

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

#### Eric Wieser (Apr 15 2021 at 13:14):

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

over `p.support`

"

#### Kevin Buzzard (Apr 15 2021 at 14:04):

Can someone put me out of my misery?

```
import algebra.direct_sum
import data.polynomial.basic
open polynomial
def polynomial_equiv (R : Type*) [semiring R] :
(polynomial R) ≃
direct_sum ℕ (λ i, add_monoid_hom.mrange (monomial i).to_add_monoid_hom) :=
sorry
-- error: don't know how to synthesize placeholder
```

I can't get the equiv to typecheck :-(

#### Kevin Buzzard (Apr 15 2021 at 14:06):

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

#### Kevin Buzzard (Apr 15 2021 at 14:51):

I am going nuts -- I have still not manage to state this equiv :-(

```
import algebra.direct_sum
import data.polynomial.basic
open polynomial
noncomputable example (R : Type) [semiring R] (i : ℕ) :
add_comm_monoid ((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange : Type) := infer_instance
noncomputable def foo (R : Type) [semiring R] :
(direct_sum ℕ (λ i, (monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange)) →
polynomial R :=
⇑(direct_sum.to_add_monoid
(λ i,
((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange.subtype :
((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange : Type) →+ polynomial R)))
/-
type mismatch at application
direct_sum.to_add_monoid (λ (i : ℕ), (monomial i).to_add_monoid_hom.mrange.subtype)
term
λ (i : ℕ), (monomial i).to_add_monoid_hom.mrange.subtype
has type
Π (i : ℕ), ↥((monomial i).to_add_monoid_hom.mrange) →+ polynomial R : Type
but is expected to have type
Π (i : ℕ), ?m_1 i →+ ?m_2 : Type (max ? ?)
-/
```

What am I doing wrong?

#### Eric Wieser (Apr 15 2021 at 14:58):

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

#### Eric Wieser (Apr 15 2021 at 15:03):

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

#### Eric Wieser (Apr 15 2021 at 15:18):

If you break it into tiny pieces it cooperates:

```
noncomputable def monomial_add_monoid_hom (R : Type) [semiring R] (n : ℕ) : R →+ polynomial R :=
(monomial n).to_add_monoid_hom
def direct_sum.submonoids_to_add_monoid (ι R : Type) [decidable_eq ι] [semiring R]
(A : ι → add_submonoid R) :
(direct_sum ι (λ i, A i)) →+ R :=
direct_sum.to_add_monoid (λ i, (A i).subtype)
noncomputable def foo (R : Type) [semiring R] :
(direct_sum ℕ (λ i, (monomial_add_monoid_hom R i).mrange)) →+ polynomial R :=
direct_sum.submonoids_to_add_monoid ℕ (polynomial R) (λ i, (monomial_add_monoid_hom R i).mrange)
```

#### Eric Wieser (Apr 15 2021 at 15:20):

Ah, this works:

```
noncomputable def foo (R : Type) [semiring R] :
(direct_sum ℕ (λ i, ((monomial i).to_add_monoid_hom : R →+ _).mrange)) →+ polynomial R :=
direct_sum.to_add_monoid (λ i, (monomial i).to_add_monoid_hom.mrange.subtype)
```

#### Eric Wieser (Apr 15 2021 at 15:21):

IN fact, it's the `⇑`

causing you all the pain in your example

#### Kevin Buzzard (Apr 15 2021 at 15:34):

Thanks! I put the `⇑`

in because it wasn't working without it (indeed what I posted doesn't work without the `⇑`

either)

#### Kevin Buzzard (Apr 15 2021 at 15:35):

Hmm, I see. This is supposed to be a field of an `equiv`

. So I just tell it the type of the add_monoid_hom I guess.

#### Yakov Pechersky (Apr 15 2021 at 15:42):

My rule of thumb is that one should not put coercion arrows in lemma statements (or function coercion). If a coercion is necessary, it should be notated using typing syntax `(_ : _)`

, and if it is function coercion, just apply as normal

#### Eric Wieser (Apr 15 2021 at 15:59):

Kevin Buzzard said:

(indeed what I posted doesn't work without the

`⇑`

either)

It does once you replace the `→`

with `→+`

I think

#### Kevin Buzzard (Apr 15 2021 at 15:59):

But here's the actual problem:

```
import algebra.direct_sum
import data.polynomial.basic
open polynomial
def polynomial_equiv (R : Type) [semiring R] :
polynomial R ≃
direct_sum ℕ (λ i, (monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange) :=
{ to_fun := sorry,
inv_fun := (direct_sum.to_add_monoid
(λ i,
((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange.subtype :
((monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange : Type) →+ polynomial R))),
left_inv := sorry,
right_inv := sorry }
```

#### Kevin Buzzard (Apr 15 2021 at 16:00):

```
type mismatch at application
direct_sum.to_add_monoid (λ (i : ℕ), (monomial i).to_add_monoid_hom.mrange.subtype)
term
λ (i : ℕ), (monomial i).to_add_monoid_hom.mrange.subtype
has type
Π (i : ℕ), ↥((monomial i).to_add_monoid_hom.mrange) →+ polynomial R : Type
but is expected to have type
Π (i : ℕ), ?m_1 i →+ ?m_2 : Type (max ? ?)
```

#### Kevin Buzzard (Apr 15 2021 at 16:01):

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

#### Eric Wieser (Apr 15 2021 at 16:17):

Why not define it as an add_equiv?

#### Kevin Buzzard (Apr 15 2021 at 16:18):

all I want to do is to prove that a function is bijective. It seemed to me that defining it as an `add_equiv`

just meant I'd have to prove more things for no reason.

#### Eric Wieser (Apr 15 2021 at 16:27):

Here you go:

```
import algebra.direct_sum
import data.polynomial.basic
open polynomial
open_locale direct_sum
noncomputable theory
abbreviation monomial.submonoid (R : Type) [semiring R] (i : ℕ) : add_submonoid (polynomial R) :=
(monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange
def polynomial_equiv (R : Type) [semiring R] :
(⨁ i, monomial.submonoid R i) ≃+ polynomial R :=
{ inv_fun := λ p, p.sum (λ n r, direct_sum.of _ n (by exact ⟨monomial n r, r, trivial, rfl⟩)),
left_inv := λ d, sorry,
right_inv := λ p, sorry,
..(direct_sum.to_add_monoid
(λ i, (monomial.submonoid R i).subtype) : (⨁ i, monomial.submonoid R i) →+ _) }
```

#### Kevin Buzzard (Apr 15 2021 at 16:28):

Thanks! I might not get back to this until tomorrow now -- right now I'm struggling with stuff like `∏ᶠ (i_1 : ι), ite (i_1 = i) x 1 = x`

#### Eric Wieser (Apr 15 2021 at 16:52):

Solved:

```
import algebra.direct_sum
import data.polynomial.basic
import data.polynomial
open polynomial
open_locale direct_sum
noncomputable theory
abbreviation monomial.submonoid (R : Type) [semiring R] (i : ℕ) : add_submonoid (polynomial R) :=
(monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange
abbreviation monomial.to_submonoid (R : Type) [semiring R] (i : ℕ) : R →+ monomial.submonoid R i :=
(monomial i : R →ₗ polynomial R).to_add_monoid_hom.mrange_restrict
def polynomial_equiv (R : Type) [semiring R] :
(⨁ i, monomial.submonoid R i) ≃+ polynomial R :=
add_monoid_hom.to_add_equiv
(direct_sum.to_add_monoid $ λ i,
(monomial.submonoid R i).subtype)
(finsupp.lift_add_hom $ λ n,
(direct_sum.of (λ i, monomial.submonoid R i) n).comp (monomial.to_submonoid R n))
(begin
ext i ⟨x, r, _, rfl⟩ : 2,
dsimp,
simp [monomial],
refl,
end)
(begin
ext i r : 2,
dsimp,
simp [monomial],
end)
```

#### Yakov Pechersky (Apr 15 2021 at 16:52):

`simp ..., refl`

also known as `simpa`

#### Eric Wieser (Apr 15 2021 at 16:52):

`simp [monomial]`

is needed because you're not supposed to use `finsupp.lift_add_hom`

on polynomials

#### Kevin Buzzard (Apr 15 2021 at 17:13):

oh it doesn't compile for me :-(

#### Kevin Buzzard (Apr 15 2021 at 17:22):

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

#### Kevin Buzzard (Apr 15 2021 at 17:29):

OK great, it works on my branch, now I have to wait for several more hours and then pay some money to download oleans :-/ (my internet is broken right now)

#### Damiano Testa (Apr 15 2021 at 19:06):

To be honest, I do not understand the proof, but is this the same as Eric's proof, except for an `add_monoid_algebra`

?

```
variables (R ι : Type) [semiring R] (M : Type) [add_monoid M] [decidable_eq M] [decidable_eq ι]
open polynomial
open_locale direct_sum
noncomputable theory
section add_monoid_algebra
/-- `monomial s a` is the monomial `a * X^s` -/
noncomputable def Mm (i : M) : R →ₗ[R] add_monoid_algebra R M :=
finsupp.lsingle i
abbreviation monomial.submonoid (i : M) : add_submonoid (add_monoid_algebra R M) :=
(Mm R M i : R →ₗ add_monoid_algebra R M).to_add_monoid_hom.mrange
abbreviation monomial.to_submonoid (i : M) : R →+ monomial.submonoid R M i :=
(Mm R M i : R →ₗ add_monoid_algebra R M).to_add_monoid_hom.mrange_restrict
def polynomial_equiv :
(⨁ i, monomial.submonoid R M i) ≃+ add_monoid_algebra R M :=
add_monoid_hom.to_add_equiv
(direct_sum.to_add_monoid $ λ i,
(monomial.submonoid R M i).subtype)
(finsupp.lift_add_hom $ λ n,
(direct_sum.of (λ i, monomial.submonoid R M i) n).comp (monomial.to_submonoid R M n))
(begin
ext i ⟨x, r, _, rfl⟩ : 2,
simpa [Mm],
end)
(begin
ext i r : 2,
simp [Mm],
end)
end add_monoid_algebra
```

#### Eric Wieser (Apr 15 2021 at 19:19):

Right, a monoid_algebra version is probably sensible

#### Eric Wieser (Apr 15 2021 at 19:19):

You can use finsupp.single_add_hom instead of touching lsingle

#### Damiano Testa (Apr 15 2021 at 19:24):

I have not managed to get `finsupp.single_add_hom`

to work.

However, if I replace randomly `add_monoid_algebra`

with `monoid_algebra`

, not even everywhere, it seems to me that Lean does not complain: is this normal?

#### Damiano Testa (Apr 15 2021 at 19:24):

Am I missing something?

#### Damiano Testa (Apr 15 2021 at 19:29):

About the `finsupp.single_add_hom`

: I should change the type of `Mm (i : M)`

to be `R →+ add_monoid_algebra R M`

, right?

If I do so, though, the abbreviations are not happy afterwards...

#### Eric Wieser (Apr 15 2021 at 19:30):

I think actually we want the version relating dfinsupp and finsupp

#### Damiano Testa (Apr 15 2021 at 19:30):

Got it!

```
/-- `monomial s a` is the monomial `a * X^s` -/
noncomputable def Mm (i : M) : R →+ add_monoid_algebra R M :=
finsupp.single_add_hom i
abbreviation monomial.submonoid (i : M) : add_submonoid (add_monoid_algebra R M) :=
(Mm R M i : R →+ add_monoid_algebra R M).mrange
abbreviation monomial.to_submonoid (i : M) : R →+ monomial.submonoid R M i :=
(Mm R M i : R →+ add_monoid_algebra R M).mrange_restrict
def polynomial_equiv :
(⨁ i, monomial.submonoid R M i) ≃+ add_monoid_algebra R M :=
add_monoid_hom.to_add_equiv
(direct_sum.to_add_monoid $ λ i,
(monomial.submonoid R M i).subtype)
(finsupp.lift_add_hom $ λ n,
(direct_sum.of (λ i, monomial.submonoid R M i) n).comp (monomial.to_submonoid R M n))
(begin
ext i ⟨x, r, _, rfl⟩ : 2,
simpa only [Mm, set_like.coe_mk, finsupp.lift_add_hom_apply_single, direct_sum.to_add_monoid_of,
add_monoid_hom.coe_comp, finsupp.single_add_hom_apply, function.comp_app,
add_submonoid.coe_subtype],
end)
(begin
ext i r : 2,
simp only [Mm, finsupp.lift_add_hom_apply_single, direct_sum.to_add_monoid_of,
add_monoid_hom.coe_mrange_restrict, add_monoid_hom.coe_comp, finsupp.single_add_hom_apply,
function.comp_app, add_submonoid.coe_subtype, add_monoid_hom.id_apply],
end)
```

#### Eric Wieser (Apr 15 2021 at 19:31):

So replace `add_monoid_algebra`

with `finsupp`

, and `direct_sum`

with `dfinsupp`

#### Damiano Testa (Apr 15 2021 at 19:32):

In any case, I view this simply as a confirmation that your approach is very robust: I could adapt it to work for the (add_)monoid_graded case, from the polynomial case, without actually understanding how it was working!

#### Eric Wieser (Apr 15 2021 at 19:32):

Well those types are defeq!

#### Eric Wieser (Apr 15 2021 at 19:32):

I'll PR a dfinsupp / finsupp version tomorrow

#### Damiano Testa (Apr 15 2021 at 19:33):

Well those types are defeq!

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

#### Eric Wieser (Apr 15 2021 at 19:35):

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

#### Damiano Testa (Apr 15 2021 at 19:36):

I tried to do the replacement `finsupp + dfinsupp`

, but I have failed. It is also getting late, so I may not give it a go tonight!

#### Eric Wieser (Apr 15 2021 at 19:36):

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

#### Damiano Testa (Apr 15 2021 at 19:36):

Btw, what is the `: 2`

in ext?

#### Eric Wieser (Apr 15 2021 at 19:36):

Ie, by solving `f.comp f_inv = id`

#### Eric Wieser (Apr 15 2021 at 19:37):

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

#### Damiano Testa (Apr 15 2021 at 19:37):

ah, like `congr' 2`

?

#### Eric Wieser (Apr 15 2021 at 19:37):

It means "apply ext twice"

#### Damiano Testa (Apr 15 2021 at 19:37):

except with ext?

#### Eric Wieser (Apr 15 2021 at 19:37):

Yes

#### Damiano Testa (Apr 15 2021 at 19:54):

I squeezed the the two `simp`

s to speed up the processing: there is quite a lot of lemmas that show up!

#### Damiano Testa (Apr 15 2021 at 19:54):

Anyway, I'm off for the day!

Kevin and Eric, thanks a lot for gradings!

#### Kevin Buzzard (Apr 15 2021 at 21:53):

These isomorphisms aren't the end of it, but they're definitely the hardest part. One also needs to check that `1`

and `*`

are well-behaved.

#### Kevin Buzzard (Apr 15 2021 at 21:53):

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

#### Eric Wieser (Apr 16 2021 at 08:20):

#### Eric Wieser (Apr 16 2021 at 08:22):

Typeclass search really wasn't happy here

#### Eric Wieser (Apr 16 2021 at 08:46):

Frustratingly `add_monoid_hom.range`

and `add_monoid_hom.mrange`

are not defeq as types, so probably some refactoring to do before I can get the add_comm_group version easily

#### Kevin Buzzard (Apr 16 2021 at 09:54):

These two monoid `range`

things can be a bit annoying to work with because the definition always involves having to prove `mem_top`

. `set.range`

does not have this problem.

#### Eric Wieser (Apr 16 2021 at 10:35):

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

#### Eric Wieser (Apr 16 2021 at 10:37):

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

#### Kevin Buzzard (Apr 16 2021 at 10:41):

#### Eric Wieser (Apr 16 2021 at 10:44):

Oops, fixed

#### Eric Wieser (Apr 16 2021 at 10:44):

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

#### Kevin Buzzard (Apr 20 2021 at 15:17):

@Johan Commelin I need some API for `finite_free`

. In `polyhedral_lattice.basic`

you have a `move_this`

section containing the definition. If I remove `[semimodule ℤ A]`

from the definition (`A`

is an `add_comm_group`

) then the `combinatorial_lemma`

file stops compiling: I get an error on line 378 with `rw oops`

failing; `oops`

is a proof of `@polyhedral_lattice.int_semimodule Λ _ = @add_comm_group.int_module Λ _`

. If I remove the proof of `oops`

and the rewrite, things work again. Is this what I'm supposed to be doing or are there reasons for me not to fiddle with this? The reason I ask is that my instinct is to set up `finite_free`

for `comm_group`

s as well as `add_comm_group`

s and I'm not sure a `comm_group`

can be a Z-module in Lean.

#### Kevin Buzzard (Apr 20 2021 at 15:25):

bleurgh I now get errors in `polyhedral_lattice.finsupp`

. Maybe I'll leave this until after the int refactor, my guess is that I have clashing semimodule instances here.

#### Johan Commelin (Apr 20 2021 at 18:29):

@Kevin Buzzard All of this will be solved in 1 or 2 days, when @Sebastien Gouezel's `gsmul`

PR is merged into mathlib.

#### Johan Commelin (Apr 20 2021 at 18:30):

So I would suggest to just add `[semimodule int A]`

assumptions for now, and we'll remove them in two days.

#### Kevin Buzzard (Apr 20 2021 at 21:44):

The next problem I find I'm running into is that I'm reluctant to do anything involving `is_basis`

now Anne has told us that they're bundling it. Right now I'm sorrying a bunch of basic algebra stuff and just trying to push on with the more serious stuff.

#### Eric Wieser (Apr 21 2021 at 18:32):

It seems that every time I try to generalize things about `finsupp`

/ `add_monoid_algebra`

/ `dfinsupp`

/ `direct_sum`

, it makes things harder not easier for me... After making what I thought would be some handy API in #7217 and #7293, I had to fight an more-awful-than-before battle against the elaborator, and a similarly awful fight with `ext`

. In the end I was able to construct:

```
/-- There is a ring equivalence between an `add_monoid_algebra` (e.g. a `polynomial`) and
the direct sum of `single_mrange k i` (e.g. the monomials of degree `i`). -/
def to_direct_sum_mrange : add_monoid_algebra k G ≃+* ⨁ i : G, single_mrange k i := _
```

#### Kevin Buzzard (Apr 21 2021 at 18:44):

But these feel to me like the things we need in the API, so it's great that you're managing to do them; hopefully users can just hide behind what you're doing. The maps are nice, the proofs are hard but hopefully people will only need the maps.

#### Eric Wieser (Apr 21 2021 at 18:50):

But even using the maps was hard

#### Eric Wieser (Apr 21 2021 at 18:50):

See my first link

#### Eric Wieser (Apr 21 2021 at 18:51):

`@`

and `letI`

everywhere

#### Johan Commelin (Apr 21 2021 at 19:04):

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

#### Johan Commelin (Apr 21 2021 at 19:05):

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

.

#### Eric Wieser (Apr 21 2021 at 19:26):

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

?

#### Johan Commelin (Apr 21 2021 at 19:32):

Well, or maybe even submodules of `add_monoid_algebra`

#### Johan Commelin (Apr 21 2021 at 19:32):

Can we have an "intrinsic" definition of `graded_ring`

?

#### Eric Wieser (Apr 21 2021 at 19:39):

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

#### Eric Wieser (Apr 21 2021 at 19:39):

For which an external direct sum is easier

#### Eric Wieser (Apr 21 2021 at 20:07):

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

#### Adam Topaz (Apr 21 2021 at 20:25):

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

#### Kevin Buzzard (Apr 21 2021 at 21:31):

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

#### Kevin Buzzard (Apr 25 2021 at 23:05):

Adam gave an update so I thought I'd give one too. I've had to made an API for gradings on rings and this has turned out to be delicate, just for stupid reasons: $R=\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 `m`

th 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 (May 03 2021 at 19:13):

It sounds like Coq may now have enough basics on polyhedral stuff for the "convex geometry" proof of Gordan's lemma https://arxiv.org/abs/2104.15021

#### Patrick Massot (May 03 2021 at 19:34):

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

#### Peter Scholze (May 03 2021 at 19:39):

No I'm not, no worries

#### Kevin Buzzard (May 03 2021 at 19:50):

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

#### Yaël Dillies (May 03 2021 at 19:51):

Oh hey yeah! Anything you need?

#### Johan Commelin (May 03 2021 at 19:52):

A port of that paper would be nice :stuck_out_tongue_wink:

#### Bhavik Mehta (May 03 2021 at 20:13):

I think we might have enough convex geometry to get close to the geometry proof of Gordan's lemma since we have Krein-Milman, HB and supporting/separating hyperplane lemmas

#### Bhavik Mehta (May 03 2021 at 20:15):

But from talking to @Kevin Buzzard I understand it might be better to get the algebraic proof so that the theory of graded rings gets developed better?

#### Johan Commelin (May 03 2021 at 20:15):

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

#### Yaël Dillies (May 05 2021 at 16:00):

I read through the paper and all of this sounds very doable and interesting! I'm already PRing exposed faces, and then Krein-Milman. We shall see how far I get on the rest.

#### Yaël Dillies (May 05 2021 at 16:01):

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

#### Kevin Buzzard (May 05 2021 at 16:06):

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

#### Riccardo Brasca (May 07 2021 at 14:00):

If we are still interested in the algebraic proof `add_monoid_algebra.finite_type_iff_fg`

is now in mathlib. I will add the easy (and I think useless for LTE) version for groups next week.

#### Johan Commelin (May 07 2021 at 15:05):

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

#### Johan Commelin (May 07 2021 at 15:07):

Unless @Bhavik Mehta and @Yaël Dillies think they can prove `explicit_gordan`

before Kevin is done with grading exams, of course.

#### Bhavik Mehta (May 07 2021 at 15:48):

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

#### Johan Commelin (May 07 2021 at 16:05):

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

#### Kevin Buzzard (May 07 2021 at 19:09):

@Bhavik Mehta just to be clear, there are several "Gordan's Lemma"s in the literature -- the one we want is much stronger than the one we were talking about recently, it needs all that matrix elimination stuff. I pointed you to precisely the lemma we needed in the LTE IIRC

#### Bhavik Mehta (May 07 2021 at 19:45):

Kevin Buzzard said:

Bhavik Mehta just to be clear, there are several "Gordan's Lemma"s in the literature -- the one we want is much stronger than the one we were talking about recently, it needs all that matrix elimination stuff. I pointed you to precisely the lemma we needed in the LTE IIRC

In what sense is it much stronger? I think the only difference from the one we talked about (with finite intersections of rational hyperplanes) was that the version I was doing was for Z^n rather than any more general version

#### Kevin Buzzard (May 07 2021 at 20:30):

Bhavik, if you can prove the version in LTE that would be absolutely fabulous. I am just pointing out that you showed me a lemma in a book and the lemma was called Gordan's Lemma but it was not what we are calling Gordan's Lemma, and what we want is what we are calling Gordan's Lemma.

#### Kevin Buzzard (May 07 2021 at 20:34):

We were initially going to do the topological proof, but then I decided that the algebraic proof looked easier, so I started on this, but then internal grading turned out to be subtle (but do-able) so I'm persevering with it, but now the topological proof is looking easier again.

I just did `rw submodule.smul_mem`

and it failed, so I did `rw @submodule.smul_mem [fill in all the fields]`

and this happened. Note that `pp.all`

was off, I just triggered the Lean "display more information if the pretty printer says that the terms match but I know they don't".

#### Kevin Buzzard (May 07 2021 at 20:38):

But my work will not be wasted because we have developed a grading API and I'm putting it through its paces (I suspect I know what I did wrong to get that error, by the way!)

#### Kevin Buzzard (May 07 2021 at 22:48):

If I use `convert`

instead of `refine`

then my 2000-line-long error turns into

```
grade_zero.has_scalar (λ (i : A), ↥(Gᵢ i)) a = smul_with_zero.to_has_scalar
```

Last updated: May 09 2021 at 23:10 UTC