Endomorphisms of finite order

An endomorphism f of a vector space with f ^ n = 1 is annihilated by X ^ n - 1. Two consequences are recorded here: every root of its characteristic polynomial is an n-th root of unity, and if n is invertible in the coefficient field then f is semisimple, because X ^ n - 1 is then squarefree.

The roots of unity are algebraic integers, so as soon as the characteristic polynomial splits the trace, being the sum of those roots, is one too. Splitting is not a real hypothesis: base change to an algebraic closure leaves the trace alone beyond transporting it along the field embedding (LinearMap.trace_baseChange), and an element of the base field whose image is integral over ℤ was already integral over ℤ. So the trace of an endomorphism of finite order is an algebraic integer over any field.

Over an algebraically closed field semisimplicity is diagonalizability, so the eigenspaces of such an f decompose the space. Every power of f acts on the μ-eigenspace as the scalar μ ^ m, which turns the trace of f ^ m into the sum ∑ μ, dim(V_μ) * μ ^ m over the eigenvalues.

That sum is what makes the trace transform predictably under a ring endomorphism σ of the coefficient field: the dimensions are natural numbers and so are fixed by σ, so if σ raises every n-th root of unity to the j-th power then σ (tr f) = tr (f ^ j). Over ℂ complex conjugation is such a σ, with j = n - 1, since it sends a root of unity μ to μ⁻¹ = μ ^ (n - 1); that instance is the source of conj (χ g) = χ g⁻¹ for characters of complex representations.

The results are stated in the Module.End namespace, so they are available through dot notation on endomorphisms.

Main results

• Module.End.pow_eq_one_of_isRoot_charpoly: the roots of the characteristic polynomial of an endomorphism of finite order n are n-th roots of unity.
• Module.End.isSemisimple_of_pow_eq_one: an endomorphism of finite order n, with n invertible in the field, is semisimple.
• Module.End.isIntegral_trace_of_pow_eq_one: over any field, the trace of an endomorphism of finite order is integral over ℤ.
• Module.End.trace_pow_eq_sum_eigenvalue_pow: over an algebraically closed field, the trace of f ^ m is the sum of the m-th powers of the eigenvalues of f, weighted by the dimensions of the eigenspaces.
• Module.End.map_trace_eq_trace_pow: a ring endomorphism raising every n-th root of unity to the j-th power sends the trace of an endomorphism of finite order n to the trace of its j-th power.
• Module.End.conj_trace_eq_trace_pow_sub_one: over ℂ, the conjugate of the trace of an endomorphism of finite order n is the trace of its inverse f ^ (n - 1).
• Module.End.exists_eq_smul_of_norm_trace_eq_finrank: over ℂ, an endomorphism of finite order whose trace has absolute value the dimension is a scalar, the scalar being a root of unity. The trace is the sum of finrank ℂ V many roots of unity, so that absolute value is the largest it can take, and it is attained only when the eigenvalues all coincide.
• Module.End.trace_eq_finrank_iff: over ℂ, an endomorphism of finite order has trace equal to the dimension exactly when it is the identity. The trace is the sum of finrank ℂ V many roots of unity, each of real part at most 1, so the value finrank ℂ V is attained only when every eigenvalue is 1, and such a diagonalizable endomorphism is the identity. The statement holds over any field of characteristic zero; ℂ is where this proof and its consumers live, the descent along an embedding of the cyclotomic field generated by the eigenvalues not being carried out here.

theorem Module.End.pow_eq_one_of_isRoot_charpoly {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {f : End k V} {n : ℕ} (hf : f ^ n = 1) {μ : k} (hμ : (LinearMap.charpoly f).IsRoot μ) : μ ^ n = 1

Every root of the characteristic polynomial of an endomorphism f with f ^ n = 1 is an n-th root of unity.

theorem Module.End.isIntegral_trace_of_pow_eq_one {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {f : End k V} {n : ℕ} (hn : n ≠ 0) (hf : f ^ n = 1) : IsIntegral ℤ ((LinearMap.trace k V) f)

The trace of an endomorphism of finite order is an algebraic integer, over an arbitrary field. When the characteristic polynomial splits the trace is a sum of roots of unity; that splitting hypothesis is removed by base change to an algebraic closure, which preserves both the order of f and, up to the field embedding, its trace, and an element of k whose image in the closure is integral over ℤ is itself integral over ℤ.

theorem Module.End.isSemisimple_of_pow_eq_one {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] {f : End k V} {n : ℕ} (hn : ↑n ≠ 0) (hf : f ^ n = 1) : f.IsSemisimple

An endomorphism f with f ^ n = 1 for some n invertible in k is semisimple, because it is annihilated by the squarefree polynomial X ^ n - 1.

theorem Module.End.mapsTo_pow_eigenspace {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] (f : End k V) (μ : k) (m : ℕ) : Set.MapsTo ⇑(f ^ m) ↑(f.eigenspace μ) ↑(f.eigenspace μ)

Every power of f maps each eigenspace of f to itself, acting there as the scalar μ ^ m.

theorem Module.End.trace_pow_restrict_eigenspace {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (f : End k V) (μ : k) (m : ℕ) : (LinearMap.trace k ↥(f.eigenspace μ)) (LinearMap.restrict (f ^ m) ⋯) = ↑(finrank k ↥(f.eigenspace μ)) * μ ^ m

The trace of f ^ m on the μ-eigenspace of f is dim(V_μ) * μ ^ m, because f ^ m acts there as the scalar μ ^ m.

theorem Module.End.pow_eq_one_of_hasEigenvalue {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {f : End k V} {n : ℕ} (hf : f ^ n = 1) {μ : k} (hμ : f.HasEigenvalue μ) : μ ^ n = 1

Every eigenvalue of an endomorphism of finite order n is an n-th root of unity.

theorem Module.End.isInternal_eigenspace_of_pow_eq_one {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {f : End k V} {n : ℕ} [IsAlgClosed k] (hn : ↑n ≠ 0) (hf : f ^ n = 1) : DirectSum.IsInternal f.eigenspace

The eigenspaces of an endomorphism of finite order decompose the space, n being invertible in the algebraically closed field k: such an f is semisimple, hence diagonalizable.

theorem Module.End.trace_pow_eq_sum_eigenvalue_pow {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {f : End k V} {n : ℕ} [IsAlgClosed k] (hn : ↑n ≠ 0) (hf : f ^ n = 1) (m : ℕ) : (LinearMap.trace k V) (f ^ m) = ∑ μ ∈ ⋯.toFinset, ↑(finrank k ↥(f.eigenspace μ)) * μ ^ m

The trace of a power of an endomorphism of finite order is the weighted sum of the powers of its eigenvalues: tr (f ^ m) = ∑ μ, dim(V_μ) * μ ^ m, the sum being over the eigenvalues of f. The hypothesis (n : k) ≠ 0 makes f diagonalizable, so that the eigenspaces already exhaust the space.

theorem Module.End.map_trace_eq_trace_pow {k : Type u} {V : Type w} [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {f : End k V} {n : ℕ} [IsAlgClosed k] {j : ℕ} (hn : ↑n ≠ 0) (hf : f ^ n = 1) (σ : k →+* k) (hσ : ∀ (μ : k), μ ^ n = 1 → σ μ = μ ^ j) : σ ((LinearMap.trace k V) f) = (LinearMap.trace k V) (f ^ j)

A ring endomorphism raising the roots of unity to the j-th power raises an endomorphism of finite order to the j-th power, as far as the trace can see: if f ^ n = 1 and σ μ = μ ^ j for every n-th root of unity μ, then σ (tr f) = tr (f ^ j). Both sides are the sum ∑ μ, dim(V_μ) · μ ^ j over the eigenvalues, since a ring homomorphism fixes the dimensions, which enter as natural numbers.

theorem Module.End.conj_trace_eq_trace_pow_sub_one {V : Type w} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] {f : End ℂ V} {n : ℕ} (hn : n ≠ 0) (hf : f ^ n = 1) : (starRingEnd ℂ) ((LinearMap.trace ℂ V) f) = (LinearMap.trace ℂ V) (f ^ (n - 1))

Complex conjugation of the trace inverts the endomorphism. If f ^ n = 1 with n ≠ 0, then the conjugate of the trace of f is the trace of its inverse f ^ (n - 1): the eigenvalues of f are n-th roots of unity, and conjugation inverts those.

theorem Module.End.exists_eq_smul_of_norm_trace_eq_finrank {V : Type w} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] {f : End ℂ V} {n : ℕ} (hn : n ≠ 0) (hf : f ^ n = 1) (h : ‖(LinearMap.trace ℂ V) f‖ = ↑(finrank ℂ V)) : ∃ (μ : ℂ), μ ^ n = 1 ∧ f = μ • 1

An endomorphism of finite order whose trace has the largest possible absolute value is a scalar. The eigenvalues of f are n-th roots of unity and the trace is their sum, weighted by the dimensions of the eigenspaces, which add up to finrank ℂ V. A sum of finrank ℂ V many unit vectors of ℂ has absolute value finrank ℂ V only when they all point the same way, so every eigenvalue equals the common phase μ; f is diagonalizable, so it is μ times the identity.

The bound itself, ‖tr f‖ ≤ finrank ℂ V, is the triangle inequality; Module.End.eq_one_of_trace_eq_finrank is the case μ = 1, where the trace attains the bound at the positive real value finrank ℂ V.

theorem Module.End.eq_one_of_trace_eq_finrank {V : Type w} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] {f : End ℂ V} {n : ℕ} (hn : n ≠ 0) (hf : f ^ n = 1) (h : (LinearMap.trace ℂ V) f = ↑(finrank ℂ V)) : f = 1

An endomorphism of finite order with trace the dimension is the identity. The trace attains the largest absolute value it can, so f is a scalar (Module.End.exists_eq_smul_of_norm_trace_eq_finrank), and the scalar is 1 because the trace of μ • 1 is μ times the dimension.

The restriction to ℂ is one of proof and of API, not of substance. The statement is true over any field of characteristic zero, the eigenvalues generating a cyclotomic subfield of the algebraic closure that embeds into ℂ; what the argument uses is the comparison Re μ ≤ ‖μ‖, which such an embedding is exactly what it takes to have. That descent is not carried out here, and ℂ is where the consumers of this file work.

theorem Module.End.trace_eq_finrank_iff {V : Type w} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] {f : End ℂ V} {n : ℕ} (hn : n ≠ 0) (hf : f ^ n = 1) : (LinearMap.trace ℂ V) f = ↑(finrank ℂ V) ↔ f = 1

An endomorphism of finite order has trace the dimension exactly when it is the identity. The forward direction is Module.End.eq_one_of_trace_eq_finrank; the converse is LinearMap.trace_one.