# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: gordan's lemma

#### Johan Commelin (Mar 10 2021 at 10:37):

@Damiano Testa I tried to write down a statement of Gordan's lemma together with @Filippo A. E. Nuccio.

We got

```
def nat_submodule : submodule ℕ ℤ := sorry
lemma gordan (hΛ_tf : torsion_free Λ) [hΛ_fg : module.finite ℤ Λ]
(l : finset Λ) :
((dual_pairing ℤ Λ).dual_set nat_submodule (l : set Λ)).fg :=
begin
sorry
end
```

#### Johan Commelin (Mar 10 2021 at 10:37):

That `nat_submodule`

is a bit awkward. Do you think you can refactor the definition of `dual_set`

so that we can just use `\N`

there?

#### Damiano Testa (Mar 10 2021 at 10:41):

I will look into this, but would using `nnR \Z`

work?

#### Johan Commelin (Mar 10 2021 at 10:45):

That's a subsemiring, and it wants a submodule

#### Johan Commelin (Mar 10 2021 at 10:46):

So then you need to cast, which makes me fear that you'll end up with a very annoying copy of `\N`

to work with.

#### Damiano Testa (Mar 10 2021 at 10:47):

ah, so even if there were an instance from a subsemiring to a subsemimodule you think that it would not be useful?

#### Johan Commelin (Mar 10 2021 at 10:47):

Right, I think it will be unpleasant to work with in the proof of 9.7

#### Damiano Testa (Mar 10 2021 at 10:47):

I can try to refactor `dual_set`

, but what should it take as input for semimodule?

#### Johan Commelin (Mar 10 2021 at 10:48):

Maybe a `P0`

, and a `is_inj_nonneg f`

for some `f : P0 -> P`

?

#### Johan Commelin (Mar 10 2021 at 10:48):

Hmm, but that gives you back the order structure on `P`

, which we wanted to avoid

#### Johan Commelin (Mar 10 2021 at 10:49):

So maybe just `f : P0 -> P`

, possibly injective?

#### Johan Commelin (Mar 10 2021 at 10:49):

I guess `f`

should be `R`

-linear

#### Damiano Testa (Mar 10 2021 at 10:50):

Ok, I will try to aim for \N to simply work in this context, possibly at the cost of introducing some extra data, like an injection somewhere.

#### Damiano Testa (Mar 10 2021 at 10:51):

after all, Eric wants to make multiplications by \N *always* smuls, right? this plays in our favour here... :upside_down:

#### Damiano Testa (Mar 10 2021 at 10:51):

But I will likely not get around to this today and probably not tomorrow either. I should have some more time on Friday.

#### Johan Commelin (Mar 10 2021 at 10:52):

Sure no worries, there is no need to haste :wink:

#### Damiano Testa (Mar 10 2021 at 10:52):

so, if in the meantime you play some more with this and come up with something that would definitely be good for you, let me know!

#### Johan Commelin (Mar 10 2021 at 12:10):

I pushed a very explicit version of Gordan's lemma, that should be exactly in the shape that we need for 9.7.

We can later work on gluing this version to whatever rolls out of Damiano's toric efforts.

#### Damiano Testa (Mar 10 2021 at 15:27):

I am looking at what you did for the statement of Gordan's lemma. It seems that you circumvented the problem by defining an *ad hoc* `dual_set`

, right?

So, in terms of refactoring, there will simply be the need for some conversion between your version and the one that is in the toric branch, am I correct?

#### Johan Commelin (Mar 10 2021 at 15:28):

@Damiano Testa yes, I agree

#### Johan Commelin (Mar 10 2021 at 15:29):

this will allow us to work on 9.7, and we can smoothen things once we have a proof of the "correct, general" version of Gordan's lemma

#### Johan Commelin (Mar 10 2021 at 15:30):

Maybe we even want to keep this ad hoc version. Then we don't have to worry about refactoring `dual_set`

for now.

#### Damiano Testa (Mar 10 2021 at 15:31):

Sounds good! Also, at some point, the inequalities will probably need to enter the picture anyway and I would certainly like to see the statement that you formalized proved in Lean!

#### Johan Commelin (Mar 13 2021 at 18:45):

If we can make the proof of Gordan's lemma constructive (it computes explicit generators of the dual submonoid, given an explicit finite list of elements), then we can make the constant $d$ in lemma 9.8 computable. That in turn would make all the other constants computable, as far as I can tell.

#### Damiano Testa (Mar 13 2021 at 19:07):

I do not know much about computability, but, as I understand the proof now of Gordan's lemma, there will be two "kinds" of generators:

- a set of generators that is, "up to finite index", the correct one;
- some more elements to add, in order to saturate the previous set.

The elements of the first part are, in spirit, the elements of a basis, so I would imagine that they will be computable, if basis of vector spaces are.

The elements of the second set at the elements in the intersection of a "cube" centered at the origin with the elements of the subsemimodule. Here is where I am not entirely how computability would work out.

#### Johan Commelin (Mar 13 2021 at 19:15):

@Damiano Testa here I don't mean anything philosophical with computability. Just that we get an actual algorithm that you can run.

#### Johan Commelin (Mar 13 2021 at 19:15):

I guess, if we can get an explicit bound on the radius of the "cube" in the second set, then we're fine.

#### Johan Commelin (Mar 13 2021 at 19:15):

And I'm quite sure that this will work, because there are all sorts of software packages out there that can do such computations, right?

#### Damiano Testa (Mar 13 2021 at 21:01):

In that case, the proof might indeed give an algorithm, since the "box" should be explicit.

Last updated: May 09 2021 at 16:20 UTC