Jordan chains of nilpotent endomorphisms

A Jordan-chain basis of an endomorphism f of a vector space V is a basis of the form f ^ j (v i), j < len i, where f ^ len i kills the chain head v i. In such a basis f is a direct sum of nilpotent Jordan blocks of the sizes len i.

This file proves that every nilpotent endomorphism of a finite-dimensional vector space over a field has a Jordan-chain basis, and that the multiset of chain lengths (the partition of finrank K V given by the Jordan block sizes) is recovered from the dimensions of the kernels of the powers of f. Consequently two nilpotent endomorphisms are conjugate exactly when their powers have kernels of the same dimensions. The basic API of Jordan-chain bases and the conjugator between Jordan-chain bases with matching lengths only need a semiring of scalars, and the kernel-dimension formulas only need a division ring.

Main definitions and results

• Module.End.JordanChainBasis f ι: Jordan chains for f, indexed by ι, forming a basis.
• Module.End.exists_jordanChainBasis: a nilpotent endomorphism of a finite-dimensional vector space has a Jordan-chain basis.
• Module.End.JordanChainBasis.finrank_ker_pow: dim ker f ^ k = ∑ i, min k (len i).
• Module.End.JordanChainBasis.card_len_eq_add_one: the number of chains of length k + 1 in terms of the dimensions of the kernels of f ^ k, f ^ (k + 1) and f ^ (k + 2).
• Module.End.JordanChainBasis.exists_equiv_len_eq: chain lengths are unique up to reindexing.
• Module.End.JordanChainBasis.equiv: the conjugator between Jordan-chain bases with matching lengths, see Module.End.JordanChainBasis.apply_equiv.
• Module.End.exists_linearEquiv_conj_eq_iff: two nilpotent endomorphisms of finite-dimensional vector spaces are conjugate if and only if dim ker f ^ k = dim ker g ^ k for every k.
• Module.End.JordanChainBasis.joinEnds: the rank-one endomorphism sending the last vector of one chain to the last vector of another.
• Module.End.JordanChainBasis.finrank_range_add_smul_joinEnds_pow and Module.End.JordanChainBasis.exists_linearEquiv_conj_add_smul_joinEnds: for t ≠ 0 the endomorphisms f + t • joinEnds i j are conjugate to one another, and the rank of the k-th power exceeds that of f ^ k by one exactly when len j ≤ k ≤ len i.

Elementary degenerations

For chains i ≠ j of lengths m = len i and r = len j, adding t • joinEnds i j to f links the end of chain i to the end of chain j. When r ≤ m and t ≠ 0 the result has Jordan chains of lengths m + 1 and r - 1 in place of m and r (the second one disappearing when r = 1), as the rank formula shows, and at t = 0 it is f again. So, over a topological field in which 0 is not isolated, f is a limit of conjugates of an endomorphism whose Jordan type is obtained from that of f by moving one box from a shorter part to a longer one. These moves generate the dominance order on partitions, and this family is the degeneration behind the description of nilpotent orbit closures by dominance. Over an infinite field the same family puts f in the Zariski closure of that conjugacy class. When m < r the rank formula shows that the perturbation does not change the Jordan type.

Implementation notes

Existence is proved by splitting off one chain of maximal length together with an invariant complement. If f ^ m kills the invariant subspace Z but f ^ (m - 1) v ≠ 0 for some v ∈ Z, choose a linear form φ with φ (f ^ (m - 1) v) ≠ 0. The common kernel in Z of the forms φ ∘ f ^ j, j < m, is invariant and complementary in Z to the span of the chain of v.

References

• P. R. Halmos, Finite-Dimensional Vector Spaces, §57.
• M. Gerstenhaber, On dominance and varieties of commuting matrices, Ann. of Math. 73 (1961), 324–348.

structure Module.End.JordanChainBasis {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] (f : End K V) (ι : Type u_4) : Type (max u_2 u_4)

A Jordan-chain basis of f indexed by ι: chain i has head head i and positive length len i, the power f ^ len i kills head i, and the vectors f ^ j (head i), j < len i, form a basis of V. In this basis f is the direct sum of nilpotent Jordan blocks of sizes len i.

• len : ι → ℕ

  The length of each chain.

• head : ι → V

  The head of each chain.

• len_pos (i : ι) : 0 < self.len i
• pow_len_apply_head (i : ι) : (f ^ self.len i) (self.head i) = 0
• linearIndependent : LinearIndependent K fun (p : (i : ι) × Fin (self.len i)) => (f ^ ↑p.snd) (self.head p.fst)
• span_eq_top : Submodule.span K (Set.range fun (p : (i : ι) × Fin (self.len i)) => (f ^ ↑p.snd) (self.head p.fst)) = ⊤

theorem Module.End.JordanChainBasis.ext {K : Type u_1} {V : Type u_2} {inst✝ : Semiring K} {inst✝¹ : AddCommMonoid V} {inst✝² : Module K V} {f : End K V} {ι : Type u_4} {x y : f.JordanChainBasis ι} (len : x.len = y.len) (head : x.head = y.head) : x = y

theorem Module.End.JordanChainBasis.ext_iff {K : Type u_1} {V : Type u_2} {inst✝ : Semiring K} {inst✝¹ : AddCommMonoid V} {inst✝² : Module K V} {f : End K V} {ι : Type u_4} {x y : f.JordanChainBasis ι} : x = y ↔ x.len = y.len ∧ x.head = y.head

noncomputable def Module.End.JordanChainBasis.basis {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) : Basis ((i : ι) × Fin (c.len i)) K V

The basis f ^ j (head i), j < len i, of a Jordan-chain basis.

@[simp]

theorem Module.End.JordanChainBasis.basis_apply {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (p : (i : ι) × Fin (c.len i)) : c.basis p = (f ^ ↑p.snd) (c.head p.fst)

theorem Module.End.JordanChainBasis.pow_apply_basis {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (k : ℕ) (i : ι) (j : Fin (c.len i)) : (f ^ k) (c.basis ⟨i, j⟩) = if h : ↑j + k < c.len i then c.basis ⟨i, ⟨↑j + k, h⟩⟩ else 0

A power of f moves a vector of a Jordan-chain basis along its chain, or kills it once it reaches the end of the chain.

theorem Module.End.JordanChainBasis.apply_basis {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (i : ι) (j : Fin (c.len i)) : f (c.basis ⟨i, j⟩) = if h : ↑j + 1 < c.len i then c.basis ⟨i, ⟨↑j + 1, h⟩⟩ else 0

The endomorphism f moves a vector of a Jordan-chain basis one step along its chain, or kills it at the end of the chain.

theorem Module.End.JordanChainBasis.isNilpotent {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} [Finite ι] (c : f.JordanChainBasis ι) : IsNilpotent f

An endomorphism with a finite Jordan-chain basis is nilpotent.

theorem Module.End.JordanChainBasis.range_pow {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (k : ℕ) : LinearMap.range (f ^ k) = Submodule.span K (Set.range fun (p : (i : ι) × Fin (c.len i - k)) => c.basis ⟨p.fst, ⟨↑p.snd + k, ⋯⟩⟩)

The range of f ^ k is spanned by the vectors of a Jordan-chain basis at depth at least k in their chains.

noncomputable def Module.End.JordanChainBasis.equiv {K : Type u_1} {V : Type u_2} {W : Type u_3} [Semiring K] [AddCommMonoid V] [AddCommMonoid W] [Module K V] [Module K W] {f : End K V} {g : End K W} {ι : Type u_4} {κ : Type u_5} (c : f.JordanChainBasis ι) (d : g.JordanChainBasis κ) (σ : ι ≃ κ) (hσ : ∀ (i : ι), d.len (σ i) = c.len i) : V ≃ₗ[K] W

The linear equivalence between the spaces of two Jordan-chain bases whose lengths agree under the reindexing σ, matching chain vectors at equal depths in corresponding chains. It conjugates one endomorphism to the other, see apply_equiv.

@[simp]

theorem Module.End.JordanChainBasis.equiv_pow_apply_head {K : Type u_1} {V : Type u_2} {W : Type u_3} [Semiring K] [AddCommMonoid V] [AddCommMonoid W] [Module K V] [Module K W] {f : End K V} {g : End K W} {ι : Type u_4} {κ : Type u_5} (c : f.JordanChainBasis ι) (d : g.JordanChainBasis κ) (σ : ι ≃ κ) (hσ : ∀ (i : ι), d.len (σ i) = c.len i) (i : ι) (j : ℕ) : (c.equiv d σ hσ) ((f ^ j) (c.head i)) = (g ^ j) (d.head (σ i))

The conjugator of two Jordan-chain bases with matching lengths sends f ^ j of a chain head to g ^ j of the corresponding head; past the end of the chains both sides vanish.

@[simp]

theorem Module.End.JordanChainBasis.equiv_symm {K : Type u_1} {V : Type u_2} {W : Type u_3} [Semiring K] [AddCommMonoid V] [AddCommMonoid W] [Module K V] [Module K W] {f : End K V} {g : End K W} {ι : Type u_4} {κ : Type u_5} (c : f.JordanChainBasis ι) (d : g.JordanChainBasis κ) (σ : ι ≃ κ) (hσ : ∀ (i : ι), d.len (σ i) = c.len i) : (c.equiv d σ hσ).symm = d.equiv c σ.symm ⋯

The inverse of the conjugator of two Jordan-chain bases with matching lengths is the conjugator in the opposite direction.

@[simp]

theorem Module.End.JordanChainBasis.apply_equiv {K : Type u_1} {V : Type u_2} {W : Type u_3} [Semiring K] [AddCommMonoid V] [AddCommMonoid W] [Module K V] [Module K W] {f : End K V} {g : End K W} {ι : Type u_4} {κ : Type u_5} (c : f.JordanChainBasis ι) (d : g.JordanChainBasis κ) (σ : ι ≃ κ) (hσ : ∀ (i : ι), d.len (σ i) = c.len i) (x : V) : g ((c.equiv d σ hσ) x) = (c.equiv d σ hσ) (f x)

The conjugator of two Jordan-chain bases with matching lengths intertwines the two endomorphisms.

theorem Module.End.JordanChainBasis.finrank_eq_sum_len {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} [StrongRankCondition K] [Fintype ι] (c : f.JordanChainBasis ι) : finrank K V = ∑ i : ι, c.len i

The dimension of V is the sum of the lengths of the chains.

theorem Module.End.JordanChainBasis.finrank_range_pow {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} [StrongRankCondition K] [Fintype ι] (c : f.JordanChainBasis ι) (k : ℕ) : finrank K ↥(LinearMap.range (f ^ k)) = ∑ i : ι, (c.len i - k)

The rank of f ^ k is ∑ i, (len i - k).

@[simp]

theorem Module.End.JordanChainBasis.conj_equiv {K : Type u_1} {V : Type u_2} {W : Type u_3} [CommSemiring K] [AddCommMonoid V] [AddCommMonoid W] [Module K V] [Module K W] {f : End K V} {g : End K W} {ι : Type u_4} {κ : Type u_5} (c : f.JordanChainBasis ι) (d : g.JordanChainBasis κ) (σ : ι ≃ κ) (hσ : ∀ (i : ι), d.len (σ i) = c.len i) : (c.equiv d σ hσ).conj f = g

Two endomorphisms are conjugate by the conjugator of Jordan-chain bases with matching lengths.

theorem Module.End.JordanChainBasis.finrank_ker_pow {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_4} [Fintype ι] (c : f.JordanChainBasis ι) (k : ℕ) : finrank K ↥(LinearMap.ker (f ^ k)) = ∑ i : ι, min k (c.len i)

The dimension of the kernel of f ^ k is ∑ i, min k (len i).

theorem Module.End.JordanChainBasis.finrank_ker_pow_succ {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_4} [Fintype ι] (c : f.JordanChainBasis ι) (k : ℕ) : finrank K ↥(LinearMap.ker (f ^ (k + 1))) = finrank K ↥(LinearMap.ker (f ^ k)) + {i : ι | k < c.len i}.card

Passing from f ^ k to f ^ (k + 1), the kernel grows by one dimension for each chain of length greater than k.

theorem Module.End.JordanChainBasis.card_len_eq_add_one {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_4} [Fintype ι] (c : f.JordanChainBasis ι) (k : ℕ) : {i : ι | c.len i = k + 1}.card = finrank K ↥(LinearMap.ker (f ^ (k + 1))) - finrank K ↥(LinearMap.ker (f ^ k)) - (finrank K ↥(LinearMap.ker (f ^ (k + 2))) - finrank K ↥(LinearMap.ker (f ^ (k + 1))))

The number of Jordan chains of length k + 1 is determined by the dimensions of the kernels of f ^ k, f ^ (k + 1) and f ^ (k + 2).

theorem Module.End.JordanChainBasis.exists_equiv_len_eq {K : Type u_1} {V : Type u_2} {W : Type u_3} [DivisionRing K] [AddCommGroup V] [AddCommGroup W] [Module K V] [Module K W] {f : End K V} {g : End K W} {ι : Type u_4} {κ : Type u_5} [Finite ι] [Finite κ] (c : f.JordanChainBasis ι) (d : g.JordanChainBasis κ) (h : ∀ (k : ℕ), finrank K ↥(f ^ k).ker = finrank K ↥(g ^ k).ker) : ∃ (σ : ι ≃ κ), ∀ (i : ι), d.len (σ i) = c.len i

The lengths of two Jordan-chain bases agree up to reindexing as soon as the kernels of the powers of the two endomorphisms have the same dimensions. For g = f this is the uniqueness of the Jordan block sizes of f.

theorem Module.End.exists_jordanChainBasis {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : End K V} [FiniteDimensional K V] (hf : IsNilpotent f) : ∃ (ι : Type) (x : Fintype ι), Nonempty (f.JordanChainBasis ι)

A nilpotent endomorphism of a finite-dimensional vector space has a Jordan-chain basis.

theorem Module.End.isNilpotent_iff_exists_jordanChainBasis {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : End K V} [FiniteDimensional K V] : IsNilpotent f ↔ ∃ (ι : Type) (x : Fintype ι), Nonempty (f.JordanChainBasis ι)

An endomorphism of a finite-dimensional vector space is nilpotent if and only if it has a Jordan-chain basis.

theorem Module.End.exists_linearEquiv_conj_eq_iff {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [AddCommGroup W] [Module K V] [Module K W] {f : End K V} {g : End K W} [FiniteDimensional K V] [FiniteDimensional K W] (hf : IsNilpotent f) (hg : IsNilpotent g) : (∃ (e : V ≃ₗ[K] W), e.conj f = g) ↔ ∀ (k : ℕ), finrank K ↥(f ^ k).ker = finrank K ↥(g ^ k).ker

Two nilpotent endomorphisms of finite-dimensional vector spaces are conjugate if and only if the kernels of their powers have the same dimensions.

@[simp]

theorem Module.End.JordanChainBasis.basis_coord_comp_pow_eq_zero {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) {p : (i : ι) × Fin (c.len i)} {k : ℕ} (hk : ↑p.snd < k) : c.basis.coord p ∘ₗ f ^ k = 0

The coordinate of depth b in a Jordan-chain basis vanishes on the range of f ^ k when b < k.

theorem Module.End.JordanChainBasis.pow_apply_head_mem_range_pow_iff {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} [Nontrivial K] (c : f.JordanChainBasis ι) (j : ι) (k : ℕ) : (f ^ (c.len j - 1)) (c.head j) ∈ LinearMap.range (f ^ k) ↔ k < c.len j

The last vector f ^ (len j - 1) (head j) of chain j lies in the range of f ^ k exactly when k < len j.

noncomputable def Module.End.JordanChainBasis.joinEnds {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (i j : ι) : End K V

The rank-one endomorphism sending the last vector f ^ (len i - 1) (head i) of chain i to the last vector of chain j, and every other vector of the Jordan-chain basis to 0.

theorem Module.End.JordanChainBasis.joinEnds_apply {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (i j : ι) (x : V) : (c.joinEnds i j) x = (c.basis.repr x) ⟨i, ⟨c.len i - 1, ⋯⟩⟩ • (f ^ (c.len j - 1)) (c.head j)

The endomorphism joinEnds i j multiplies the last vector of chain j by the coordinate of the last vector of chain i.

@[simp]

theorem Module.End.JordanChainBasis.joinEnds_pow_apply_head {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (i j : ι) : (c.joinEnds i j) ((f ^ (c.len i - 1)) (c.head i)) = (f ^ (c.len j - 1)) (c.head j)

The endomorphism joinEnds i j sends the last vector of chain i to the last vector of chain j.

@[simp]

theorem Module.End.JordanChainBasis.mul_joinEnds {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (i j : ι) : f * c.joinEnds i j = 0

The image of joinEnds i j is killed by f, being spanned by the end of a chain.

@[simp]

theorem Module.End.JordanChainBasis.joinEnds_mul_joinEnds {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) {i j : ι} (hij : i ≠ j) : c.joinEnds i j * c.joinEnds i j = 0

For distinct chains i ≠ j, the endomorphism joinEnds i j squares to zero.

@[simp]

theorem Module.End.JordanChainBasis.joinEnds_mul_pow_of_le {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) (i j : ι) {k : ℕ} (hk : c.len i ≤ k) : c.joinEnds i j * f ^ k = 0

The endomorphism joinEnds i j vanishes on the range of f ^ k once len i ≤ k.

theorem Module.End.JordanChainBasis.add_smul_joinEnds_pow_succ {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) {i j : ι} (hij : i ≠ j) (t : K) (k : ℕ) : (f + t • c.joinEnds i j) ^ (k + 1) = f ^ (k + 1) + t • (c.joinEnds i j * f ^ k)

For distinct chains i ≠ j, the powers of f + t • joinEnds i j are f ^ (k + 1) + t • joinEnds i j * f ^ k, since f * joinEnds i j and joinEnds i j ^ 2 vanish.

theorem Module.End.JordanChainBasis.isNilpotent_add_smul_joinEnds {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_4} [Finite ι] (c : f.JordanChainBasis ι) {i j : ι} (hij : i ≠ j) (t : K) : IsNilpotent (f + t • c.joinEnds i j)

For distinct chains i ≠ j of a finite Jordan-chain basis, f + t • joinEnds i j is nilpotent.

theorem Module.End.JordanChainBasis.range_add_smul_joinEnds_pow {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_4} (c : f.JordanChainBasis ι) {i j : ι} (hij : i ≠ j) {t : K} (ht : t ≠ 0) {k : ℕ} (hk₀ : 0 < k) (hk : k ≤ c.len i) : LinearMap.range ((f + t • c.joinEnds i j) ^ k) = LinearMap.range (f ^ k) ⊔ K ∙ (f ^ (c.len j - 1)) (c.head j)

For t ≠ 0 and 0 < k ≤ len i, the range of (f + t • joinEnds i j) ^ k is spanned by the range of f ^ k together with the last vector of chain j.

theorem Module.End.JordanChainBasis.finrank_range_add_smul_joinEnds_pow {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_4} [Finite ι] (c : f.JordanChainBasis ι) {i j : ι} (hij : i ≠ j) {t : K} (ht : t ≠ 0) (k : ℕ) : finrank K ↥(LinearMap.range ((f + t • c.joinEnds i j) ^ k)) = finrank K ↥(LinearMap.range (f ^ k)) + if c.len j ≤ k ∧ k ≤ c.len i then 1 else 0

Ranks along an elementary degeneration. For distinct chains i ≠ j and t ≠ 0, the rank of (f + t • joinEnds i j) ^ k exceeds the rank of f ^ k by one when len j ≤ k ≤ len i, and equals it otherwise.

theorem Module.End.JordanChainBasis.exists_linearEquiv_conj_add_smul_joinEnds {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_4} [Finite ι] (c : f.JordanChainBasis ι) {i j : ι} (hij : i ≠ j) {s t : K} (hs : s ≠ 0) (ht : t ≠ 0) : ∃ (e : V ≃ₗ[K] V), e.conj (f + s • c.joinEnds i j) = f + t • c.joinEnds i j

The elementary degeneration has a single orbit away from t = 0. For distinct chains i ≠ j and s, t ≠ 0, the endomorphisms f + s • joinEnds i j and f + t • joinEnds i j are conjugate.