Documentation

Mathlib.Algebra.Lie.BaseChange

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 #

Tags #

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

noncomputable instance LieAlgebra.ExtendScalars.instBracketTensorProduct (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
Equations
@[simp]
theorem LieAlgebra.ExtendScalars.bracket_tmul (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L 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) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] :
Equations
noncomputable instance LieAlgebra.ExtendScalars.instLieAlgebra (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] :
Equations
noncomputable instance LieAlgebra.ExtendScalars.instLieRingModule (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L 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) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
Equations
  • =
noncomputable instance LieAlgebra.RestrictScalars.lieAlgebra (R : Type u_1) (A : Type u_2) (L : Type u_3) [h : LieRing L] [CommRing A] [LieAlgebra A L] [CommRing R] [Algebra R A] :
Equations
@[simp]
theorem LieModule.toEnd_baseChange (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [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} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] (N : LieSubmodule R L M) :

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
Instances For
    @[simp]
    theorem LieSubmodule.coe_baseChange (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [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} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [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) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] {N : LieSubmodule R L M} {m : TensorProduct R A M} :
    @[simp]
    theorem LieSubmodule.baseChange_bot (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] :
    @[simp]
    theorem LieSubmodule.baseChange_top (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] :