Documentation

LeanPool.RegtsSevenster.RS.Classical.SchurTheory.EndSum

Constructive simplicity of endomorphism algebras #

Every nonzero endomorphism of a finite-dimensional complex vector space generates the full endomorphism algebra in the sense that it can be "sandwiched" to produce the identity: there exist endomorphisms U i, W i such that ∑ i, U i * A * W i = 1.

theorem RS.exists_sum_conj_eq_one {V : Type u_1} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (A : Module.End ℂ V) (hA : A ≠ 0) :
∃ (n : ℕ) (U : Fin n → Module.End ℂ V) (W : Fin n → Module.End ℂ V), ∑ i : Fin n, U i * A * W i = 1

The sandwich identity: a nonzero endomorphism generates the identity as a finite sum of two-sided products.