[Merged by Bors] - feat(Polynomial): polynomial sequences are bases for R[X] by Julian · Pull Request #20846 · leanprover-community/mathlib4

Julian · 2025-01-19T15:52:02Z

We define polynomial sequences -- that is, sequences of polynomials where the ith polynomial has degree i.

We do not yet refactor any existing polynomial sequences to go via this proof (e.g. for the usual monomial basis which has its own proof already in Mathlib).

Co-authored-by: Aaron Hill aa1ronham@gmail.com
Co-authored-by: Julian Berman Julian@GrayVines.com
Co-authored-by: Matej Penciak matej.penciak@gmail.com
Co-authored-by: Austin Letson waustinletson@gmail.com

We do not yet refactor any existing polynomial sequences to go via this proof (e.g. for the monomial basis). Co-authored-by: Julian Berman <Julian@GrayVines.com> Co-authored-by: Matej Penciak <matej.penciak@gmail.com> Co-authored-by: Austin Letson <waustinletson@gmail.com>

github-actions · 2025-01-19T15:52:58Z

PR summary 1f8bcb55bd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Polynomial.Sequence` (new file)	1022

Declarations diff

+ Sequence
+ basis
+ basis_degree_strictMono
+ basis_eq_self
+ basis_natDegree_strictMono
+ coeFun
+ degree_eq
+ degree_smul_of_isRightRegular_leadingCoeff
+ degree_strictMono
+ linearIndependent
+ natDegree_eq
+ natDegree_strictMono
+ ne_zero
+ span

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Ruben-VandeVelde

Thanks!

Ruben-VandeVelde · 2025-01-20T16:28:20Z

+
+/-- Polynomials in a polynomial sequence are linearly independent. -/
+lemma linearIndependent [NoZeroDivisors R] :
+    LinearIndependent R S := linearIndependent_iff'.mpr <| fun s g eqzero i hi ↦ by


This proof doesn't immediately generalize, but is this true over semirings?

I wasn't sure, and I saw lots of the linear independence API being generalized the last few weeks to Semirings. I'll look again to see if perhaps now I can find something that works.

I discussed the question with a friend today and our conclusion is that this will only be true over semirings which have injective addition, i.e. a + b = a + c -> b = c (this would be AddCancelCommMonoid). Counter-example: if a + c = b + c but a ≠ b, you have a • 1 + c • (1 + X) = b • 1 + c • (1 + X) while a ≠ b. In the case of an AddCancelCommMonoid it will be true since the space of polynomials will also be an AddCancelCommMonoid. This in particular covers the case of ℕ. However I did not find a typeclass in Mathlib to talk about such semirings, so I would say that the way to go here is to write a TODO mentioning the missing typeclass (if it is missing, maybe it would be nice to open a Zulip thread to make sure).

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

* origin/master: (294 commits) feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084) feat: separating set in the category of ind-objects (#21082) feat: derivWithin lemmas (#21092) chore(Fintype): golf a proof (#21113) chore: golf using `funext₂` (#21106) chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101) doc(ComputeDegree): typos (#21095) ...

…ion.

Julian · 2025-02-21T19:00:12Z

I believe I've covered all the suggestions @EtienneC30, thanks for all the tips! And asked on Zulip about the last remaining generalization (which I've added a TODO for).

pechersky · 2025-02-21T19:22:03Z

Results about injectivity and lt on degree and natDegree can likely be stated as StrictMono. There is a StrictMono.injective.

Julian · 2025-02-21T19:36:04Z

Ah, nice! Done as well.

EtienneC30 · 2025-02-22T16:12:46Z

Thanks!
maintainer merge

github-actions · 2025-02-22T16:13:07Z

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

jcommelin

Thanks!

bors d+

mathlib-bors · 2025-02-24T08:35:28Z

✌️ Julian can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Julian · 2025-02-24T15:38:47Z

bors r+

We define [polynomial sequences](https://en.wikipedia.org/wiki/Polynomial_sequence) -- that is, sequences of polynomials where the `i`th polynomial has degree `i`. We do not yet refactor any existing polynomial sequences to go via this proof (e.g. for the usual monomial basis which has its own proof already in Mathlib). Co-authored-by: Aaron Hill <aa1ronham@gmail.com> Co-authored-by: Julian Berman <Julian@GrayVines.com> Co-authored-by: Matej Penciak <matej.penciak@gmail.com> Co-authored-by: Austin Letson <waustinletson@gmail.com> Co-authored-by: Aaron Hill <aa1ronham@gmail.com>

mathlib-bors · 2025-02-24T16:42:04Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: feat(Polynomial): polynomial sequences are bases for R[X] (#20846) feat: monoidal structure on Hopf algebras (#12011) feat(DiscreteValuationRing): addVal_eq_zero_iff (#21154) refactor(Cache): refactor getPackageDir to not use manually provided package directories (#21817) feat(CategoryTheory): categories of homological complexes have a separator (#20229) chore(Data/Complex): deprecate `Complex.abs` (#21995) feat: uncountable instances for `Ordinal` and isomorphic types (#18547) feat(Data/Set/Card): a few missing lemmas (#22186) feat: discrete topological spaces are 0-manifolds (#22105) feat(Data/Matroid/Loop): matroid loops (#22045) feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162) feat(Data/Matroid/Circuit): matroid cocircuits (#21692) feat(Topology/Compactification/OnePoint): generalize instance (#22179) feat(Combinatorics/SimpleGraph): takeUntil properties (#21250) feat(Tactic): `pnat_to_nat` and `enat_to_nat` tactics (#21602) refactor: move `Polynomial.coeffs` and related results (#22225) chore: add AlgHom.ker_coe_equiv, resolve porting notes and erws (#22019) refactor(Order/Category): `ConcreteCategory` instance for `\omegaCPO` (#21478) feat(CategoryTheory): Grothendieck categories have a coseparator (#22224) feat: tweak calc widget (#22170) feat(CategoryTheory): the Freyd-Mitchell embedding theorem (#22222) chore(CategoryTheory): turn more `simp` into `simps!` (#22223) feat(CategoryTheory): the category of ind-objects is Grothendieck abelian (#21606) feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` (#21743) chore(CategoryTheory/DiscreteCategory): turn `simp` to `simps!` (#22217) feat(Analysis/Asymptotics): exponential growth of a sequence (#21178) feat(CategoryTheory): sigmaConst preserves monomorphisms (#21599) feat(RingTheory/Cotangent): `liftBaseChange` is injective for localizations (#21037) chore(CategoryTheory): fix incorrect name (#22210) feat(CategoryTheory): `IsPullback` version of 'pullback of iso is iso' (#22211) feat(CategoryTheory): pullbacks in functor categories (#22209) feat(CategoryTheory): detecting limit cones over connected diagrams (#22192) feat(LinearAlgebra): add theorems for injective/surjective/bijective compositions of bilinear maps (#21491)

We define [polynomial sequences](https://en.wikipedia.org/wiki/Polynomial_sequence) -- that is, sequences of polynomials where the `i`th polynomial has degree `i`. We do not yet refactor any existing polynomial sequences to go via this proof (e.g. for the usual monomial basis which has its own proof already in Mathlib). Co-authored-by: Aaron Hill <aa1ronham@gmail.com> Co-authored-by: Julian Berman <Julian@GrayVines.com> Co-authored-by: Matej Penciak <matej.penciak@gmail.com> Co-authored-by: Austin Letson <waustinletson@gmail.com> Co-authored-by: Aaron Hill <aa1ronham@gmail.com>

Aaron1011 and others added 12 commits January 18, 2025 21:47

Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out

997024e

Copyright header and more twiddling.

0a54e80

Remove redundant imports.

db07c84

Quiet linters.

89f7d13

More

7ce6683

Bit shorter.

799c02e

Does protected satisfy the docstring linter?

8a435c6

Touch more natDegree.

8933d58

Kill more temporary names.

b13ebeb

Probably enough initial tidying to send the PR.

164eb8c

Try satisfying the linter gods again.

d7a6ec4

github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 19, 2025

Julian added 3 commits January 19, 2025 10:58

Aha, here's how to get Lean to stop showing S.elems' in the infoview.

bb94214

Don't quash span with the namespace open, and more minor tidying.

96f9cad

One more.

bab5332

EtienneC30 reviewed Jan 20, 2025

View reviewed changes

Comment thread Mathlib/Algebra/Polynomial/Sequence.lean Outdated

Ruben-VandeVelde reviewed Jan 20, 2025

View reviewed changes

Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 20, 2025

Apply suggestions from code review

0fc1a7d

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Julian force-pushed the polynomial-sequences branch from 48fce04 to 0fc1a7d Compare January 20, 2025 21:56

Julian added 8 commits January 20, 2025 19:40

Add an injectivity lemma as well.

4f5e526

= top rather than the le business.

0ab41dd

Add the suggested basis API lemma.

2ab0778

More basis API and flag the lemma we really need.

a2fcb37

Revert accidental whitespace change.

935b143

And the natDegree version.

3de084c

Back to sorry free.

a3809e2

Julian added 5 commits February 21, 2025 10:45

Fix the empty docstring.

1773d00

Hopefully more correct injectivity lemmas matching the naming convent…

6cc45c3

…ion.

nontiviality to simplify this proof, and some dedenting.

fe1f27a

Same injectivity twiddling for basis.

1d8e6a2

One more dedent.

7e58df2

Mention the TODO on li generalization to semirings.

4626ccb

Julian removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 21, 2025

Julian added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 21, 2025

Talk about strict monotonicity instead, thanks @pechersky.

fb1594b

Julian removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 21, 2025

Correct the TODO to mention IsCancelAdd which does exist.

4f2e17f

github-actions Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 22, 2025

jcommelin reviewed Feb 24, 2025

View reviewed changes

Comment thread Mathlib/Algebra/Polynomial/Sequence.lean

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 24, 2025

Comments instead of blank space!

1f8bcb5

mathlib-bors Bot changed the title ~~feat(Polynomial): polynomial sequences are bases for R[X]~~ [Merged by Bors] - feat(Polynomial): polynomial sequences are bases for R[X] Feb 24, 2025

mathlib-bors Bot closed this Feb 24, 2025

mathlib-bors Bot deleted the polynomial-sequences branch February 24, 2025 16:42

Uh oh!

Conversation

Julian commented Jan 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jan 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 1f8bcb55bd

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Ruben-VandeVelde Jan 20, 2025

Choose a reason for hiding this comment

Uh oh!

Julian Jan 20, 2025

Choose a reason for hiding this comment

Uh oh!

EtienneC30 Feb 21, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Julian commented Feb 21, 2025

Uh oh!

pechersky commented Feb 21, 2025

Uh oh!

Julian commented Feb 21, 2025

Uh oh!

EtienneC30 commented Feb 22, 2025

Uh oh!

github-actions Bot commented Feb 22, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors Bot commented Feb 24, 2025

Uh oh!

Julian commented Feb 24, 2025

Uh oh!

mathlib-bors Bot commented Feb 24, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Julian commented Jan 19, 2025 •

edited

Loading

github-actions Bot commented Jan 19, 2025 •

edited

Loading