1. FormalConjectures
  2. Other
  3. GerstenhaberThreeMatrices
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import FormalConjecturesUtil

The Gerstenhaber problem for three commuting matrices

Gerstenhaber proved in 1961 [Ger61] that the unital algebra generated by two commuting $n \times n$ matrices over a field has dimension at most $n$. It is an open problem, known as the Gerstenhaber problem, whether the same bound holds for three pairwise commuting matrices. The bound fails for four or more pairwise commuting matrices.

References:

    [Ger61] M. Gerstenhaber, On dominance and varieties of commuting matrices. Annals of Mathematics (2) 73 (1961), no. 2, 324–348. https://doi.org/10.2307/1970336

    arXiv:2402.16334, M. Satriano and W. Zhang, On the algebra generated by three commuting matrices: combinatorial cases.

    arXiv:2006.08588, J. Holbrook and M. Omladič, A computing strategy and programs to resolve the Gerstenhaber Problem for commuting triples of matrices.

@[expose] public sectionnamespace Gerstenhabervariable {K : Type*} [Field K] {n : ℕ}

Gerstenhaber's theorem [Ger61]: if $A$ and $B$ are commuting $n \times n$ matrices over a field $K$, then the unital $K$-algebra $K[A, B]$ they generate has dimension at most $n$.

@[category research solved, AMS 15 16] theorem finrank_adjoin_pair_le (A B : Matrix (Fin n) (Fin n) K) (hAB : Commute A B) : Module.finrank K (Algebra.adjoin K {A, B}) ≤ n := K:Type u_1inst✝:Field Kn:ℕA:Matrix (Fin n) (Fin n) KB:Matrix (Fin n) (Fin n) KhAB:Commute A B⊢ Module.finrank K ↥K[A, B] ≤ n All goals completed! 🐙

The Gerstenhaber problem: if $A$, $B$, and $C$ are pairwise commuting $n \times n$ matrices over a field $K$, is the dimension of the unital $K$-algebra $K[A, B, C]$ they generate always at most $n$?

@[category research open, AMS 15 16] theorem finrank_adjoin_triple_le : answer(sorry) ↔ ∀ (K : Type*) [Field K] (n : ℕ) (A B C : Matrix (Fin n) (Fin n) K), ({A, B, C} : Set (Matrix (Fin n) (Fin n) K)).Pairwise Commute → Module.finrank K (Algebra.adjoin K {A, B, C}) ≤ n := ⊢ True ↔ ∀ (K : Type u_2) [inst : Field K] (n : ℕ) (A B C : Matrix (Fin n) (Fin n) K), {A, B, C}.Pairwise Commute → Module.finrank K ↥K[A, B, C] ≤ n All goals completed! 🐙

The analogue of Gerstenhaber's theorem fails for four pairwise commuting matrices: over any field there are four pairwise commuting $4 \times 4$ matrices generating a unital algebra of dimension greater than $4$. The standard example is $e_{13}, e_{14}, e_{23}, e_{24}$, whose pairwise products all vanish, so the algebra they generate has dimension $5$.

K:Type u_2inst✝:Field KS:Subalgebra K (Matrix (Fin 4) (Fin 4) K) := K[Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]hS:S = K[Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]v:Fin 5 → Matrix (Fin 4) (Fin 4) K := ![1, Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]hv:∀ (i : Fin 5), v i ∈ Shw:LinearIndependent K fun i ↦ ⟨v i, ⋯⟩⊢ 4 < Module.finrank K ↥S K:Type u_2inst✝:Field KS:Subalgebra K (Matrix (Fin 4) (Fin 4) K) := K[Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]hS:S = K[Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]v:Fin 5 → Matrix (Fin 4) (Fin 4) K := ![1, Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]hv:∀ (i : Fin 5), v i ∈ Shw:LinearIndependent K fun i ↦ ⟨v i, ⋯⟩this:Fintype.card (Fin 5) ≤ Module.finrank K ↥S⊢ 4 < Module.finrank K ↥S K:Type u_2inst✝:Field KS:Subalgebra K (Matrix (Fin 4) (Fin 4) K) := K[Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]hS:S = K[Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]v:Fin 5 → Matrix (Fin 4) (Fin 4) K := ![1, Matrix.single 0 2 1, Matrix.single 0 3 1, Matrix.single 1 2 1, Matrix.single 1 3 1]hv:∀ (i : Fin 5), v i ∈ Shw:LinearIndependent K fun i ↦ ⟨v i, ⋯⟩this:5 ≤ Module.finrank K ↥S⊢ 4 < Module.finrank K ↥S All goals completed! 🐙end Gerstenhaber