The Gerstenhaber problem for three commuting matrices

/-
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.
-/

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](https://arxiv.org/abs/2402.16334), M. Satriano and W. Zhang,
  *On the algebra generated by three commuting matrices: combinatorial cases*.
- [arXiv:2006.08588](https://arxiv.org/abs/2006.08588), J. Holbrook and M. Omladič,
  *A computing strategy and programs to resolve the Gerstenhaber Problem for
  commuting triples of matrices*.
-/

namespace Gerstenhaber

variable {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 := by
  sorry

/--
**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 := by
  sorry

/--
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$.
-/
@[category research solved, AMS 15 16]
theorem exists_finrank_adjoin_quadruple_gt (K : Type*) [Field K] :
    ∃ A B C D : Matrix (Fin 4) (Fin 4) K,
      ({A, B, C, D} : Set (Matrix (Fin 4) (Fin 4) K)).Pairwise Commute ∧
      4 < Module.finrank K (Algebra.adjoin K {A, B, C, D}) := by
  sorry

end Gerstenhaber

• Formalization source ↗

On-site verification needs an executable Lean target. None is attached yet.

A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.