Linear independence of polynomial sequences over semirings

Stream: mathlib4

[Julian Berman]

In #20846 we define polynomial sequences and prove they are linearly independent in R[X] for R a ring. The question was asked on whether this is true in a semiring. @Etienne Marion mentioned after discussing with a friend that this seems likely true in a semiring with injective addition, but we don't seem to have an AddCancelCommSemiring class to go along with docs#AddCancelCommMonoid. I think (especially given I am nearly at the limits of what I understand personally) that for the PR we're going to leave this as a TODO regardless, but it seemed like a good suggestion to confirm that in fact that typeclass doesn't exist with some other name, and/or whether I've missed anything else obvious.

[Riccardo Brasca]

Don't we have IsAddCancel or something like that?

[Etienne Marion]

Ah indeed there is docs#IsCancelAdd !

[Etienne Marion]

The proof strategy we discussed was to use the fact that a semiring which has IsCancelAdd could be injected in a ring, which we did not check but seemed reasonable. However I'm not at all sure how this should be stated, I'll take any suggestions.

Maybe it will just be easier to do the proof "by hand", I think I'll give it a try this week-end.

[Riccardo Brasca]

Yes, this is related to the fact that the natural map from a commutative cancellative monoid to the groupification is injective. I think this is somewhere in mathlib

[Riccardo Brasca]

Anyway proving this by hand should be easy in any concrete case

[Junyan Xu]

This also arose in #maths > Linear independence over semirings @ 💬

[Etienne Marion]

Ah indeed! I had no idea there had been a recent change in the definition. I don't feel confident enough to dive in those localization questions.

[Riccardo Brasca]

The previous definition (the usual one just written for semirings) is not very interesting, since 1,2,3, ... is ℕ-linearly independent.

[Etienne Marion]

Yes but I thought the current definition had always been there

[Riccardo Brasca]

I think the current one is the same as "linear independent over the ringification" (at least for cancellative semirings)

[Riccardo Brasca]

I just made the word "ringification" up, but I mean the same construction as getting ℤ from ℕ (the should be the adjoint of the forgetful functor).

[Edward van de Meent]

for those who missed it and don't feel like searching through the previous thread, under the previous definition, a family was LinearIndependent exactly when the kernel of docs#Finsupp.linearCombination is trivial. Indeed, the kernel of taking linear combinations of Nat.succ is trivial, but taking linear combinations is not injective (which is the current definition of LinearIndependent)

[Etienne Marion]

I got

lemma linearIndependent {R : Type*} [Semiring R] [IsCancelAdd R] [IsRightCancelMulZero R]
    (S : Sequence R) : LinearIndependent R S

sorry-free! It needs some tidying though.

[Julian Berman]

Amazing. I saw your "horrible" last night :) looking forward to learning from the less-horrible version.

[Etienne Marion]

Haha yeah I had never dealt with polynomials in Mathlib before and got a little bit frustrated :sweat_smile:

[Antoine Chambert-Loir]

(Just a comment that won't help much, I fear.) This seems to be a particular case of the following situation: Starting from an R-module M with a filtration (which doesn't seem to be formalized in mathlib), that is a monotone family of submodules indexed by an ordered set, you can consider its associated graded module (direct sum of quotient of the filtered parts modulo the sum of the strictly slower ones), and you have a family in that module which induces a basis in the graded module—then it is a basis.

[Eric Wieser]

(there is an open PR about associated graded rings, and possibly also modules)

[Julian Berman]

Yeah in trying to understand Antoine's comment we found an old thread from you Eric on them :) EDIT: looks like #20913 and #20940

[Antoine Chambert-Loir]

Thanks. I'll try to review these PR.

[Jz Pan]

Antoine Chambert-Loir said:

you can consider its associated graded module (direct sum of quotient of the filtered parts modulo the sum of the strictly slower ones)

But for this particular question you only need to consider the R-module structure of this graded module, but not over any graded ring.