feat(RingTheory/HopfAlgebra): delta operators and Rota's classification#39465
feat(RingTheory/HopfAlgebra): delta operators and Rota's classification#39465RaggedR wants to merge 6 commits into
Conversation
…G_a) Add the Coalgebra, Bialgebra, and HopfAlgebra instances on `R[X]` with additive comultiplication `Δ(X) = X ⊗ 1 + 1 ⊗ X`, counit `ε(p) = p(0)`, and antipode `S(X) = -X`. This is the coordinate ring of the additive group scheme 𝔾_a, dual to the multiplicative 𝔾_m already formalized via Laurent polynomials.
Adds `module` keyword and changes `import` to `public import` to match the module system introduced in Lean 4.30.0-rc2, which Mathlib master now requires.
Add `public section` for Lean 4.30.0 module visibility and remove deprecated/unused simp lemmas (`AlgEquiv.toAlgHom_eq_coe`, `AlgHom.coe_coe`, `Algebra.TensorProduct.assoc_tmul`) flagged by linters.
Formalize the fundamental theorem of the umbral calculus: the basic sequence of any delta operator is a sequence of binomial type. New definitions: - `Polynomial.IsBinomialType`: binomial convolution for the coalgebra comultiplication - `Polynomial.IsShiftEquivariant`: commutes with Taylor shift - `Polynomial.IsDeltaOperator`: shift-equivariant, kills constants, unit leading term - `Polynomial.forwardDiff`: forward difference operator - `Polynomial.IsBasicSequence`: basic sequence of a delta operator Main results: - `Polynomial.X_pow_isBinomialType`: monomials are of binomial type - `Polynomial.descPochhammer_isBinomialType`: Vandermonde's identity - `Polynomial.IsBasicSequence.isBinomialType`: Rota's classification
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 0a15124a6fImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
bd14ac2 to
a84f277
Compare
|
As I have commented in #39410, please write the PR description yourself. There is also a specific format to follow for dependent PR |
|
Could a maintainer add the LLM-generated label please? |
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
Sorry about that — I've rewritten the PR description and added an AI
disclosure. I'm new to Mathlib contributions, still getting the hang of
the
process.
…On Sun, May 17, 2026 at 1:36 AM mathlib-dependent-issues[bot] < ***@***.***> wrote:
*mathlib-dependent-issues[bot]* left a comment
(leanprover-community/mathlib4#39465)
<#39465 (comment)>
This PR/issue depends on:
- #39410 <#39410>
By *Dependent Issues <https://github.com/z0al/dependent-issues>* (🤖).
Happy coding!
—
Reply to this email directly, view it on GitHub
<#39465 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AH2XESK5ZR4RCRSKTNJLG2T43CDGPAVCNFSM6AAAAACZASUWZSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHM2DINRXGI4DQMJSGA>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.
You are receiving this because you authored the thread.Message ID:
***@***.***>
--
*Disclaimer:*
This email and any attachments are intended solely for the use of the
individual or entity to whom they are addressed and may contain
confidential or privileged information. If you are not the intended
recipient, any disclosure, copying, distribution, or use of the information
contained herein is strictly prohibited. If you have received this email in
error, please notify the sender immediately and delete it from your system.
|
SnirBroshi
added
the
LLM-generated
|
LLM-generated |
219be5b to
0a15124
Compare
|
Please add the |
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
3 participants
This formalizes the fundamental theorem of the umbral calculus: that the basic sequence of any delta operator is a sequence of binomial type.
A delta operator on R[X] is a shift-equivariant linear operator which is essentially a formal power series in the variable d/dx. Rota's classification theorem states that the images of monomials x^n under delta operators are sequences of binomial type.
This PR defines
IsBinomialType,IsShiftEquivariant,IsDeltaOperator,forwardDiff, andIsBasicSequence. It proves that monomials and falling factorials are of binomial type, that the derivative and forward difference are delta operators, and that basic sequences are of binomial type (Rota's classification).The mathematical content is from the first half of my masters thesis (arXiv:0907.3950). See also Rota, Kahaner, and Odlyzko, Finite Operator Calculus (JMAA 42, 1973) and Roman, The Umbral Calculus (Academic Press, 1984).
Depends on #39410.
LLM tools were used to assist with Lean formalization. The mathematical content is the author's own work.