The adjoint action of a product of Lie algebras

The bracket on L × L' is computed coordinatewise, so the adjoint endomorphism of a pair is the product of the adjoint endomorphisms of its coordinates. This identity is what lets trace, nilpotence and semisimplicity statements about ad on a product be reduced to the factors.

Main statements

• LieAlgebra.ad_prod: ad (x, x') = (ad x).prodMap (ad x').

theorem LieAlgebra.ad_prod {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (x : L × L') : (ad R (L × L')) x = LinearMap.prodMap ((ad R L) x.1) ((ad R L') x.2)

The adjoint endomorphism in a binary product acts separately on the two factors.