Endomorphisms of tensor products

This file establishes semisimplicity and nilpotence properties of tensor-product endomorphisms. After embedding an unchanged projective factor as a direct summand of a free module, the tensor product is a direct summand of a direct sum of copies of the original module, and the corresponding one-sided tensor endomorphism acts componentwise.

Main declarations

• Module.End.IsSemisimple.rTensor: f ⊗ 1 is semisimple when f is.
• Module.End.IsSemisimple.lTensor: 1 ⊗ f is semisimple when f is.
• Module.End.commute_rTensor_lTensor: one-sided tensor endomorphisms on different factors commute.
• Module.End.IsSemisimple.tensorProduct: tensor products of semisimple endomorphisms are semisimple.
• IsNilpotent.tensorProduct_map_sub_one: TensorProduct.map f g - 1 is nilpotent when f - 1 and g - 1 are nilpotent.

@[simp]

theorem Module.End.rTensorAlgHom_apply {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (f : End K V) : (rTensorAlgHom K V W) f = LinearMap.rTensor W f

The right-tensor algebra homomorphism sends f to f.rTensor W.

@[simp]

theorem Module.End.lTensorAlgHom_apply {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (f : End K W) : (lTensorAlgHom K W V) f = LinearMap.lTensor V f

The left-tensor algebra homomorphism sends f to f.lTensor V.

theorem Module.End.commute_rTensor_lTensor {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (f : End K V) (g : End K W) : Commute (LinearMap.rTensor W f) (LinearMap.lTensor V g)

One-sided tensor endomorphisms acting on different factors commute.

theorem Module.End.IsSemisimple.rTensor {K : Type u} {V : Type v} {W : Type w} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [Projective K W] {f : End K V} (hf : f.IsSemisimple) : IsSemisimple (LinearMap.rTensor W f)

Tensoring a semisimple endomorphism on the right with an identity endomorphism preserves semisimplicity.

theorem Module.End.IsSemisimple.lTensor {K : Type u} {V : Type v} {W : Type w} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [Projective K V] {f : End K W} (hf : f.IsSemisimple) : IsSemisimple (LinearMap.lTensor V f)

Tensoring a semisimple endomorphism on the left with an identity endomorphism preserves semisimplicity.

theorem IsNilpotent.tensorProduct_map_sub_one {K : Type u} {V : Type v} {W : Type w} [CommSemiring K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] {f : Module.End K V} {g : Module.End K W} (hf : IsNilpotent (f - 1)) (hg : IsNilpotent (g - 1)) : IsNilpotent (TensorProduct.map f g - 1)

If f - 1 and g - 1 are nilpotent, then TensorProduct.map f g - 1 is nilpotent.

theorem Module.End.IsSemisimple.tensorProduct {K : Type u} {V : Type v} {W : Type w} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [PerfectField K] [FiniteDimensional K V] [FiniteDimensional K W] {f : End K V} {g : End K W} (hf : f.IsSemisimple) (hg : g.IsSemisimple) : IsSemisimple (TensorProduct.map f g)

The tensor product of two semisimple endomorphisms is semisimple.