feat(Algebra/Lie/Classical): finrank of sl(n) equals n² - 1#33818
feat(Algebra/Lie/Classical): finrank of sl(n) equals n² - 1#33818JohnnyTeutonic wants to merge 7 commits intoleanprover-community:masterfrom
Conversation
PR summary 2c8f930e22
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Lie.Classical | 1533 | 1537 | +4 (+0.26%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Algebra.Lie.Classical |
4 |
Declarations diff
+ finrank_sl
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
| public import Mathlib.LinearAlgebra.Dimension.Finrank | ||
| public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas |
There was a problem hiding this comment.
Can you reorganize the imports alphabetically please?
There was a problem hiding this comment.
of course =)
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
|
Hi @alreadydone - just checking in on this PR. Let me know if there's anything you'd like me to address. Thanks! |
|
I think #Is there code for X? > lie algebra @ 💬 was working towards a proof that worked for @ocfnash, would you be happy to merge this less-general proof with a TODO comment in the docstring linking the Zulip thread? |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Unless someone needs to build on top of this result right now, I think we should not take this approach and should instead just define the standard basis with |
|
@JohnnyTeutonic I'll mark this as awaiting author until you've given feedback on my opinion here. |
ocfnash
added
the
awaiting-author
|
Thanks for the feedback @ocfnash. I'm happy to defer to your judgement here - if the standard basis approach is preferable, I'll close this and leave it for someone with more Lie algebra expertise to do properly. Let me know if you'd like me to take a crack at the basis construction instead." |
|
Thanks @JohnnyTeutonic If you want to construct the basis, then go for it. Based on the Zulip thread linked above, nobody has worked on it since since last May. I think it should be not be hard and it will have the advantage of giving a result for any coefficients, rather than just fields. |
…iagonal index
This adds a standard basis for the special linear Lie algebra sl n R
parametrized by a chosen diagonal index i. The basis consists of:
- Off-diagonal matrix units E_ij for i j
- Diagonal differences E_ii - E_{ii} for i i
The diagonal entry at i is determined by the trace-zero condition.
New definitions:
- OffDiag n: off-diagonal index pairs
- slBasisIndex i: basis index type
- slBasisFun i: basis element function
- slBasisRepr, slBasisCoord: linear maps for representation
- slBasisEquiv: linear equivalence to coordinate functions
- slBasis i: the actual basis
Closes a request from leanprover-community#33818.
5 participants
Proves
finrank R (sl n R) = Fintype.card n ^ 2 - 1using rank-nullity andMatrix.trace_surjective.