feat(mathematics): add the degree-wise linear universal property of the symmetric algebra - #1468
Conversation
Co-authored-by: ChatGPT <noreply@openai.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
|
|
||
| /-! | ||
| # Symmetric monomials and the lift out of the symmetric algebra | ||
|
|
There was a problem hiding this comment.
Is this also from a Mathlib PR, if so I think we should put right at the top of the doc-string, what PR and who the author is.
There was a problem hiding this comment.
I added the author to symmetricmap.lean as that was from a mathlib PR, this file was not from a mathlib PR though
jstoobysmith
added
the
awaiting-author
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
| variable (f : ∀ n, SymmetricMap R M N (Fin n)) | ||
|
|
||
| /-- The linear map on the tensor algebra assembled from the degreewise symmetric maps. -/ | ||
| private noncomputable def Lhat : TensorAlgebra R M →ₗ[R] N := |
There was a problem hiding this comment.
Is there an analogy for this to ExteriorAlgebra? I'm wondering about the choice of name
|
|
||
| /-- The largest ring congruence on which `Lhat f` is constant: it relates `u` and `w` when | ||
| `Lhat f (a * u * b) = Lhat f (a * w * b)` for all `a` and `b`. -/ | ||
| private def Qcon : RingCon (TensorAlgebra R M) where |
There was a problem hiding this comment.
Likewise, wondering about this choice of name.
2 participants
Adds symmetric multilinear maps, symmetric-algebra monomials, and the degree-wise linear universal property of the symmetric algebra.