The Killing form of a product of Lie algebras

The adjoint action of L × L' acts separately on the two factors, so the Killing form of the product is the sum of the Killing forms of the factors. Consequently a product of two Killing Lie algebras is again Killing. This lets constructions stated for finite-dimensional Lie algebras with nondegenerate Killing form, such as the internal Jordan decomposition, be applied to products and compared with the corresponding constructions on the factors.

The statements hold over any commutative ring for factors that are free of finite rank, which is what the trace of a product endomorphism needs.

Main declarations

• LieAlgebra.killingForm_prod_apply: the Killing form of L × L' is the sum of the Killing forms of L and L'.
• LieAlgebra.killingForm_prod: the Killing form of L × L' is the product bilinear form of the Killing forms of L and L'.
• LieAlgebra.IsKilling.instProd: a product of Killing Lie algebras is Killing.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §5.2.

@[simp]

theorem LieAlgebra.killingForm_prod_apply (R : Type u_1) (L : Type u_2) (L' : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [Module.Free R L] [Module.Finite R L] [Module.Free R L'] [Module.Finite R L'] (x y : L × L') : ((killingForm R (L × L')) x) y = ((killingForm R L) x.1) y.1 + ((killingForm R L') x.2) y.2

The Killing form of a product of Lie algebras is the sum of the Killing forms of the factors.

theorem LieAlgebra.killingForm_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'] [Module.Free R L] [Module.Finite R L] [Module.Free R L'] [Module.Finite R L'] : killingForm R (L × L') = (killingForm R L).prod (killingForm R L')

The Killing form of a product of Lie algebras is the product bilinear form of the Killing forms of the factors.

instance LieAlgebra.IsKilling.instProd (R : Type u_1) (L : Type u_2) (L' : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [Module.Free R L] [Module.Finite R L] [Module.Free R L'] [Module.Finite R L'] [IsKilling R L] [IsKilling R L'] : IsKilling R (L × L')

A product of two Killing Lie algebras is Killing.