Schur's bound for commuting matrices

Over any field, a subspace of n × n matrices whose elements commute pairwise has dimension at most ⌊n²/4⌋ + 1, and for n ≥ 1 the bound is attained by the identity together with the matrices [[0, X], [0, 0]] with X of size ⌈n/2⌉ × ⌊n/2⌋ (Theorem of the Day; Schur 1905, Jacobson 1944, short proof by Mirzakhani 1998).

Main results

• SchurCommuting.finrank_le: commuting subspaces of n × n matrices have dimension ≤ ⌊n²/4⌋ + 1
• SchurCommuting.exists_finrank_eq: the bound is attained for n ≥ 1
• SchurCommuting.finrank_le_and_attained: both together (Theorem of the Day)

References

• R. Whitty, Theorem of the Day, «Schur's Commuting Matrices Bound» (Algebra/SchurMatrix).
• I. Schur (1905); N. Jacobson, Schur's theorems on commutative matrices, Bull. AMS 50 (1944); M. Mirzakhani, A simple proof of a theorem of Schur, Amer. Math. Monthly 105 (1998) 260–262.

def SchurCommuting.Inv {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] (S : Submodule K (Module.End K V)) (W : Submodule K V) : Prop

W is stable under every element of S.

Equations

• SchurCommuting.Inv S W = ∀ s ∈ S, ∀ w ∈ W, s w ∈ W

theorem SchurCommuting.inv_range {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] {S : Submodule K (Module.End K V)} (hS : ∀ a ∈ S, ∀ b ∈ S, a * b = b * a) {a : Module.End K V} (ha : a ∈ S) : Inv S (LinearMap.range a)

theorem SchurCommuting.inv_ker {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] {S : Submodule K (Module.End K V)} (hS : ∀ a ∈ S, ∀ b ∈ S, a * b = b * a) {a : Module.End K V} (ha : a ∈ S) : Inv S (LinearMap.ker a)

theorem SchurCommuting.dual_lemma {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (P : Submodule K (Module.Dual K V)) (Q : Submodule K V) (h : ∀ f ∈ P, ∀ q ∈ Q, f q = 0) : Module.finrank K ↥P + Module.finrank K ↥Q ≤ Module.finrank K V

theorem SchurCommuting.key {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Submodule K (Module.End K V)) (hS : ∀ a ∈ S, ∀ b ∈ S, a * b = b * a) (H U : Submodule K V) (hUH : U ≤ H) (hUne : U ≠ ⊥) (hHtop : H ≠ ⊤) (hHmax : ∀ (W : Submodule K V), Inv S W → W ≠ ⊥ → W ≠ ⊤ → H ≤ W → W = H) (hUmin : ∀ (W : Submodule K V), Inv S W → W ≠ ⊥ → W ≤ U → W = U) (X Y : Submodule K ↥S) (hX : ∀ x ∈ X, ∀ (v : V), ↑x v ∈ U) (hY : ∀ y ∈ Y, ∀ h ∈ H, ↑y h = 0) : Module.finrank K ↥X + Module.finrank K ↥Y ≤ Module.finrank K V

noncomputable def SchurCommuting.quotHom {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] (S : Submodule K (Module.End K V)) (U : Submodule K V) (hU : Inv S U) : ↥S →ₗ[K] Module.End K (V ⧸ U)

Action on the quotient V ⧸ U.

Equations

• SchurCommuting.quotHom S U hU = { toFun := fun (s : ↥S) => U.mapQ U ↑s ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem SchurCommuting.quotHom_apply {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] (S : Submodule K (Module.End K V)) (U : Submodule K V) (hU : Inv S U) (s : ↥S) (v : V) : ((quotHom S U hU) s) (Submodule.Quotient.mk v) = Submodule.Quotient.mk (↑s v)

noncomputable def SchurCommuting.resHom {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] (S : Submodule K (Module.End K V)) (H : Submodule K V) (hH : Inv S H) : ↥S →ₗ[K] Module.End K ↥H

Restriction to an invariant subspace.

Equations

• SchurCommuting.resHom S H hH = { toFun := fun (s : ↥S) => LinearMap.restrict ↑s ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem SchurCommuting.resHom_apply {K : Type u_1} [Field K] {V : Type u} [AddCommGroup V] [Module K V] (S : Submodule K (Module.End K V)) (H : Submodule K V) (hH : Inv S H) (s : ↥S) (h : ↥H) : ↑(((resHom S H hH) s) h) = ↑s ↑h

theorem SchurCommuting.bmono {a b : ℕ} (h : a ≤ b) : a * a / 4 + 1 ≤ b * b / 4 + 1

theorem SchurCommuting.self_le (n : ℕ) : n ≤ n * n / 4 + 1

theorem SchurCommuting.arith (n d : ℕ) (hn : 1 ≤ n) (h : 2 * d ≤ n + 2 * ((n - 1) * (n - 1) / 4 + 1)) : d ≤ n * n / 4 + 1

theorem SchurCommuting.finrank_le_aux (K : Type u_1) [Field K] (n : ℕ) (V : Type u) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Module.finrank K V = n → ∀ (S : Submodule K (Module.End K V)), (∀ a ∈ S, ∀ b ∈ S, a * b = b * a) → Module.finrank K ↥S ≤ n * n / 4 + 1

@[reducible, inline]

abbrev SchurCommuting.Idx (n a : ℕ) : Type

Index set of the upper-right block: rows < a, columns ≥ a.

Equations

• SchurCommuting.Idx n a = { x : Fin n × Fin n // ↑x.1 < a ∧ a ≤ ↑x.2 }

noncomputable def SchurCommuting.blk (K : Type u_1) [Field K] (n a : ℕ) : Submodule K (Matrix (Fin n) (Fin n) K)

Matrices supported on the upper-right block.

Equations

• SchurCommuting.blk K n a = Submodule.span K (Set.range fun (x : SchurCommuting.Idx n a) => Matrix.single (↑x).1 (↑x).2 1)

theorem SchurCommuting.blk_mul_blk {K : Type u_1} [Field K] {n a : ℕ} {b₁ b₂ : Matrix (Fin n) (Fin n) K} (h₁ : b₁ ∈ blk K n a) (h₂ : b₂ ∈ blk K n a) : b₁ * b₂ = 0

theorem SchurCommuting.finrank_blk {K : Type u_1} [Field K] {n : ℕ} (a : ℕ) : Module.finrank K ↥(blk K n a) = min n a * (n - a)

theorem SchurCommuting.entry_zero_of_mem_blk {K : Type u_1} [Field K] {n a : ℕ} (ha : 0 < a) (hn : 0 < n) {b : Matrix (Fin n) (Fin n) K} (hb : b ∈ blk K n a) : b ⟨0, hn⟩ ⟨0, hn⟩ = 0

noncomputable def SchurCommuting.extremal (K : Type u_2) [Field K] (n a : ℕ) : Submodule K (Matrix (Fin n) (Fin n) K)

The extremal commutative subspace: scalars plus the upper-right block.

Equations

• SchurCommuting.extremal K n a = K ∙ 1 ⊔ SchurCommuting.blk K n a

theorem SchurCommuting.extremal_comm {K : Type u_1} [Field K] {n : ℕ} (a : ℕ) {A B : Matrix (Fin n) (Fin n) K} (hA : A ∈ extremal K n a) (hB : B ∈ extremal K n a) : A * B = B * A

theorem SchurCommuting.finrank_extremal {K : Type u_1} [Field K] {n : ℕ} (hn : 0 < n) {a : ℕ} (ha : 0 < a) : Module.finrank K ↥(extremal K n a) = min n a * (n - a) + 1

theorem SchurCommuting.exists_finrank_eq {K : Type u_1} [Field K] {n : ℕ} (hn : 1 ≤ n) : ∃ (S : Submodule K (Matrix (Fin n) (Fin n) K)), (∀ A ∈ S, ∀ B ∈ S, A * B = B * A) ∧ Module.finrank K ↥S = n ^ 2 / 4 + 1

The bound n ^ 2 / 4 + 1 is attained for n ≥ 1.

theorem SchurCommuting.finrank_le {K : Type u_1} [Field K] {n : ℕ} (S : Submodule K (Matrix (Fin n) (Fin n) K)) (hS : ∀ A ∈ S, ∀ B ∈ S, A * B = B * A) : Module.finrank K ↥S ≤ n ^ 2 / 4 + 1

Schur's bound: a commutative subspace of M_n(K) has dimension ≤ n ^ 2 / 4 + 1.

theorem SchurCommuting.finrank_le_and_attained (K : Type u_2) [Field K] (n : ℕ) : (∀ (S : Submodule K (Matrix (Fin n) (Fin n) K)), (∀ A ∈ S, ∀ B ∈ S, A * B = B * A) → Module.finrank K ↥S ≤ n ^ 2 / 4 + 1) ∧ (1 ≤ n → ∃ (S : Submodule K (Matrix (Fin n) (Fin n) K)), (∀ A ∈ S, ∀ B ∈ S, A * B = B * A) ∧ Module.finrank K ↥S = n ^ 2 / 4 + 1)