gordan's lemma

Stream: condensed mathematics

[Johan Commelin]

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

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]

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

[Johan Commelin]

That's a subsemiring, and it wants a submodule

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I guess f should be R-linear

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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]

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]

@Damiano Testa yes, I agree

[Johan Commelin]

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]

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]

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]

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]

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]

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

[Johan Commelin]

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]

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]

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

[Yaël Dillies]

Do we want Gordan's lemma in mathlib?

[Johan Commelin]

Yes!

[Johan Commelin]

But I think it depends on the nnrat.lean file about about nonnegative rationals. And that is duplicating nnreal.lean. So we want some API generalizing the two.

[Johan Commelin]

If I'm not mistaken, @Floris van Doorn wrote stuff about a general nonneg subtype a while ago. But I don't think nnrat.lean was adapted to that.

[Yaël Dillies]

I haven't had much of a look at nnrat, but is it defined as nonneg ℚ or as coprime pairs of naturals?

[Johan Commelin]

/-- Nonnegative rational numbers. -/
def nnrat := {q : ℚ // 0 ≤ q}
localized "notation ` ℚ≥0 ` := nnrat" in nnreal

[Yaël Dillies]

That looks like nonneg to me!

[Johan Commelin]

Yep, but it doesn't use src/algebra/order/nonneg.lean at all, because history

[Yaël Dillies]

I guess we can try adapting it then.

[Floris van Doorn]

Almost all instances can be gotten from from nonneg, but it doesn't have much else yet (for lemmas you probably also prefer nnrat.my_lemma over nonneg.my_lemma).

I love deleting things, so I'll make the changes.

[Yaël Dillies]

I would really love to see Gordan's lemma in mathlib, so tell me what I can take care of.

[Floris van Doorn]

What is the workflow for lean-liquid? Build locally and if it builds, push?

[Yaël Dillies]

I personally only ever pushed to mathlib, but I was working on leaf files, or rather leaf declarations.

[Johan Commelin]

@Floris van Doorn Yep, that's right.

[Johan Commelin]

Sorry's are fine, but compile errors should be avoided.

[Johan Commelin]

And please don't break the proof in liquid.lean (-;

[Floris van Doorn]

There were 2 minor breakages, but nowhere near liquid.lean :-)

[Floris van Doorn]

I pushed.
There is still a lot of stuff duplicated in nnreal/nnrat that could be moved to nonneg, but currently I think everything that is in nonneg is now used in nnrat.

[Johan Commelin]

@Floris van Doorn what do you think? would it make sense to PR this to mathlib, and deduplicate later?

[Floris van Doorn]

Yeah, I think that is completely fine.

[Yaël Dillies]

What even is duplicated? Lemmas? Is it a problem of not having the correct typeclass? Are you telling me I should write more order typeclasses?

[Johan Commelin]

@Yaël Dillies nnrat.lean is currently ~ 500 lines. I would be surprised if there's more than 50 lines of lemmas that aren't exact duplicates of lemmas that hold for nnreal.

[Yaël Dillies]

Ohohoh!