Extension and restriction of scalars for Lie algebras #
Lie algebras have a well-behaved theory of extension and restriction of scalars.
Main definitions #
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)
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)