Endomorphisms commuting with a subalgebra

An endomorphism linear over a subalgebra of Module.End K N commutes with that subalgebra. Restricting scalars therefore gives an element of its centralizer in Module.End K N. This fact uses only semiring scalars and an additive commutative monoid, independently of semisimplicity or finiteness assumptions used in double centralizer theorems.

theorem Subalgebra.restrictScalars_mem_centralizer {K : Type u_1} {N : Type u_2} [CommSemiring K] [AddCommMonoid N] [Module K N] (A : Subalgebra K (Module.End K N)) (g : Module.End (↥A) N) : ↑K g ∈ centralizer K ↑A

An endomorphism linear over a subalgebra of Module.End K N lies in its centralizer after restricting scalars to K.