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

source
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
source
@[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) :
⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ[R] ⁅x, y⁆
source
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
source
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
source
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
source
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] :
LieModule A (TensorProduct R A L) (TensorProduct R A M)
Equations
  • ⋯ = ⋯
source
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
source
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
source
@[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) :
(LieModule.toEnd A (TensorProduct R A L) (TensorProduct R A M)) (1 ⊗ₜ[R] x) = LinearMap.baseChange A ((LieModule.toEnd R L M) x)
source
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
Instances For
    source
    @[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) :
    ↑(LieSubmodule.baseChange A N) = Submodule.baseChange A ↑N
    source
    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 ∈ LieSubmodule.baseChange A N
    source
    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 ∈ LieSubmodule.baseChange A N ↔ m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
    source
    @[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] :
    LieSubmodule.baseChange A ⊥ = ⊥
    source
    @[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] :
    LieSubmodule.baseChange A ⊤ = ⊤
    source
    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} :
    LieSubmodule.baseChange A ⁅I, N⁆ = ⁅LieSubmodule.baseChange A I, LieSubmodule.baseChange A N⁆