Nilpotent Jordan Chains

Abstract

Actual positive-length Jordan chains and all iterate ranks for a nilpotent operator.

Theorem 1.1 (A chain basis computes every iterate rank).

$$\forall K\in Type,V\in Type,f\in \mathrm{End}\left(K,V\right),\left(\mathrm{Field}\left(K\right)\wedge \left(\mathrm{AddCommGroup}\left(V\right)\wedge \left(\mathrm{Module}\left(K,V\right)\wedge \left(\mathrm{FiniteDimensional}\left(K,V\right)\wedge \mathrm{IsNilpotent}\left(f\right)\right)\right)\right)\right)\Rightarrow \left(\exists I\in Type,hI\in \mathrm{Fintype}\left(I\right),s\in \mathrm{Function}\left(I,\mathrm{PNat}\left(\right)\right),b\in \mathrm{Basis}\left(\mathrm{Positions}\left(I,s\right),K,V\right),\left(\forall m\in \mathrm{Nat}\left(\right),i\in I,j\in \mathrm{Fin}\left(s\left(i\right)\right),\mathrm{apply}\left(\mathrm{pow}\left(f,m\right),b\left(i,j\right)\right)=\mathrm{ite}\left(\mathrm{add}\left(j,m\right)<s\left(i\right),b\left(i,\mathrm{add}\left(j,m\right)\right),0\right)\right)\wedge \left(\forall m\in \mathrm{Nat}\left(\right),\mathrm{finrank}\left(K,\mathrm{range}\left(\mathrm{pow}\left(f,m\right)\right)\right)=\sum _{i\in I}\mathrm{natSub}\left(s\left(i\right),m\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Eigenstructure/NilpotentJordanChains.nilpotent_jordan_chains_rank (✓ std3). ∎

Source. Repository-derived.

Commentary.

K is any field and V is a finite-dimensional K-vector space. The finite index type I may be empty; each s(i) is a positive natural. Positions(I,s) denotes the dependent sum of Fin(s(i)) over i in I. The basis is ordered along each chain toward its terminal zero. In the conditional formula b(i,j+m) is used only when j+m is below s(i). natSub is truncated natural subtraction.

Mathlib’s Module.torsion_by_prime_power_decomposition supplies the complete primary-decomposition induction over K[X]. Nilpotence makes Module.AEval’ f torsion by powers of X. AdjoinRoot.powerBasis’ gives the basis of each quotient K[X]/(X^s); polynomial linearity transports its shift to f. Removing empty quotient slots leaves positive lengths. The range of each iterate is proved equal to the span of the corresponding basis tails, whose independence computes its dimension. No algebraic closure, invariant complement, or preexisting Jordan basis is assumed.

References

• Truth anchor: D5/S1/Eigenstructure/NilpotentJordanChains.nilpotent_jordan_chains_rank