Invariant vectors under extension of scalars

For a Lie module M over a Lie algebra L over a commutative ring R, the invariant vectors form the Lie submodule LieModule.maxTrivSubmodule R L M. This file compares the invariants of the extension of scalars A ⊗[R] M, as a module over A ⊗[R] L, with the extension of the invariants of M:

maxTrivSubmodule A (A ⊗[R] L) (A ⊗[R] M) = (maxTrivSubmodule R L M).baseChange A.

The containment ⊇ holds for every coefficient algebra. The reverse containment holds when A is flat over R and L is finitely generated as an R-module: the invariants are then the kernel of the linear map m ↦ (⁅s i, m⁆)ᵢ for a finite spanning family s of L, and a flat extension of scalars commutes with kernels (LinearMap.ker_baseChange_of_flat).

The equality is what lets an invariant vector found after extending scalars be traded for one over the original ring: if every invariant vector of M lies in a submodule N, then every invariant vector of A ⊗[R] M lies in N.baseChange A. Weyl's complete reducibility theorem over a field of characteristic zero is descended from the algebraically closed case in exactly this way.

Main results

• LieModule.baseChange_maxTrivSubmodule_le: the extension of an invariant vector is invariant.
• LieModule.maxTrivSubmodule_baseChange: over a flat coefficient algebra, and for a finitely generated Lie algebra, the invariants of the extension are the extension of the invariants.

theorem LieModule.baseChange_maxTrivSubmodule_le (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] : LieSubmodule.baseChange A (maxTrivSubmodule R L M) ≤ maxTrivSubmodule A (TensorProduct R A L) (TensorProduct R A M)

The extension of an invariant vector is invariant, over any coefficient algebra.

theorem LieModule.maxTrivSubmodule_baseChange (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] [Module.Flat R A] [Module.Finite R L] : maxTrivSubmodule A (TensorProduct R A L) (TensorProduct R A M) = LieSubmodule.baseChange A (maxTrivSubmodule R L M)

Over a flat coefficient algebra, extension of scalars commutes with taking invariants, for a Lie algebra that is finitely generated as a module.