feat(Algebra/Lie): grading on loop algebras

[ScottCarnahan]

In this PR we introduce a decomposition of a tensor product of modules induced by a decomposition of the module on the left side. This is used to produce the canonical "energy" grading on a loop Lie algebra. This will (eventually) give us the "energy" grading on smooth representations of affine algebras.

---

Should I make the tensor decomposition more ring-polymorphic?

• depends on: chore(LinearAlgebra/TensorProduct/Map): add symm_lTensor and symm_rTensor #41550

[github-actions]

PR summary 9560b815cc

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Lie.Loop	1590	1605	+15 (+0.94%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Lie.Loop	15

---

Declarations diff (regex)

+ coe_decomposeTensor_apply
+ decomposeLinearEquiv_comp_subtype
+ decomposeTensor
+ decomposeTensorEquiv
+ decomposeTensorEquiv_apply
+ decomposeTensorEquiv_of_apply
+ decomposeTensor_apply
+ directSumLeft_symm_of
+ instance [DecidableEq A] [AddCommMonoid A] :
+ subtype_rTensor_injective
+ symm_lTensor
+ symm_rTensor
+ tensorDecomposition

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 9560b81).

• +13 new declarations
• −0 removed declarations

+DirectSum.coe_decomposeTensor_apply
+DirectSum.decomposeLinearEquiv_comp_subtype
+DirectSum.decomposeTensor
+DirectSum.decomposeTensorEquiv
+DirectSum.decomposeTensorEquiv_apply
+DirectSum.decomposeTensorEquiv_of_apply
+DirectSum.decomposeTensor_apply
+DirectSum.subtype_rTensor_injective
+DirectSum.tensorDecomposition
+LieAlgebra.LoopAlgebra.instGradedLieAlgebraTensorProductAddMonoidAlgebraDecomposeTensorGrade
+LinearEquiv.symm_lTensor
+LinearEquiv.symm_rTensor
+TensorProduct.directSumLeft_symm_of

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 9560b815cc
Reference commit d8d7c66091

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[themathqueen]

@ScottCarnahan, can you please split this off to its own PR?

[mathlib-dependent-issues]

This PR/issue depends on:

• chore(LinearAlgebra/TensorProduct/Map): add symm_lTensor and symm_rTensor #41550
  By Dependent Issues (🤖). Happy coding!