linear order on finsupps

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is there code already for defining a linear order on finsupps with source and target that are linearly ordered?

Specifically, I would like to have

def finsupp.lex {α N} [linear_order α] [linear_order N] [has_zero N] : linear_order (α →₀ N) :=

where f < g if f ≠ g and

• either f = 0, or
• the smallest a : α where f a ≠ g a satisfies f a < g a.

This is essentially a lex-order, but I was not able to find it in the lex files.

Thanks!

[Alex J. Best]

One observation: it might be convenient to define this as the pullback of the lex order on functions under the embedding of funsupps into functions

[Yaël Dillies]

I don't see why you need the f = 0 case.

[Damiano Testa]

The 0 case was only to be able to talk about the "smallest ...".

[Damiano Testa]

Anyway, I have tried getting the functions to work, but I might be missing some imports.

[Yaël Dillies]

Still it doesn't seem like you need it. If f is minimal, then the smallest a will respect f a < g a (because g a < f a would be contradictory.

[Yaël Dillies]

Also, you will need N to be well-ordered for the minimal a to even exist.

[Yaël Dillies]

docs#pi.lex.linear_order

[Damiano Testa]

If you do not need to split that case, that is fine as well. I was just worried that applying f to a would cause problems is a was the bottom of with_bot α.

[Damiano Testa]

Is well-ordering necessary, since I am always dealing with finsupps?

[Damiano Testa]

What I mean is that the minimal a can be chosen in the union of the supports of f and g.

[Damiano Testa]

I'll try with docs#pi.lex.linear_order and see how far I get, thanks!

[Yaël Dillies]

Oh yeah, maybe not. In that case you can pull back the order from pi.lex, but not its linearity, so you will need to prove that separately.

[Yaël Dillies]

This brings up a lot of memory, so I wonder whether I didn't try implementing this for Shing and his Gröbner bases somewhere.

[Yaël Dillies]

I think I didn't, so please go ahead

[Damiano Testa]

Ok, so pi.lex will give me an order once I have orders on source and target, right? And you are saying that this order is linear, but this final fact is not proven?

[Damiano Testa]

Yaël Dillies said:

This brings up a lot of memory, so I wonder whether I didn't try implementing this for Shing and his Gröbner bases somewhere.

This makes lots of sense to me, since I am thinking about this in the context of add_monoid_algebras.

[Damiano Testa]

Yaël, you are suggesting this, correct?

def finsupp.lex {α N} [linear_order α] [linear_order N] [has_zero N] : linear_order (α →₀ N) :=
{ le := λ f g, pi.lex (≤) (λ _, (≤)) f g,
  lt := _,
  le_refl := _,
  le_trans := _,
  lt_iff_le_not_le := _,
  le_antisymm := _,
  le_total := _,
  decidable_le := _,
  decidable_eq := _,
  decidable_lt := _,
  max := _,
  max_def := _,
  min := _,
  min_def := _ }

[Yaël Dillies]

You can get at least partial_order for free: docs#partial_order.lift

[Damiano Testa]

Ah, great! I was having problems proving reflexivity! With your suggestion, I can probably make it to the end!

I'll let you know if I need more help, but I will get back to this in an hour or so.

Thanks!

[Yaël Dillies]

You can get lattice from defining sup and inf and then using docs#function.injective.lattice.

[Yaël Dillies]

So you'll only to prove totality afterwards

[Alex J. Best]

import data.pi.lex
import order.synonym
import data.finsupp.order
.

noncomputable
instance {α N} [linear_order α] [is_well_order α (<)] [linear_order N] [has_zero N] :
  linear_order (lex (α →₀ N)) :=
linear_order.lift' _ (@id (function.injective (_ : lex (α →₀ N) → lex (α → N))) finsupp.coe_fn_injective)
example : (to_lex (finsupp.single 1 1) : lex (ℕ →₀ ℕ)) ≤ to_lex (finsupp.single 1 1) :=
begin
  simp,
end

[Yaël Dillies]

And now try getting rid of is_well_order :stuck_out_tongue:

[Alex J. Best]

For Damiano I would imagine alpha is fin n or something anyways

[Yaël Dillies]

I suspect it might be int

[Damiano Testa]

Alex, I would prefer to leave α arbitrary, but fin n is one of the main players.

Yaël, N is likely to be ℕ or ℤ, depending on whether I'm thinking of polynomials or Laurent polynomials.

[Damiano Testa]

Anyway, thank you both! I'll see what I can do with the well-order wrinkle!

[Damiano Testa]

Can you tell that I do not know my way around the lex API?

import data.pi.lex
import data.finsupp.basic

instance {α N} [linear_order α] [partial_order N] [has_zero N] :
  partial_order (lex (α →₀ N)) :=
partial_order.lift _ (@id (function.injective (_ : lex (α →₀ N) → lex (α → N)))
  finsupp.coe_fn_injective)

lemma ne_or_ne_of_ne {α} {a b : α} (c : α) (ab : a ≠ b) :
  a ≠ c ∨ b ≠ c :=
begin
  by_cases ac : a = c,
  { exact or.inr (ne_of_ne_of_eq ab.symm ac) },
  { exact or.inl ac },
end

open_locale classical

noncomputable def finsupp.lex {α N} [linear_order α] [linear_order N] [add_zero_class N] :
  linear_order (lex (α →₀ N)) :=
{ le_total := λ f g, begin
  let dfug : finset α := (f.support ∪ g.support).filter (λ a, of_lex f a ≠ of_lex g a),
  by_cases de : dfug = ∅,
  { refine or.inl (le_of_eq _),
    ext a,
    refine not_ne_iff.mp (λ h, not_ne_iff.mpr de _),
    refine finset.ne_empty_of_mem (_ : a ∈ _),
    simp only [ne.def, finset.mem_filter, finset.mem_union, finsupp.mem_support_iff],
    exact ⟨ne_or_ne_of_ne _ h, h⟩ },
  { rw [← ne.def, ← finset.nonempty_iff_ne_empty] at de,
    let min : α := dfug.min' de,
    by_cases mf : of_lex f min ≤ of_lex g min,
    { refine or.inl (or.inr _),
      rcases finset.mem_filter.mp (finset.min'_mem _ de) with ⟨-, h⟩,
      refine ⟨min, λ j hj, _, lt_of_le_of_ne mf h⟩,
      by_cases js : j ∈ f.support ∪ g.support,
      { contrapose! hj,
        exact finset.min'_le _ _ (finset.mem_filter.mpr ⟨js, hj⟩) },
      { simp only [finset.mem_union, ne.def, not_or_distrib, finsupp.mem_support_iff, not_not] at js,
        simp only [js] } },
    { refine or.inr (or.inr ⟨min, λ j hj, _, not_le.mp mf⟩),
      by_cases js : j ∈ f.support ∪ g.support,
      { contrapose! hj,
        exact finset.min'_le _ _ (finset.mem_filter.mpr ⟨js, hj.symm⟩) },
      { simp only [finset.mem_union, ne.def, not_or_distrib, finsupp.mem_support_iff, not_not] at js,
        simp only [js] } } }
    end,
  decidable_le := infer_instance,
  decidable_eq := infer_instance,
  decidable_lt := infer_instance,
  ..(infer_instance : partial_order (lex (α →₀ N))) }

[Yaël Dillies]

I will have a go at it myself when I have access to a computer

[Damiano Testa]

Should I make a PR about this or is it too niche? :upside_down:

[FR]

It may be helpful to prove is_domain (add_monoid_algebra R (σ → ₀ G)), which can be used in the proof of the Lindemann-Weierstrass theorem. Otherwise it needs a copy of mv_polynomial.is_domain.

[Damiano Testa]

Yes, my goal is to prove no_zero_divisors on add_monoid_algebras in as much a generality as I can.

[Damiano Testa]

I already have a proof with enough covariant assumptions on the grading type. Now I'd like to make sure that these assumptions are unneeded!

[Damiano Testa]

I opened two PRs:

• #15983, where there are results about non-zero divisors in add_monoid_algebras,
• #15984, where there is the proof above that finsupps can be linearly ordered.

Any comments on these PRs are very welcome! In particular, if you have a use-case in mind for either the linear extensions or the non-existence of zero-divisors, I would be happy to hear about them and try to improve/generalize as needed!

Thanks!