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_mul_eq_mul_trace_restrict_range: if c * c = a • c and f commutes with c, then trace (c * f) = a * trace (f|range c). Taking c to be the action of a quasi-idempotent of a group algebra computes the character of its image.
• TauCeti.LinearMap.trace_eq_mul_finrank_range: if f * f = a • f, then trace f = a * finrank (range f), the case f = 1 of the previous statement.
• TauCeti.LinearMap.two_mul_finrank_ker_one_add_of_sq_eq_one: for an involution σ, 2 dim ker (1 + σ) = dim M - tr σ, applying the above to f = 1 + σ, whose square is 2 f.
• TauCeti.LinearMap.three_mul_finrank_ker_one_add_add_sq_of_pow_three_eq_one: for υ ^ 3 = 1, 3 dim ker (1 + υ + υ²) = 2 dim M - tr υ - tr υ², applying it to f = 1 + υ + υ², whose square is 3 f.

These two dimension formulas need no hypothesis on the characteristic: when 2, respectively 3, vanishes in K, the essentially idempotent f is nilpotent and both sides are zero.

theorem TauCeti.LinearMap.trace_mul_eq_mul_trace_restrict_range {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] {c f : Module.End K M} {a : K} (hc : c * c = a • c) (hcf : Commute c f) (hf : ∀ x ∈ LinearMap.range c, f x ∈ LinearMap.range c := ⋯) : (LinearMap.trace K M) (c * f) = a * (LinearMap.trace K ↥(LinearMap.range c)) (LinearMap.restrict f hf)

The trace of a map commuting with an essentially idempotent endomorphism. If the square of c is a • c and f commutes with c, so that f preserves the range of c, then the trace of c * f is a times the trace of f on the range of c.

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

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.

theorem TauCeti.LinearMap.two_mul_finrank_ker_one_add_of_sq_eq_one {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] {σ : Module.End K M} (hσ : σ ^ 2 = 1) : 2 * ↑(Module.finrank K ↥(1 + σ).ker) = ↑(Module.finrank K M) - (LinearMap.trace K M) σ

The trace of an involution determines its -1-eigenspace: if σ ^ 2 = 1, then 2 dim ker (1 + σ) = dim M - tr σ in K.

theorem TauCeti.LinearMap.three_mul_finrank_ker_one_add_add_sq_of_pow_three_eq_one {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] {υ : Module.End K M} (hυ : υ ^ 3 = 1) : 3 * ↑(Module.finrank K ↥(1 + υ + υ ^ 2).ker) = 2 * ↑(Module.finrank K M) - (LinearMap.trace K M) υ - (LinearMap.trace K M) (υ ^ 2)

The traces of an order-three map determine the kernel of 1 + υ + υ²: if υ ^ 3 = 1, then 3 dim ker (1 + υ + υ²) = 2 dim M - tr υ - tr υ² in K.