The trace of an endomorphism whose square is a multiple of itself

An endomorphism f of a finite-dimensional vector space satisfying f * f = a • f is a scaled projection: when a ≠ 0 the endomorphism a⁻¹ • f is idempotent with the same range as f, so the trace of f is a times the dimension of that range. The degenerate case a = 0 obeys the same formula, because then f squares to zero, hence is nilpotent and traceless.

This is the standard device for pinning down the scalar in an essential idempotence identity c * c = a • c in a finite-dimensional algebra: compute the trace of multiplication by c in two ways, once from the identity and once from a basis. Mathlib has the idempotent case (LinearMap.IsProj.trace, together with IsIdempotentElem.isProj_range); this file removes the normalisation, which is exactly what makes the identity usable when the scalar is the unknown.

Main statements

• TauCeti.LinearMap.trace_eq_mul_finrank_range: if f * f = a • f, then trace f = a * finrank (range f).

theorem TauCeti.LinearMap.trace_eq_mul_finrank_range {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] {f : M →ₗ[K] M} {a : K} (hf : f * f = a • f) : (LinearMap.trace K M) f = a * ↑(Module.finrank K ↥f.range)

The trace of an essentially idempotent endomorphism. If the square of f is a • f, then the trace of f is a times the dimension of the range of f.

For a ≠ 0 this says that a⁻¹ • f is a projection onto range f; for a = 0 both sides vanish, because f then squares to zero.