feat(RingTheory/HopfAlgebra): Hopf algebra structure on polynomials (𝔾ₐ)#39410
feat(RingTheory/HopfAlgebra): Hopf algebra structure on polynomials (𝔾ₐ)#39410RaggedR wants to merge 15 commits into
Conversation
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 02512ac5cbImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
Hello, could you disclose usage of AI, if any, according to the guideline? In particular
Could you write the PR description yourself, following the existing template? |
|
*Edit: Sorry, I originally sent this by email and didn't realize I was supposed to leave a comment directly.*
I've fixed the PR description. Sorry about that.
This work is the beginning of a formalization of the first half of my masters thesis.
https://arxiv.org/abs/0907.3950
In particular we look at the ring of polynomials in a single variable with the usual multiplication and coproduct given by: Δ(X) = X ⊗ 1 + 1 ⊗ X. The counit is evaluation at zero, and the antipode is S(x) = -x
Claude Code was used extensively in the development of the Lean proofs, however the mathematics itself comes from my masters thesis (and is well known).
This is a first step towards an implementation of the umbral calculus of Gian-Carlo Rota and then its generalization to Symmetric Functions (which I believe is original)
|
wwylele
left a comment
wwylele
left a comment
There was a problem hiding this comment.
I know little in this field, so just based on my naive code search: is this the same construction as the existing AddMonoidAlgebra.instHopfAlgebra? And if so, given Polynomial is defined over AddMonoidAlgebra, can we transfer the result? (I have also heard of a plan to make Polynomial an abbrev of AddMonoidAlgebra, which means it will automatically get these instances.
| instance instCoalgebra : Coalgebra R R[X] := | ||
| { instCoalgebraStruct R with | ||
| rTensor_counit_comp_comul := by | ||
| rw [counit_eq, comul_eq, rTensor_counit_eq, mk_one_eq_includeRight] |
There was a problem hiding this comment.
I think Mathlib prefers the newer where style
| rw [counit_eq, comul_eq, rTensor_counit_eq, mk_one_eq_includeRight] | |
| instance instCoalgebra : Coalgebra R R[X] where | |
| -- __ := instCoalgebraStruct R -- This line should be unnecessary as Lean should find the base struct, but in case it errors you can add it | |
| rTensor_counit_comp_comul := by |
This comment was marked as low quality.
This comment was marked as low quality.
|
AI disclosure: this PR was developed with assistance from Claude Code. The |
SnirBroshi
added
the
LLM-generated
|
LLM-generated |
@RaggedR, note that, as per the contribution guidelines https://leanprover-community.github.io/contribute/index.html#use-of-ai, you need to use your own words in comments in GitHub and messages in Zulip; using an LLM for comments is not allowed.
You haven't fixed this. |
| comul := (comulAdditiveAlgHom R).toLinearMap | ||
| counit := (counitAdditiveAlgHom R).toLinearMap |
There was a problem hiding this comment.
Instead of adding the comulAdditiveAlgHom and counitAdditiveAlgHom definitions above, can you just do the following instead?
| comul := (comulAdditiveAlgHom R).toLinearMap | |
| counit := (counitAdditiveAlgHom R).toLinearMap | |
| comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap | |
| counit := (Polynomial.aeval (0 : R)).toLinearMap |
And then use counit and comul for the above theorems (you'd obviously need to move the theorems after this instance).
| theorem mk_one_eq_includeRight : | ||
| TensorProduct.mk R R R[X] 1 = | ||
| (Algebra.TensorProduct.includeRight : R[X] →ₐ[R] R ⊗[R] R[X]).toLinearMap := by | ||
| ext y; simp [Algebra.TensorProduct.includeRight_apply] | ||
|
|
||
| theorem mk_flip_one_eq_includeLeft : | ||
| (TensorProduct.mk R R[X] R).flip 1 = | ||
| (Algebra.TensorProduct.includeLeft : R[X] →ₐ[R] R[X] ⊗[R] R).toLinearMap := by | ||
| ext y; simp [Algebra.TensorProduct.includeLeft_apply, LinearMap.flip_apply] |
There was a problem hiding this comment.
These are in the wrong way around and should go in an earlier file.
theorem Algebra.TensorProduct.toLinearMap_includeRight {R A B} [CommSemiring R] [Semiring A]
[Algebra R A] [Semiring B] [Algebra R B] :
(Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B).toLinearMap =
TensorProduct.mk R A B 1 := rfl
theorem Algebra.TensorProduct.toLinearMap_includeLeft
{R A B} [CommSemiring R] [Semiring A]
[Algebra R A] [Semiring B] [Algebra R B] [Algebra R A] :
(Algebra.TensorProduct.includeLeft : A →ₐ[R] A ⊗[R] B).toLinearMap =
(TensorProduct.mk R A B).flip 1 := rfl
themathqueen
added
the
awaiting-author
2371a6e to
41f1663
Compare
|
Thankyou Monica for taking the time to review my PR. In summary: Polynomial.lean — the big diff removes comulAdditiveAlgHom, counitAdditiveAlgHom, instCoalgebraStruct, comul_eq, counit_eq, mk_one_eq_includeRight, mk_flip_one_eq_includeLeft, and all the specific rTensor_counit_eq/lTensor_counit_eq/rTensor_comul_eq/lTensor_comul_eq lemmas. Replaces them with two generic private glue lemmas (rTensor_toLinearMap_eq/lTensor_toLinearMap_eq) and a single where-style instCoalgebra with everything inlined. Simp lemmas now use Coalgebra.comul/Coalgebra.counit and change to unfold through the instance. You can probably tell that much of this work was generated by Claude using my thesis as a "prompt" https://arxiv.org/abs/0907.3950 In some cases Claude has "brute forced" the proofs rather than using the theory to prove them. I didn't realize this at first but am working on fixing it now. (This applies to upstream PRs more so than this one, particularly the graph theory examples) I am new to Lean so thankyou again for your patience. |
8286571 to
c5c7470
Compare
github-actions
Bot
added
the
merge-conflict
|
Please add the |
|
@RaggedR, can you please fix the git history? I'm not sure what you did.
This is already applied. And I have already explained how to add this yourself. |
|
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 |
c5c7470 to
b02f79a
Compare
github-actions
Bot
removed
the
merge-conflict
…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.
…earMap lemmas
Address review feedback:
- Remove comulAdditiveAlgHom/counitAdditiveAlgHom as standalone defs,
inline aeval expressions directly in the Coalgebra instance
- Use where style for instCoalgebra instead of { ... with }
- Add Algebra.TensorProduct.toLinearMap_includeRight/Left as rfl lemmas
in TensorProduct/Basic.lean, replacing the reversed mk_one_eq lemmas
- State simp lemmas in terms of Coalgebra.comul/counit after the instance
Separate CoalgebraStruct from Coalgebra instance and add comul_def, counit_def, comul_apply, counit_apply lemmas. This eliminates all `change` tactics in favour of `rw`/`simp` with the new API lemmas.
The private rTensor_toLinearMap_eq and lTensor_toLinearMap_eq lemmas
need explicit {A : Type*} [CommSemiring A] [Algebra R A] parameters
since they are no longer under a variable block that provides these.
Separate CoalgebraStruct from Coalgebra, add comulAlgHom/counitAlgHom as named definitions, and provide comul_def/counit_def/comul_apply/ counit_apply API lemmas. All proofs verified with lake build.
f69ca96 to
2572d75
Compare
github-actions
Bot
removed
the
large-import
| comul := (comulAlgHom R).toLinearMap | ||
| counit := (counitAlgHom R).toLinearMap |
There was a problem hiding this comment.
Just please inline these instead of having them as separate definitions:
| comul := (comulAlgHom R).toLinearMap | |
| counit := (counitAlgHom R).toLinearMap | |
| comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap | |
| counit := (Polynomial.aeval (0 : R)).toLinearMap |
|
Please merge master |
GitHub Actions
Inactive
|
Done — merged master and inlined the comul/counit definitions in the CoalgebraStruct instance. The named comulAlgHom/counitAlgHom defs have been removed since the Lean 4.31 module system requires exported rfl theorems to resolve without unfolding intermediate definitions. |
I don't understand. I suggested you inline them because there was no point in having them as separate definitions. |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
|
You're right — I overcomplicated the explanation. They were unnecessary as separate definitions, as you said. I've merged master to resolve the conflicts. |
github-actions
Bot
removed
the
merge-conflict
| theorem comul_apply (p : R[X]) : | ||
| Coalgebra.comul (R := R) p = | ||
| Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])) p := rfl | ||
|
|
||
| theorem counit_apply (p : R[X]) : | ||
| Coalgebra.counit (R := R) p = Polynomial.aeval (0 : R) p := rfl |
There was a problem hiding this comment.
If you make both these simp lemmas, then you wouldn't need comul_X, comul_C, counit_X, counit_C.
| rw [rTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap, | ||
| ← AlgebraTensorModule.mk_eq, ← Algebra.TensorProduct.toLinearMap_includeRight] | ||
| congr 1; apply Polynomial.algHom_ext | ||
| simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply] |
There was a problem hiding this comment.
these two are already simp lemmas, you don't need them here
| simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply] | |
| simp |
| dsimp only [Coalgebra.comul, CoalgebraStruct.comul] | ||
| rw [rTensor_toLinearMap_eq, lTensor_toLinearMap_eq] |
There was a problem hiding this comment.
you already have comul_def so use it
| dsimp only [Coalgebra.comul, CoalgebraStruct.comul] | |
| rw [rTensor_toLinearMap_eq, lTensor_toLinearMap_eq] | |
| rw [comul_def, rTensor_toLinearMap_eq, lTensor_toLinearMap_eq] |
| simp only [← C_mul_X_pow_eq_monomial, map_mul, map_pow, aeval_X, aeval_C] | ||
| have hassoc : ∀ x, (TensorProduct.assoc R R[X] R[X] R[X]) x = | ||
| (Algebra.TensorProduct.assoc R R R[X] R[X] R[X] R[X]) x := fun _ => rfl | ||
| simp only [hassoc, map_mul, map_pow] | ||
| congr 1 | ||
| · simp [Algebra.TensorProduct.one_def, | ||
| Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul'] | ||
| · congr 1 | ||
| simp only [aeval_X, map_add, Algebra.TensorProduct.map_tmul, AlgHom.id_apply, | ||
| map_one, Algebra.TensorProduct.assoc_tmul, | ||
| Algebra.TensorProduct.one_def, TensorProduct.add_tmul, TensorProduct.tmul_add] | ||
| abel |
There was a problem hiding this comment.
| simp only [← C_mul_X_pow_eq_monomial, map_mul, map_pow, aeval_X, aeval_C] | |
| have hassoc : ∀ x, (TensorProduct.assoc R R[X] R[X] R[X]) x = | |
| (Algebra.TensorProduct.assoc R R R[X] R[X] R[X] R[X]) x := fun _ => rfl | |
| simp only [hassoc, map_mul, map_pow] | |
| congr 1 | |
| · simp [Algebra.TensorProduct.one_def, | |
| Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul'] | |
| · congr 1 | |
| simp only [aeval_X, map_add, Algebra.TensorProduct.map_tmul, AlgHom.id_apply, | |
| map_one, Algebra.TensorProduct.assoc_tmul, | |
| Algebra.TensorProduct.one_def, TensorProduct.add_tmul, TensorProduct.tmul_add] | |
| abel | |
| have hassoc : ∀ x, (TensorProduct.assoc R R[X] R[X] R[X]) x = | |
| (Algebra.TensorProduct.assoc R R R[X] R[X] R[X] R[X]) x := fun _ => rfl | |
| simp [← C_mul_X_pow_eq_monomial, hassoc, Algebra.TensorProduct.one_def, TensorProduct.add_tmul, | |
| TensorProduct.tmul_add, add_assoc] |
Make comul_apply and counit_apply @[simp], removing the now-redundant comul_X, comul_C, counit_X, counit_C lemmas. Simplify coalgebra proofs to use comul_def/counit_def and bare simp. Consolidate the coassoc monomial case.
4 participants
This is the beginning of a formalization of the first half of my masters thesis (https://arxiv.org/abs/0907.3950).
In particular we look at the ring of polynomials in a single variable with the usual multiplication and coproduct given by: Δ(X) = X ⊗ 1 + 1 ⊗ X. The counit is evaluation at zero, and the antipode is S(x) = -x.
The mathematics itself comes from my masters thesis (and is well known). This is a first step towards an implementation of the umbral calculus of Gian-Carlo Rota and then its generalization to Symmetric Functions (which I believe is original).
LLM tools were used to assist with Lean formalization. The mathematical content is the author's own work.