Graded Lie algebras

This file defines typeclasses SetLike.GradedBracket and GradedLieAlgebra, for working with Lie algebras that are graded by a collection ℒ of submodules.

Main definitions

• SetLike.GradedBracket: A typeclass for a bracket to be compatible with a vector-additive grading.
• GradedLieAlgebra: A typeclass for a Lie algebra bracket to respect an additive grading.
• GradedLieModule: A typeclass for a Lie module to be compatible with a vector-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.

Implementation notes

For now we only implement internally-graded Lie algebras; supporting the externally-graded case would be achieved by generalizing the LieRing (⨁ i, ℒ i) instance to take a family of types, and defining a new GradedMonoid.GBracket class to provide the data piecewise.

class SetLike.GradedBracket {ι : Type u_1} {κ : Type u_2} {σ : Type u_3} {τ : Type u_4} {L : Type u_6} {M : Type u_7} [SetLike σ L] [SetLike τ M] [Bracket L M] [VAdd ι κ] (ℒ : ι → σ) (ℳ : κ → τ) : Prop

A graded bracket class that ensures a bracket action preserves a vector-additive grading.

• bracket_mem ⦃i : ι⦄ ⦃j : κ⦄ {gi : L} {hj : M} : gi ∈ ℒ i → hj ∈ ℳ j → ⁅gi, hj⁆ ∈ ℳ (i +ᵥ j)

  Bracket is homogeneous

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

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

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

class GradedLieModule {ι : Type u_1} {κ : Type u_2} {R : Type u_5} {L : Type u_6} {M : Type u_7} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [DecidableEq κ] [VAdd ι κ] [AddCommGroup M] [Module R M] [LieRingModule L M] (ℳ : κ → Submodule R M) [GradedLieAlgebra ℒ] [DirectSum.Decomposition ℳ] extends SetLike.GradedBracket ℒ ℳ : Prop

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

• bracket_mem ⦃i : ι⦄ ⦃j : κ⦄ {gi : L} {hj : M} : gi ∈ ℒ i → hj ∈ ℳ j → ⁅gi, hj⁆ ∈ ℳ (i +ᵥ j)

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

theorem DirectSum.bracket_apply_apply_self {ι : Type u_1} {R : Type u_5} {L : Type u_6} [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⁆

@[instance_reducible]

instance DirectSum.instLieRingModuleSubtypeMemSubmodule {ι : Type u_1} {κ : Type u_2} {R : Type u_5} {L : Type u_6} {M : Type u_7} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] [DecidableEq κ] [AddCommGroup M] [Module R M] [LieRingModule L M] (ℳ : κ → Submodule R M) [Decomposition ℳ] : LieRingModule (DirectSum ι fun (i : ι) => ↥(ℒ i)) (DirectSum κ fun (k : κ) => ↥(ℳ k))

Equations

• One or more equations did not get rendered due to their size.

theorem DirectSum.bracket_apply_apply {ι : Type u_1} {κ : Type u_2} {R : Type u_5} {L : Type u_6} {M : Type u_7} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] [DecidableEq κ] [AddCommGroup M] [Module R M] [LieRingModule L M] (ℳ : κ → Submodule R M) [Decomposition ℳ] (x : DirectSum ι fun (i : ι) => ↥(ℒ i)) (y : DirectSum κ fun (k : κ) => ↥(ℳ k)) : ⁅x, y⁆ = (decomposeLinearEquiv ℳ) ⁅(decomposeLinearEquiv ℒ).symm x, (decomposeLinearEquiv ℳ).symm y⁆

theorem DirectSum.decompose_bracket {ι : Type u_1} {κ : Type u_2} {R : Type u_5} {L : Type u_6} {M : Type u_7} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] [DecidableEq κ] [AddCommGroup M] [Module R M] [LieRingModule L M] (ℳ : κ → Submodule R M) [Decomposition ℳ] (x : L) (y : M) : (decompose ℳ) ⁅x, y⁆ = ⁅(decompose ℒ) x, (decompose ℳ) y⁆

@[simp]

theorem DirectSum.decompose_symm_bracket {ι : Type u_1} {κ : Type u_2} {R : Type u_5} {L : Type u_6} {M : Type u_7} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] [DecidableEq κ] [AddCommGroup M] [Module R M] [LieRingModule L M] (ℳ : κ → Submodule R M) [Decomposition ℳ] (x : DirectSum ι fun (i : ι) => ↥(ℒ i)) (y : DirectSum κ fun (k : κ) => ↥(ℳ k)) : (decompose ℳ).symm ⁅x, y⁆ = ⁅(decompose ℒ).symm x, (decompose ℳ).symm y⁆

@[instance_reducible]

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

Equations

• DirectSum.instLieAlgebraSubtypeMemSubmodule ℒ = { toDistribMulAction := DirectSum.instModule.toDistribMulAction, add_smul := ⋯, zero_smul := ⋯, lie_smul := ⋯ }

instance DirectSum.instLieModuleSubtypeMemSubmodule {ι : Type u_1} {κ : Type u_2} {R : Type u_5} {L : Type u_6} {M : Type u_7} [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L] (ℒ : ι → Submodule R L) [GradedLieAlgebra ℒ] [DecidableEq κ] [AddCommGroup M] [Module R M] [LieRingModule L M] (ℳ : κ → Submodule R M) [Decomposition ℳ] [LieModule R L M] : LieModule R (DirectSum ι fun (i : ι) => ↥(ℒ i)) (DirectSum κ fun (k : κ) => ↥(ℳ k))

def DirectSum.decomposeLieEquiv {ι : Type u_1} {R : Type u_5} {L : Type u_6} [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.

Equations

• DirectSum.decomposeLieEquiv ℒ = { toLinearMap := ↑(DirectSum.decomposeLinearEquiv ℒ), map_lie' := ⋯, invFun := (DirectSum.decomposeLinearEquiv ℒ).invFun, left_inv := ⋯, right_inv := ⋯ }

def LieDerivation.ofGradingSum {ι : Type u_1} {R : Type u_5} {L : Type u_6} [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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieDerivation.ofGradingSum_of {ι : Type u_1} {R : Type u_5} {L : Type u_6} [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_5} {L : Type u_6} [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.

Equations

• One or more equations did not get rendered due to their size.

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