# Extension and restriction of scalars for Lie algebras and Lie modules #

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

## Main definitions #

• LieAlgebra.ExtendScalars.instLieAlgebra
• LieAlgebra.ExtendScalars.instLieModule
• LieAlgebra.RestrictScalars.lieAlgebra

## Tags #

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

@[simp]
theorem LieAlgebra.ExtendScalars.bracket_tmul (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [Algebra R A] [] [] [] [Module R M] [] [LieModule R L M] (s : A) (t : A) (x : L) (y : M) :
noncomputable instance LieAlgebra.ExtendScalars.instLieRing (R : Type u_1) (A : Type u_2) (L : Type u_3) [] [] [Algebra R A] [] [] :
Equations
noncomputable instance LieAlgebra.ExtendScalars.instLieAlgebra (R : Type u_1) (A : Type u_2) (L : Type u_3) [] [] [Algebra R A] [] [] :
Equations
noncomputable instance LieAlgebra.ExtendScalars.instLieRingModule (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [Algebra R A] [] [] [] [Module R M] [] [LieModule R L M] :
Equations
noncomputable instance LieAlgebra.ExtendScalars.instLieModule (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [Algebra R A] [] [] [] [Module R M] [] [LieModule R L M] :
LieModule A () ()
Equations
• =
noncomputable instance LieAlgebra.RestrictScalars.instLieRingRestrictScalars (R : Type u_1) (A : Type u_2) (L : Type u_3) [h : ] :
Equations
noncomputable instance LieAlgebra.RestrictScalars.lieAlgebra (R : Type u_1) (A : Type u_2) (L : Type u_3) [h : ] [] [] [] [Algebra R A] :
Equations
@[simp]
theorem LieModule.toEndomorphism_baseChange (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] (x : L) :
noncomputable def LieSubmodule.baseChange {R : Type u_1} (A : Type u_2) {L : Type u_3} {M : Type u_4} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] (N : LieSubmodule R L M) :
LieSubmodule A () ()

If A is an R-algebra, any Lie submodule of a Lie module M with coefficients in R may be pushed forward to a Lie submodule of A ⊗ M with coefficients in A.

This "base change" operation is also known as "extension of scalars".

Equations
• = let __src := ; { toSubmodule := __src, lie_mem := }
Instances For
@[simp]
theorem LieSubmodule.coe_baseChange (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] (N : LieSubmodule R L M) :
() =
theorem LieSubmodule.tmul_mem_baseChange_of_mem {R : Type u_1} {A : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] {N : LieSubmodule R L M} (a : A) {m : M} (hm : m N) :
theorem LieSubmodule.mem_baseChange_iff (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] {N : LieSubmodule R L M} {m : } :
m Submodule.span A (Submodule.map (() 1) N)
@[simp]
theorem LieSubmodule.baseChange_bot (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] :
@[simp]
theorem LieSubmodule.baseChange_top (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] :
theorem LieSubmodule.lie_baseChange (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] {I : LieIdeal R L} {N : LieSubmodule R L M} :