Eigenvalues of sums of commuting idempotents

A finite family of pairwise commuting idempotents has a particularly rigid spectrum. If its sum scales a nonzero vector in a module with no zero scalar divisors, then the scalar is the image of a natural number no larger than the size of the family. This bounds the possible eigenvalues without requiring finite-dimensionality or a simultaneous eigenspace decomposition.

Main results

• Finset.exists_eq_natCast_of_sum_smul_eq_smul: an eigenvalue of a finite sum of commuting idempotents is a bounded natural-number cast.
• Finset.smul_eq_self_of_sum_smul_eq_card_smul: if that eigenvalue is the number of idempotents, every idempotent in the family fixes the vector.

theorem Finset.exists_eq_natCast_of_sum_smul_eq_smul {K : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} [Ring K] [Semiring A] [AddCommGroup M] [Module K M] [Module A M] [SMulCommClass A K M] [NoZeroSMulDivisors K M] (s : Finset ι) (p : ι → A) (hp : ∀ i ∈ s, IsIdempotentElem (p i)) (hcomm : (↑s).Pairwise fun (i j : ι) => Commute (p i) (p j)) {x : M} (hx : x ≠ 0) {μ : K} (heigen : (∑ i ∈ s, p i) • x = μ • x) : ∃ m ≤ s.card, μ = ↑m

If a finite sum of pairwise commuting idempotents scales a nonzero vector, its eigenvalue is the cast of a natural number bounded by the number of idempotents.

No finite-dimensionality or splitting hypothesis is needed. The no-zero-scalar-divisors assumption is exactly what makes a scalar determined by its action on the nonzero vector.

theorem Finset.smul_eq_self_of_sum_smul_eq_card_smul {K : Type u_5} {A : Type u_6} {M : Type u_7} {ι : Type u_8} [Ring K] [CharZero K] [Ring A] [AddCommGroup M] [Module K M] [Module A M] [SMulCommClass A K M] [NoZeroSMulDivisors K M] (s : Finset ι) (p : ι → A) (hp : ∀ i ∈ s, IsIdempotentElem (p i)) (hcomm : (↑s).Pairwise fun (i j : ι) => Commute (p i) (p j)) {x : M} (heigen : (∑ i ∈ s, p i) • x = ↑s.card • x) {a : ι} (ha : a ∈ s) : p a • x = x

If a sum of commuting idempotents acts on a vector by the cardinality of the family, then every idempotent in the family fixes that vector, including when the vector is zero.