Graded Lie algebras

This file defines typeclasses SetLike.GradedBracket and GradedLieAlgebra, for working with Lie algebras that are graded by a collection ℒ of submodules. The additivity of degree with respect to the bracket product is encoded by an addition condition so we can avoid the usual difficulties of adding elements of A (i + j) to elements of A (j + i).

Main definitions

• SetLike.GradedBracket: A typeclass for a bracket to respect an additive grading.
• GradedLieAlgebra: A typeclass for a Lie algebra to respect an additive grading.
• LieDerivation.ofGradingSum: A Lie derivation on the direct sum of graded pieces, that scalar- multiplies the pieces by an additive map applied to degree.
• LieDerivation.ofGrading: A Lie derivation on a graded Lie algebra, that scalar-multiplies graded pieces by an additive map applied to degree.

class SetLike.GradedBracket {ι : Type u_1} {σ : Type u_2} {L : Type u_4} [SetLike σ L] [Bracket L L] [Add ι] (ℒ : ι → σ) : Prop

A class that ensures a bracket product preserves an additive grading.

• bracket_mem ⦃i j k : ι⦄ {gi gj : L} : i + j = k → gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ k

  Bracket is homogeneous

class GradedLieAlgebra {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) extends SetLike.GradedBracket ℒ, DirectSum.Decomposition ℒ : Type (max u_1 u_4)

A class that ensures a Lie algebra has a bracket that preserves a decomposition.

• bracket_mem ⦃i j k : ι⦄ {gi gj : L} : i + j = k → gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ k
• decompose' : L → DirectSum ι fun (i : ι) => ↥(ℒ i)
• left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℒ)) decompose'
• right_inv : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℒ)) decompose'

@[implicit_reducible]

instance DirectSum.instLieRingSubtypeMemSubmodule {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] : LieRing (DirectSum ι fun (i : ι) => ↥(ℒ i))

theorem DirectSum.bracket_apply_apply {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] (x y : DirectSum ι fun (i : ι) => ↥(ℒ i)) : ⁅x, y⁆ = (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x, (decomposeLinearEquiv ℒ).symm y⁆

@[simp]

theorem DirectSum.decompose_bracket {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] (x y : L) : (decompose ℒ) ⁅x, y⁆ = ⁅(decompose ℒ) x, (decompose ℒ) y⁆

@[simp]

theorem DirectSum.decompose_symm_bracket {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] (x y : DirectSum ι fun (i : ι) => ↥(ℒ i)) : (decompose ℒ).symm ⁅x, y⁆ = ⁅(decompose ℒ).symm x, (decompose ℒ).symm y⁆

@[implicit_reducible]

instance DirectSum.instLieAlgebraSubtypeMemSubmodule {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] : LieAlgebra R (DirectSum ι fun (i : ι) => ↥(ℒ i))

def DirectSum.decomposeLieEquiv {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] : L ≃ₗ⁅R⁆ DirectSum ι fun (i : ι) => ↥(ℒ i)

If L is graded by ι with degree i component ℒ i, then it is isomorphic as a Lie algebra to a direct sum of components.

def LieDerivation.ofGradingSum {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] (φ : ι →+ R) : LieDerivation R (DirectSum ι fun (i : ι) => ↥(ℒ i)) (DirectSum ι fun (i : ι) => ↥(ℒ i))

A derivation on the direct sum of graded pieces of a graded Lie algebra, induced by an additive map on the grading monoid.

@[simp]

theorem LieDerivation.ofGradingSum_of {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] (φ : ι →+ R) (i : ι) (a : ↥(ℒ i)) : (ofGradingSum ℒ φ) ((DirectSum.of (fun (x : ι) => ↥(ℒ x)) i) a) = φ i • (DirectSum.of (fun (x : ι) => ↥(ℒ x)) i) a

def LieDerivation.ofGrading {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] (φ : ι →+ R) : LieDerivation R L L

The Lie derivation on a graded Lie algebra that scalar-multiplies by an additive function of the degree.

theorem LieDerivation.ofGrading_apply_apply {ι : Type u_1} {R : Type u_3} {L : Type u_4} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] (φ : ι →+ R) {i : ι} {a : L} (ha : a ∈ ℒ i) : (ofGrading ℒ φ) a = φ i • a