Extension and restriction of scalars for Lie algebras

Lie algebras have a well-behaved theory of extension and restriction of scalars.

Main definitions

• LieAlgebra.ExtendScalars.lieAlgebra
• LieAlgebra.RestrictScalars.lieAlgebra

Tags

lie ring, lie algebra, extension of scalars, restriction of scalars, base change

instance LieAlgebra.ExtendScalars.instBracketTensorProductToCommSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToAddCommMonoidToAddCommGroupToModuleOfAssociativeRingOfAssociativeAlgebraToModule (R : Type u) (A : Type w) (L : Type v) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] : Bracket (TensorProduct R A L) (TensorProduct R A L)

@[simp]

theorem LieAlgebra.ExtendScalars.bracket_tmul (R : Type u) (A : Type w) (L : Type v) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] (s : A) (t : A) (x : L) (y : L) : ⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ[R] ⁅x, y⁆

instance LieAlgebra.ExtendScalars.instLieRingTensorProductToCommSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToAddCommMonoidToAddCommGroupToModuleOfAssociativeRingOfAssociativeAlgebraToModule (R : Type u) (A : Type w) (L : Type v) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] : LieRing (TensorProduct R A L)

instance LieAlgebra.ExtendScalars.lieAlgebra (R : Type u) (A : Type w) (L : Type v) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] : LieAlgebra A (TensorProduct R A L)

instance LieAlgebra.RestrictScalars.instLieRingRestrictScalars (R : Type u) (A : Type w) (L : Type v) [h : LieRing L] : LieRing (RestrictScalars R A L)

instance LieAlgebra.RestrictScalars.lieAlgebra (R : Type u) (A : Type w) (L : Type v) [h : LieRing L] [CommRing A] [LieAlgebra A L] [CommRing R] [Algebra R A] : LieAlgebra R (RestrictScalars R A L)