The Jordan partition of a nilpotent endomorphism

The lengths of a Jordan-chain basis form a native Nat.Partition of the dimension. This partition is independent of the chosen chains: the multiplicity of each positive part is the drop in successive increases of the kernel dimensions. Conversely, the partition recovers all those dimensions, and therefore completely determines conjugacy of nilpotent endomorphisms between finite-dimensional vector spaces.

Module.End.jordanPartition makes this invariant available without choosing chains. Module.End.JordanChainBasis.jordanPartition_eq identifies it with any supplied chain basis, and Module.End.exists_linearEquiv_conj_eq_iff_jordanPartition_parts_eq gives the conjugacy criterion. No algebraic closure or characteristic assumption is needed.

The dominance order on Jordan partitions compares ranks of powers: Module.End.jordanPartition_dominates_jordanPartition_iff says that the Jordan partition of f dominates that of g exactly when rank (g ^ k) ≤ rank (f ^ k) for every k. For nilpotent matrices this is the combinatorial side of the description of orbit closures by dominance.

References

• P. R. Halmos, Finite-Dimensional Vector Spaces, §57.

noncomputable def Module.End.JordanChainBasis.partition {K : Type u_1} {V : Type u_2} [Semiring K] [StrongRankCondition K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_3} [Fintype ι] (c : f.JordanChainBasis ι) : (finrank K V).Partition

The partition whose parts are the lengths of the chains.

@[simp]

theorem Module.End.JordanChainBasis.partition_parts {K : Type u_1} {V : Type u_2} [Semiring K] [StrongRankCondition K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_3} [Fintype ι] (c : f.JordanChainBasis ι) : c.partition.parts = Multiset.map c.len Finset.univ.val

The parts of a chain partition are the chain lengths, with their multiplicities.

theorem Module.End.JordanChainBasis.count_partition_parts {K : Type u_1} {V : Type u_2} [Semiring K] [StrongRankCondition K] [AddCommMonoid V] [Module K V] {f : End K V} {ι : Type u_3} [Fintype ι] (c : f.JordanChainBasis ι) (k : ℕ) : Multiset.count k c.partition.parts = {i : ι | c.len i = k}.card

The multiplicity of a part is the number of chains of that length.

theorem Module.End.JordanChainBasis.finrank_ker_pow_eq_sum_partition {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_3} [Fintype ι] (c : f.JordanChainBasis ι) (k : ℕ) : finrank K ↥(LinearMap.ker (f ^ k)) = (Multiset.map (min k) c.partition.parts).sum

The partition recovers the dimensions of the kernels of all powers.

theorem Module.End.JordanChainBasis.count_partition_parts_succ {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_3} [Fintype ι] (c : f.JordanChainBasis ι) (k : ℕ) : Multiset.count (k + 1) c.partition.parts = 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))))

Positive-part multiplicities are recovered from successive kernel dimensions.

theorem Module.End.JordanChainBasis.card_filter_partition_parts {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {f : End K V} {ι : Type u_3} [Fintype ι] (c : f.JordanChainBasis ι) (k : ℕ) : (Multiset.filter (fun (x : ℕ) => k < x) c.partition.parts).card = finrank K ↥(LinearMap.ker (f ^ (k + 1))) - finrank K ↥(LinearMap.ker (f ^ k))

The number of parts larger than k is the increase in kernel dimension from power k to power k + 1.

noncomputable def Module.End.jordanPartition {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (hf : IsNilpotent f) : (finrank K V).Partition

The Jordan partition of a nilpotent endomorphism, with each Jordan block contributing its size as a part. It is characterized by count_jordanPartition_parts_succ.

theorem Module.End.count_jordanPartition_parts_succ {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (hf : IsNilpotent f) (k : ℕ) : Multiset.count (k + 1) (f.jordanPartition hf).parts = 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 multiplicity of the part k + 1 is the drop in kernel-dimension increases from k to k + 1 and from k + 1 to k + 2.

theorem Module.End.JordanChainBasis.jordanPartition_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} {ι : Type u_3} [Fintype ι] (c : f.JordanChainBasis ι) (hf : IsNilpotent f) : f.jordanPartition hf = c.partition

Every Jordan-chain basis gives the same Jordan partition.

theorem Module.End.finrank_ker_pow_eq_sum_jordanPartition {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (hf : IsNilpotent f) (k : ℕ) : finrank K ↥(LinearMap.ker (f ^ k)) = (Multiset.map (min k) (f.jordanPartition hf).parts).sum

The Jordan partition determines all dimensions of kernels of powers.

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

Two nilpotent endomorphisms have equal Jordan-partition parts exactly when all their kernel dimensions agree, even on different vector spaces.

theorem Module.End.exists_linearEquiv_conj_eq_iff_jordanPartition_parts_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type u_3} [AddCommGroup W] [Module K W] [FiniteDimensional K W] (f : End K V) (g : End K W) (hf : IsNilpotent f) (hg : IsNilpotent g) : (∃ (e : V ≃ₗ[K] W), e.conj f = g) ↔ (f.jordanPartition hf).parts = (g.jordanPartition hg).parts

The Jordan partition is a complete conjugacy invariant for nilpotent endomorphisms, including endomorphisms of different vector spaces.

@[simp]

theorem Module.End.jordanPartition_conj {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (e : V ≃ₗ[K] V) (h : IsNilpotent (e.conj f)) : (e.conj f).jordanPartition h = f.jordanPartition ⋯

Conjugating an endomorphism preserves its Jordan partition.

theorem Module.End.card_filter_jordanPartition_parts {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (hf : IsNilpotent f) (k : ℕ) : (Multiset.filter (fun (x : ℕ) => k < x) (f.jordanPartition hf).parts).card = finrank K ↥(LinearMap.ker (f ^ (k + 1))) - finrank K ↥(LinearMap.ker (f ^ k))

The length of column k + 1 of the Jordan diagram is the increase in kernel dimension from the kth to the (k + 1)st power.

theorem Module.End.jordanPartition_dominates_jordanPartition_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f g : End K V) (hf : IsNilpotent f) (hg : IsNilpotent g) : (f.jordanPartition hf).Dominates (g.jordanPartition hg) ↔ ∀ (k : ℕ), finrank K ↥(g ^ k).range ≤ finrank K ↥(f ^ k).range

The Jordan partition of f dominates that of g exactly when, for every k, the rank of g ^ k is at most the rank of f ^ k.

@[simp]

theorem Module.End.jordanPartition_zero {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : jordanPartition 0 ⋯ = TauCeti.Nat.Partition.ones (finrank K V)

The zero operator has one part of size one for each dimension, including no parts on the zero-dimensional space.