feat(Algebra/Lie): grading on loop algebras

Mathlib/Algebra/Lie/Loop.lean

@@ -7,8 +7,11 @@ module
 
 public import Mathlib.Algebra.Group.EvenFunction
 public import Mathlib.Algebra.Lie.Cochain
+public import Mathlib.Algebra.Lie.Graded
 public import Mathlib.Algebra.Lie.InvariantForm
+public import Mathlib.Algebra.MonoidAlgebra.Grading
 public import Mathlib.Algebra.Polynomial.Laurent
+public import Mathlib.LinearAlgebra.TensorProduct.Decomposition
 
 /-!
 # Loop Lie algebras and their central extensions
@@ -70,6 +73,43 @@ def loopAlgebraEquivLaurent :
 
 namespace LoopAlgebra
 
+noncomputable instance [DecidableEq A] [AddCommMonoid A] :
+    GradedLieAlgebra (fun (a : A) ↦ (DirectSum.decomposeTensor
+      (fun b ↦ AddMonoidAlgebra.grade R b) L a)) where
+  bracket_mem i j xi xj hi hj := by
+    rw [DirectSum.decomposeTensor_apply] at hi hj ⊢
+    obtain ⟨xi, hxi⟩ := hi
+    obtain ⟨xj, hxj⟩ := hj
+    rw [← hxi, ← hxj]
+    clear hxi hxj
+    induction xi using TensorProduct.induction_on with
+    | zero => simp
+    | tmul x y =>
+      simp only [LinearMap.rTensor_tmul, Submodule.subtype_apply]
+      induction xj using TensorProduct.induction_on with
+      | zero => simp
+      | tmul u v =>
+        obtain ⟨x, hx⟩ := x
+        obtain ⟨u, hu⟩ := u
+        use ⟨x * u, SetLike.mul_mem_graded hx hu⟩ ⊗ₜ ⁅y, v⁆
+        simp
+      | add u v hu hv =>
+        rw [LinearMap.map_add, lie_add]
+        obtain ⟨u', hu'⟩ := hu
+        obtain ⟨v', hv'⟩ := hv
+        use u' + v'
+        simp [← hu', ← hv']
+    | add x y hx hy =>
+      rw [LinearMap.map_add, add_lie]
+      obtain ⟨u, hu⟩ := hx
+      obtain ⟨v, hv⟩ := hy
+      use u + v
+      simp [← hu, ← hv]
+  decompose' :=
+    (DirectSum.tensorDecomposition (fun (a : A) ↦ AddMonoidAlgebra.grade R a) L).decompose'
+  left_inv := (DirectSum.tensorDecomposition _ L).left_inv
+  right_inv := (DirectSum.tensorDecomposition _ L).right_inv
+
 open Classical in
 /-- A linear isomorphism to finitely supported functions. -/
 def toFinsupp : loopAlgebra R A L ≃ₗ[R] A →₀ L :=

Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

@@ -116,6 +116,16 @@ lemma directSumLeft_tmul (m : ⨁ i, M₁ i) (n : M₂') (i : ι₁) :
   · subst hj; simp
   · simp [DirectSum.component.of, hj]
 
+lemma directSumLeft_symm_of {i : ι₁} (x : (M₁ i) ⊗[R] M₂') :
+    (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) x) =
+      rTensor M₂' (lof S ι₁ M₁ i) x := by
+  induction x using TensorProduct.induction_on with
+  | zero => simp
+  | tmul x y =>
+    refine (LinearEquiv.symm_apply_eq (directSumLeft R S M₁ M₂')).mpr ?_
+    rw [rTensor_tmul, coe_restrictScalars, directSumLeft_tmul_lof, lof_eq_of]
+  | add x y h₁ h₂ => simp [h₁, h₂]
+
 @[simp]
 theorem directSumRight_tmul_lof (x : M₁') (i : ι₂) (y : M₂ i) :
     directSumRight R S M₁' M₂ (x ⊗ₜ[R] DirectSum.lof R _ _ i y) =

Mathlib/LinearAlgebra/TensorProduct/Decomposition.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kenny Lau
+Authors: Kenny Lau, Scott Carnahan
 -/
 module
 
@@ -10,9 +10,13 @@ public import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 
 /-! # Decomposition of tensor product
 
-In this file we show that if `ℳ` is a decomposition of an `R`-module `M` indexed by a type `ι`,
-then the `S`-module `S ⊗[R] M` has a decomposition `fun i ↦ (ℳ i).baseChange S` indexed by the
-same `ι`.
+In this file, we describe the properties of decomposition under tensor product. Suppose `ℳ` is a
+decomposition of an `R`-module `M` indexed by a type `ι`. Given an `R`-module `N`, the `R`-module
+`M ⊗[R] N` has a decomposition into pieces `fun i ↦ (ℳ i) ⊗[R] N`. Given a commutative `R`-algebra
+`S`, the `S`-module `S ⊗[R] M` has a decomposition `fun i ↦ (ℳ i).baseChange S`.
+
+## Declarations
+
 -/
 
 public section
@@ -21,13 +25,13 @@ open TensorProduct LinearMap
 
 namespace DirectSum
 
-variable {ι R M S : Type*} [DecidableEq ι]
+variable {ι R M S : Type*}
   [CommSemiring R] [AddCommMonoid M] [Module R M]
   (ℳ : ι → Submodule R M)
-  [CommSemiring S] [Algebra R S]
 
-section Decomposition
-variable [Decomposition ℳ]
+section BaseChange
+
+variable [DecidableEq ι] [Decomposition ℳ] [CommSemiring S] [Algebra R S]
 
 instance Decomposition.baseChange : Decomposition fun i ↦ (ℳ i).baseChange S := by
   refine .ofLinearMap _ (lmap (ℳ · |>.toBaseChange S) ∘ₗ
@@ -52,10 +56,84 @@ theorem toBaseChange_injective (i : ι) : Function.Injective ((ℳ i).toBaseChan
 theorem toBaseChange_bijective (i : ι) : Function.Bijective ((ℳ i).toBaseChange S) :=
   ⟨toBaseChange_injective ℳ i, (ℳ i).toBaseChange_surjective S⟩
 
-end Decomposition
+end BaseChange
+
+section TensorModule
+
+variable (N : Type*) [AddCommMonoid N] [Module R N]
+
+/-- The submodule of a tensor product corresponding to a decomposition on the left. -/
+def decomposeTensor : ι → Submodule R (M ⊗[R] N) :=
+  fun i ↦ ((ℳ i).subtype.rTensor N).range
+
+lemma decomposeTensor_apply {i : ι} :
+    decomposeTensor ℳ N i = ((ℳ i).subtype.rTensor N).range := by
+  exact Submodule.toSubMulAction_inj.mp rfl
+
+variable [DecidableEq ι] [Decomposition ℳ]
+
+lemma subtype_rTensor_injective (i : ι) :
+    Function.Injective ((ℳ i).subtype.rTensor N) :=
+  injective_of_comp_eq_id ((ℳ i).subtype.rTensor N) (((component R ι (fun i ↦ ↥(ℳ i)) i) ∘ₗ
+    (DirectSum.decomposeLinearEquiv ℳ).toLinearMap).rTensor N) (by ext; simp)
+
+/-- The linear isomorphism to the submodule from the tensor product with a summand. -/
+noncomputable def decomposeTensorEquiv (i : ι) :
+    (ℳ i) ⊗[R] N ≃ₗ[R] decomposeTensor ℳ N i :=
+  LinearEquiv.ofInjective ((ℳ i).subtype.rTensor N) (subtype_rTensor_injective ℳ N i)
+
+@[simp]
+lemma decomposeTensorEquiv_apply {i : ι} (x : (ℳ i) ⊗[R] N) :
+    decomposeTensorEquiv ℳ N i x = ((ℳ i).subtype.rTensor N) x := by rfl
+
+lemma decomposeTensorEquiv_of_apply {i : ι} (x : (ℳ i) ⊗[R] N) :
+    (congrLinearEquiv fun a ↦ decomposeTensorEquiv ℳ N a) ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) x) =
+    (of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) (decomposeTensorEquiv ℳ N i x) := by
+  ext; simp [coe_congrLinearEquiv]
+
+lemma decomposeLinearEquiv_comp_subtype {i : ι} :
+    (decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype = lof R ι (fun i ↦ ℳ i) i := by
+  ext; simp
+
+lemma coe_decomposeTensor_apply (x : (⨁ (i : ι), decomposeTensor ℳ N i)) :
+    (DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) x =
+    ((DirectSum.decomposeLinearEquiv ℳ).symm.rTensor N)
+    ((TensorProduct.directSumLeft R R (fun a ↦ ℳ a) N).symm
+      ((DirectSum.congrLinearEquiv fun a ↦ decomposeTensorEquiv ℳ N a).symm x)) := by
+  rw [← LinearEquiv.symm_rTensor, LinearEquiv.eq_symm_apply]
+  induction x using DirectSum.induction_on with
+  | zero => simp
+  | of i x =>
+    obtain ⟨x, y, h⟩ := x
+    simp only [← h, coeAddMonoidHom_of]
+    rw [LinearEquiv.eq_symm_apply, LinearEquiv.eq_symm_apply,
+      ← LinearEquiv.coe_coe (LinearEquiv.rTensor N _), LinearEquiv.coe_rTensor,
+      ← rTensor_comp_apply, decomposeLinearEquiv_comp_subtype]
+    have : (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
+        (directSumLeft R R (fun i ↦ ℳ i) N).symm ((of (fun i ↦ ℳ i ⊗[R] N) i) y) :=
+      (TensorProduct.directSumLeft_symm_of R R (M₁ := fun i ↦ ℳ i) y).symm
+    rw [this, LinearEquiv.apply_symm_apply, decomposeTensorEquiv_of_apply]
+    rfl
+  | add x y hx hy => simp [hx, hy]
+
+/-- The decomposition of a tensor product induced by a decomposition of the left module. -/
+@[reducible]
+noncomputable def tensorDecomposition (N : Type*) [AddCommGroup N] [Module R N] :
+    DirectSum.Decomposition (decomposeTensor ℳ N) where
+  decompose' x := (DirectSum.congrLinearEquiv fun a ↦ decomposeTensorEquiv ℳ N a)
+    (TensorProduct.directSumLeft R R (fun a ↦ ℳ a) N
+      ((DirectSum.decomposeLinearEquiv ℳ).rTensor N x))
+  left_inv x := by
+    simp [coe_decomposeTensor_apply ℳ N _, ← LinearEquiv.symm_rTensor]
+  right_inv x := by
+    simp [coe_decomposeTensor_apply ℳ N _, ← LinearEquiv.symm_rTensor]
+
+end TensorModule
 
 namespace IsInternal
 
+variable [DecidableEq ι] [CommSemiring S] [Algebra R S]
+
 theorem baseChange (hm : IsInternal ℳ) : IsInternal fun i ↦ (ℳ i).baseChange S :=
   haveI := hm.chooseDecomposition
   Decomposition.isInternal _

Mathlib/LinearAlgebra/TensorProduct/Map.lean

@@ -595,6 +595,10 @@ def rTensor (f : N ≃ₗ[R] P) : N ⊗[R] M ≃ₗ[R] P ⊗[R] M := TensorProdu
 
 variable (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (m : M) (n : N) (p : P) (x : M ⊗[R] N) (y : N ⊗[R] M)
 
+theorem symm_lTensor : (f.lTensor M).symm = f.symm.lTensor M := rfl
+
+theorem symm_rTensor : (f.rTensor M).symm = f.symm.rTensor M := rfl
+
 @[simp] theorem coe_lTensor : lTensor M f = (f : N →ₗ[R] P).lTensor M := rfl
 
 @[simp] theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl