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

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] : Bracket (TensorProduct R A L) (TensorProduct R A M)

Equations

• LieAlgebra.ExtendScalars.instBracketTensorProduct R A L M = { bracket := fun (x : TensorProduct R A L) (m : TensorProduct R A M) => ((LieAlgebra.ExtendScalars.bracket'✝ R A L M) x) m }

@[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 t : A) (x : L) (y : M) : ⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ[R] ⁅x, y⁆

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] : LieRing (TensorProduct R A L)

Equations

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

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] : LieAlgebra A (TensorProduct R A L)

Equations

• LieAlgebra.ExtendScalars.instLieAlgebra R A L = { toModule := TensorProduct.leftModule, lie_smul := ⋯ }

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] : LieRingModule (TensorProduct R A L) (TensorProduct R A M)

Equations

• LieAlgebra.ExtendScalars.instLieRingModule R A L M = { toBracket := LieAlgebra.ExtendScalars.instBracketTensorProduct R A L M, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

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] : LieModule A (TensorProduct R A L) (TensorProduct R A M)

noncomputable instance LieAlgebra.RestrictScalars.instLieRingRestrictScalars (R : Type u_1) (A : Type u_2) (L : Type u_3) [h : LieRing L] : LieRing (RestrictScalars R A L)

Equations

• LieAlgebra.RestrictScalars.instLieRingRestrictScalars R A L = h

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] : LieAlgebra R (RestrictScalars R A L)

Equations

• LieAlgebra.RestrictScalars.lieAlgebra R A L = { toModule := RestrictScalars.module R A L, lie_smul := ⋯ }

@[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) : (toEnd A (TensorProduct R A L) (TensorProduct R A M)) (1 ⊗ₜ[R] x) = LinearMap.baseChange A ((toEnd R L M) x)

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) : LieSubmodule A (TensorProduct R A L) (TensorProduct R A 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

• LieSubmodule.baseChange A N = { toSubmodule := Submodule.baseChange A ↑N, lie_mem := ⋯ }

@[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) : ↑(baseChange A N) = Submodule.baseChange A ↑N

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) : a ⊗ₜ[R] m ∈ baseChange A 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} : m ∈ baseChange A N ↔ m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)

@[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] : baseChange 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] : baseChange A ⊤ = ⊤

theorem LieSubmodule.lie_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] {I : LieIdeal R L} {N : LieSubmodule R L M} : baseChange A ⁅I, N⁆ = ⁅baseChange A I, baseChange A N⁆