Ranks of powers on closures of conjugacy classes

For a square matrix Z and j r : ℕ, the condition rank (Z ^ j) ≤ r is Zariski closed, and closed in the usual topology over a field with continuous ring operations and closed points, such as ℂ (Matrix.rank_pow_le_of_mem_zeroLocus_vanishingIdeal, Matrix.isClosed_setOfPred_rank_pow_le).

Conjugation does not change the rank of any power, so the ranks of the powers can only drop on the closure of a conjugacy class: if Y lies in the closure of the GL n K-conjugacy class of X, then rank (Y ^ j) ≤ rank (X ^ j) for every j. For nilpotent matrices the ranks of the powers determine the Jordan type, and these inequalities are the necessary half of the description of nilpotent orbit closures by the dominance order on partitions. The statements are set-theoretic: the closures are taken in the K-points Matrix n n K, with the Zariski closure expressed through Mathlib's MvPolynomial.zeroLocus and MvPolynomial.vanishingIdeal.

Conversely, the elementary degenerations of Jordan types occur in orbit closures. Let Y be a matrix whose linear map has a Jordan-chain basis c, and let i ≠ j be two of its chains. With M the matrix of c.joinEnds i j, which links the end of chain i to the end of chain j, the matrices Y + t • M with t ≠ 0 all lie in the conjugacy class of Y + M. So Y lies in the closure of that class in the usual topology over a topological field in which 0 is not isolated, such as ℂ, and in its Zariski closure over any infinite field. For every k the rank of (Y + M) ^ k is the rank of Y ^ k plus one when len j ≤ k ≤ len i, and equals it otherwise. When len j ≤ len i the Jordan type of Y + M arises from that of Y by moving one box from the part len j to the part len i. Such moves generate the dominance order on partitions.

Chaining these degenerations gives Gerstenhaber's theorem: for a nilpotent matrix X, a matrix Y lies in the closure of the conjugacy class of X exactly when rank (Y ^ k) ≤ rank (X ^ k) for every k, equivalently when the Jordan partition of X dominates that of Y. Both closures are covered by one induction principle, Matrix.mem_of_forall_rank_pow_le: a set of matrices that contains the conjugacy class of X, and contains Y whenever it contains the conjugacy class of an elementary degeneration Y + M, contains every Y satisfying these rank inequalities.

Main results

• Matrix.rank_pow_le_of_mem_zeroLocus_vanishingIdeal_orbit and Matrix.rank_pow_le_of_mem_closure_orbit: on the Zariski closure, and on the topological closure, of the conjugacy class of X, the rank of every power is at most that of X.
• Matrix.mem_closure_orbit_add_toMatrix'_joinEnds and Matrix.mem_zeroLocus_vanishingIdeal_orbit_add_toMatrix'_joinEnds: Y lies in the closure of the conjugacy class of Y + M over a topological field in which 0 is not isolated, and in its Zariski closure over an infinite field.
• Matrix.rank_pow_add_smul_toMatrix'_joinEnds: the ranks of the powers of Y + t • M.
• Matrix.mem_of_forall_rank_pow_le: induction along elementary degenerations.
• Matrix.mem_closure_orbit_iff_forall_rank_pow_le and Matrix.mem_zeroLocus_vanishingIdeal_orbit_iff_forall_rank_pow_le: Gerstenhaber's theorem, the rank criterion for nilpotent orbit closures, in the usual and the Zariski topology.
• Matrix.mem_closure_orbit_iff_jordanPartition_dominates and Matrix.mem_zeroLocus_vanishingIdeal_orbit_iff_jordanPartition_dominates: the same criterion as dominance of Jordan partitions.

References

• M. Gerstenhaber, On dominance and varieties of commuting matrices, Ann. of Math. 73 (1961), 324–348.
• D. H. Collingwood and W. M. McGovern, Nilpotent Orbits in Semisimple Lie Algebras, Van Nostrand Reinhold, 1993, §6.2.

theorem Matrix.isNilpotent_of_forall_rank_pow_le {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {X Y : Matrix n n K} (hX : IsNilpotent X) (h : ∀ (k : ℕ), (Y ^ k).rank ≤ (X ^ k).rank) : IsNilpotent Y

If the ranks of all powers of Y are bounded by those of a nilpotent matrix X, then Y is nilpotent too.

theorem Matrix.rank_pow_le_of_mem_zeroLocus_vanishingIdeal_orbit {n : Type u_1} [Fintype n] [DecidableEq n] {k : Type u_2} {K : Type u_3} [Field k] [Field K] [Algebra k K] {X Y : Matrix n n K} (hY : Function.uncurry Y ∈ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal k (Function.uncurry '' MulAction.orbit (ConjAct (GL n K)) X))) (j : ℕ) : (Y ^ j).rank ≤ (X ^ j).rank

On the Zariski closure of the conjugacy class of X, the rank of every power is at most the rank of the same power of X.

theorem Matrix.rank_pow_le_of_mem_closure_orbit {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] {X Y : Matrix n n K} (hY : Y ∈ closure (MulAction.orbit (ConjAct (GL n K)) X)) (j : ℕ) : (Y ^ j).rank ≤ (X ^ j).rank

Over a field with continuous ring operations and closed points, on the closure of the conjugacy class of X the rank of every power is at most the rank of the same power of X.

theorem Matrix.add_smul_toMatrix'_joinEnds_mem_orbit {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {Y : Matrix n n K} {ι : Type u_3} [Finite ι] (c : Module.End.JordanChainBasis (toLin' Y) ι) {i j : ι} (hij : i ≠ j) {t : K} (ht : t ≠ 0) : Y + t • LinearMap.toMatrix' (c.joinEnds i j) ∈ MulAction.orbit (ConjAct (GL n K)) (Y + LinearMap.toMatrix' (c.joinEnds i j))

For t ≠ 0, the matrix Y + t • M, where M is the matrix of c.joinEnds i j for distinct chains i ≠ j, is conjugate to Y + M.

theorem Matrix.rank_pow_add_smul_toMatrix'_joinEnds {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {Y : Matrix n n K} {ι : Type u_3} [Finite ι] (c : Module.End.JordanChainBasis (toLin' Y) ι) {i j : ι} (hij : i ≠ j) {t : K} (ht : t ≠ 0) (k : ℕ) : ((Y + t • LinearMap.toMatrix' (c.joinEnds i j)) ^ k).rank = (Y ^ k).rank + 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 (Y + t • M) ^ k, where M is the matrix of c.joinEnds i j, is the rank of Y ^ k plus one when len j ≤ k ≤ len i, and equals it otherwise.

theorem Matrix.mem_closure_orbit_add_toMatrix'_joinEnds {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {Y : Matrix n n K} {ι : Type u_3} [TopologicalSpace K] [IsTopologicalRing K] [(nhdsWithin 0 {0}ᶜ).NeBot] (c : Module.End.JordanChainBasis (toLin' Y) ι) {i j : ι} (hij : i ≠ j) : Y ∈ closure (MulAction.orbit (ConjAct (GL n K)) (Y + LinearMap.toMatrix' (c.joinEnds i j)))

Elementary degenerations lie in orbit closures. Over a field with continuous ring operations in which 0 is not isolated, such as ℂ, a matrix Y lies in the closure of the conjugacy class of Y + M, where M is the matrix of c.joinEnds i j for distinct chains i ≠ j: it is the limit of the conjugates Y + t • M as t → 0.

theorem Matrix.mem_zeroLocus_vanishingIdeal_orbit_add_toMatrix'_joinEnds {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {Y : Matrix n n K} {ι : Type u_3} [Finite ι] {k : Type u_4} [Field k] [Algebra k K] [Infinite K] (c : Module.End.JordanChainBasis (toLin' Y) ι) {i j : ι} (hij : i ≠ j) : Function.uncurry Y ∈ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal k (Function.uncurry '' MulAction.orbit (ConjAct (GL n K)) (Y + LinearMap.toMatrix' (c.joinEnds i j))))

Elementary degenerations lie in Zariski orbit closures. Over an infinite field K, a matrix Y lies in the Zariski closure of the conjugacy class of Y + M, where M is the matrix of c.joinEnds i j for distinct chains i ≠ j, with polynomials taken over any subfield k.

theorem Matrix.mem_of_forall_rank_pow_le {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {X : Matrix n n K} (hX : IsNilpotent X) {S : Set (Matrix n n K)} (horbit : MulAction.orbit (ConjAct (GL n K)) X ⊆ S) (hdeg : ∀ (Y : Matrix n n K) (ι : Type) [Finite ι] (c : Module.End.JordanChainBasis (toLin' Y) ι) (i j : ι), i ≠ j → c.len j ≤ c.len i → MulAction.orbit (ConjAct (GL n K)) (Y + LinearMap.toMatrix' (c.joinEnds i j)) ⊆ S → Y ∈ S) {Y : Matrix n n K} (h : ∀ (k : ℕ), (Y ^ k).rank ≤ (X ^ k).rank) : Y ∈ S

Induction along elementary degenerations. Let X be nilpotent and let S be a set of matrices containing the conjugacy class of X. Suppose that S contains Y as soon as it contains the conjugacy class of Y + M, where M is the matrix of c.joinEnds i j for a Jordan-chain basis c of Y and distinct chains with len j ≤ len i. Then S contains every Y with rank (Y ^ k) ≤ rank (X ^ k) for all k.

theorem Matrix.mem_closure_orbit_iff_forall_rank_pow_le {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] [(nhdsWithin 0 {0}ᶜ).NeBot] {X Y : Matrix n n K} (hX : IsNilpotent X) : Y ∈ closure (MulAction.orbit (ConjAct (GL n K)) X) ↔ ∀ (k : ℕ), (Y ^ k).rank ≤ (X ^ k).rank

Gerstenhaber's theorem. Over a field with continuous ring operations and closed points in which 0 is not isolated, such as ℂ, a matrix Y lies in the closure of the conjugacy class of a nilpotent matrix X exactly when rank (Y ^ k) ≤ rank (X ^ k) for every k.

theorem Matrix.mem_zeroLocus_vanishingIdeal_orbit_iff_forall_rank_pow_le {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {k : Type u_3} [Field k] [Algebra k K] [Infinite K] {X Y : Matrix n n K} (hX : IsNilpotent X) : Function.uncurry Y ∈ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal k (Function.uncurry '' MulAction.orbit (ConjAct (GL n K)) X)) ↔ ∀ (j : ℕ), (Y ^ j).rank ≤ (X ^ j).rank

Gerstenhaber's theorem, Zariski form. Over an infinite field K, a matrix Y lies in the Zariski closure of the conjugacy class of a nilpotent matrix X, for polynomials over any subfield k, exactly when rank (Y ^ j) ≤ rank (X ^ j) for every j.

theorem Matrix.jordanPartition_dominates_jordanPartition_iff {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {X Y : Matrix n n K} (hX : IsNilpotent X) (hY : IsNilpotent Y) : (Module.End.jordanPartition (toLin' X) ⋯).Dominates (Module.End.jordanPartition (toLin' Y) ⋯) ↔ ∀ (k : ℕ), (Y ^ k).rank ≤ (X ^ k).rank

The Jordan partition of a nilpotent matrix X dominates that of a nilpotent matrix Y exactly when rank (Y ^ k) ≤ rank (X ^ k) for every k.

theorem Matrix.mem_closure_orbit_iff_jordanPartition_dominates {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] [(nhdsWithin 0 {0}ᶜ).NeBot] {X Y : Matrix n n K} (hX : IsNilpotent X) (hY : IsNilpotent Y) : Y ∈ closure (MulAction.orbit (ConjAct (GL n K)) X) ↔ (Module.End.jordanPartition (toLin' X) ⋯).Dominates (Module.End.jordanPartition (toLin' Y) ⋯)

Orbit closures and dominance. Over a field with continuous ring operations and closed points in which 0 is not isolated, such as ℂ, a nilpotent matrix Y lies in the closure of the conjugacy class of a nilpotent matrix X exactly when the Jordan partition of X dominates that of Y.

theorem Matrix.mem_zeroLocus_vanishingIdeal_orbit_iff_jordanPartition_dominates {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {k : Type u_3} [Field k] [Algebra k K] [Infinite K] {X Y : Matrix n n K} (hX : IsNilpotent X) (hY : IsNilpotent Y) : Function.uncurry Y ∈ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal k (Function.uncurry '' MulAction.orbit (ConjAct (GL n K)) X)) ↔ (Module.End.jordanPartition (toLin' X) ⋯).Dominates (Module.End.jordanPartition (toLin' Y) ⋯)

Zariski orbit closures and dominance. Over an infinite field K, a nilpotent matrix Y lies in the Zariski closure of the conjugacy class of a nilpotent matrix X, for polynomials over any subfield k, exactly when the Jordan partition of X dominates that of Y.