feat(RingTheory/HopfAlgebra): ascending Pochhammer is of binomial type#39636
feat(RingTheory/HopfAlgebra): ascending Pochhammer is of binomial type#39636RaggedR wants to merge 14 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. |
|
maintainer merge Could a maintainer please add the |
PR summary 6cf2ceee25
|
| Files | Import difference |
|---|---|
Mathlib.RingTheory.HopfAlgebra.Lah (new file) |
1205 |
Mathlib.RingTheory.HopfAlgebra.Polynomial (new file) |
1228 |
Mathlib.RingTheory.HopfAlgebra.BinomialType (new file) |
1231 |
Mathlib.RingTheory.HopfAlgebra.DeltaOperator (new file) |
1341 |
Mathlib.RingTheory.HopfAlgebra.AscPochhammer (new file) |
1342 |
Declarations diff
+ IsBasicSequence
+ IsBasicSequence.isBinomialType
+ IsBinomialType
+ IsBinomialType.comp_coalgebraHom
+ IsBinomialType.comul_zero
+ IsBinomialType.of_coalgebraHom
+ IsDeltaOperator
+ IsShiftEquivariant
+ X_pow_isBasicSequence
+ X_pow_isBinomialType
+ aeval_C_eq_C_eval
+ antipodeAdditiveAlgHom
+ antipodeAdditiveAlgHom_C
+ antipodeAdditiveAlgHom_X
+ ascPochhammer_isBasicSequence_backwardDiff
+ ascPochhammer_isBinomialType
+ backwardDiff
+ backwardDiff_C
+ backwardDiff_X
+ backwardDiff_apply
+ backwardDiff_ascPochhammer
+ backwardDiff_isDeltaOperator
+ backwardDiff_isShiftEquivariant
+ coeff_lahSeries_pow
+ coeff_lahSeries_pow_succ
+ coeff_taylor_sub_eq
+ comulAdditiveAlgHom
+ comulAdditiveAlgHom_C
+ comulAdditiveAlgHom_X
+ comul_X_sub_natCast
+ comul_eq
+ comul_taylor_bridge
+ counitAdditiveAlgHom
+ counitAdditiveAlgHom_C
+ counitAdditiveAlgHom_X
+ counit_eq
+ delta_ker_eval_zero
+ delta_op_Q_X_eq_C
+ derivative_isDeltaOperator
+ descPochhammer_isBasicSequence_forwardDiff
+ descPochhammer_isBinomialType
+ descPochhammer_mul_X
+ descPochhammer_mul_X_sub
+ eval_determines
+ eval_tensor_zero
+ forwardDiff
+ forwardDiff_C
+ forwardDiff_X
+ forwardDiff_apply
+ forwardDiff_isDeltaOperator
+ forwardDiff_isShiftEquivariant
+ forwardDiff_one_descPochhammer
+ hasseDeriv_isShiftEquivariant
+ instBialgebra
+ instCoalgebra
+ instCoalgebraStruct
+ instHopfAlgebra
+ instTorsionFree
+ isShiftEquivariant_add
+ isShiftEquivariant_comp
+ lTensor_comul_eq
+ lTensor_counit_eq
+ lahSeries
+ lahSeries_pow
+ mk_flip_one_eq_includeLeft
+ mk_one_eq_includeRight
+ natDegree_Q_of_bounded
+ natDegree_delta_op_pow
+ natDegree_taylor_sub_le
+ rTensor_comul_eq
+ rTensor_counit_eq
+ sum_hasseDeriv_eq_zero
+ summand_identity
+ taylor_basic_eq
+ taylor_invariant_eq_C
+ taylor_neg_one_ascPochhammer_succ
+ taylor_one_X_sub_natCast
+ taylor_one_mul
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
No changes to strong technical debt.
No changes to weak technical debt.
…lling factorials)
You can add the label by commenting |
|
Also, when you add "depends on: prnumber" in the description, please add it below the I've edited the description for you here, but you should do them for the rest of your PRs. |
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
The `intro` tactic cannot see through the `IsShiftEquivariant` definition when it is imported from another module. Adding an explicit `unfold` makes the proof robust to cross-module reducibility.
`unfold` fails on applied definitions in Lean 4.30; `delta` forces definitional unfolding regardless of reducibility.
|
LLM-generated |
github-actions
Bot
added
the
LLM-generated
Both `intro`, `unfold`, and `delta` fail to see through IsShiftEquivariant across module boundaries in Lean 4.30. `simp only` with the definition name forces unfolding.
`intro`, `unfold`, `delta`, and `simp only` all fail to see through IsShiftEquivariant across module boundaries in Lean 4.30. Term-mode `fun a =>` directly provides the argument without needing to unfold the definition.
Lean 4.30's module system makes definitions unexposed by default. `@[expose] public section` is needed for definitions like IsShiftEquivariant to be unfoldable by tactics and term-mode unification across module boundaries.
With @[expose], simp can already prove these from the definition, making the @[simp] tags redundant (linter error).
RaggedR
force-pushed
the
feat/ascpochhammer-binomial
branch
from
b7a041d to
6cf2cee
Compare
|
Please add the |
2 participants
This adds two concrete examples to the delta operator framework from #39465, illustrating the change of basis between the two classical families of binomial-type sequences beyond the monomials.
The first file proves that the ascending Pochhammer (rising factorial) sequence is of binomial type. The backward difference operator ∇f(x) = f(x) − f(x−1) is defined, shown to be a delta operator, and the ascending Pochhammer sequence is verified as its basic sequence via a telescoping argument. The final theorem
ascPochhammer_isBinomialTypeis a one-line application of Rota's classification from #39465, complementing the existingdescPochhammer_isBasicSequence_forwardDifffor falling factorials and the forward difference.The second file computes the Jabotinsky matrix entries of the geometric delta series y/(1−y), giving the unnormalized Lah numbers C(n−1, k−1) as the change-of-basis coefficients between rising and falling factorials. The proof factors the power (y/(1−y))ᵏ = Xᵏ · (1−X)⁻ᵏ and applies Mathlib's existing
mk_one_pow_eq_mk_choose_addfor the negative binomial series.