Extension of scalars for Lie-module maps #
A Lie-module map remains equivariant after extending both the Lie algebra and its modules. This transports an equivariant map together with the action, for example from an integral Chevalley lattice to its modular short-root representation.
@[simp]
theorem
LieModuleHom.baseChange_map_lie
{R : Type u_1}
{L : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[AddCommGroup N]
[Module R N]
[LieRingModule L N]
[LieModule R L N]
(A : Type u_5)
[CommRing A]
[Algebra R A]
(f : M →ₗ⁅R,L⁆ N)
(x : TensorProduct R A L)
(m : TensorProduct R A M)
:
Extending scalars preserves the equivariance of a Lie-module map.
def
LieModuleHom.baseChange
{R : Type u_1}
{L : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[AddCommGroup N]
[Module R N]
[LieRingModule L N]
[LieModule R L N]
(A : Type u_5)
[CommRing A]
[Algebra R A]
(f : M →ₗ⁅R,L⁆ N)
:
Extend scalars on a Lie-module morphism, including its acting Lie algebra.
Equations
- LieModuleHom.baseChange A f = { toLinearMap := LinearMap.baseChange A ↑f, map_lie' := ⋯ }
Instances For
@[simp]
theorem
LieModuleHom.baseChange_toLinearMap
{R : Type u_1}
{L : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[AddCommGroup N]
[Module R N]
[LieRingModule L N]
[LieModule R L N]
(A : Type u_5)
[CommRing A]
[Algebra R A]
(f : M →ₗ⁅R,L⁆ N)
:
The underlying linear map of scalar extension is the linear scalar extension.