Zulip Chat Archive

Stream: condensed mathematics

Topic: gordan's lemma


view this post on Zulip 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

view this post on Zulip 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?

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

I will look into this, but would using nnR \Zwork?

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

That's a subsemiring, and it wants a submodule

view this post on Zulip 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.

view this post on Zulip 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?

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

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

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

I can try to refactor dual_set, but what should it take as input for semimodule?

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

Maybe a P0, and a is_inj_nonneg f for some f : P0 -> P?

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

Hmm, but that gives you back the order structure on P, which we wanted to avoid

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

So maybe just f : P0 -> P, possibly injective?

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

I guess f should be R-linear

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

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

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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?

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

@Damiano Testa yes, I agree

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 dd in lemma 9.8 computable. That in turn would make all the other constants computable, as far as I can tell.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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