FormalConjectures/Other/GerstenhaberThreeMatrices.lean

GitHub source file

3 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Gerstenhaber.finrank_adjoin_pair_le 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$ sorry line 51 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Field, Nat, Matrix, Fin, Commute, LE.le, Module.finrank, Subtype, Membership.mem, Subalgebra, Algebra.adjoin, Insert.insert, Set, Singleton.singleton

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   41 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   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
   …

2. theorem Gerstenhaber.finrank_adjoin_triple_le Documented declaration: finrank_adjoin_triple_le sorry line 61 source

   Source documentation

   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$?

   depends on sorry what this means

   Statement uses: Iff, True, Field, Nat, Matrix, Fin, Set.Pairwise, Insert.insert, Set, Singleton.singleton, Commute, LE.le, Module.finrank, Subtype, Membership.mem, Subalgebra, Algebra.adjoin

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   41 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   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
   …

3. theorem Gerstenhaber.exists_finrank_adjoin_quadruple_gt The analogue of Gerstenhaber's theorem fails for four pairwise commuting matrices: over any field there are four pairwise commuting line 76 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, Exists, Matrix, Fin, OfNat.ofNat, Nat, And, Set.Pairwise, Insert.insert, Set, Singleton.singleton, Commute, LT.lt, Module.finrank, Subtype, Membership.mem, Subalgebra, Algebra.adjoin

   Proof uses: Exists.intro, Matrix.single, And.intro, Ne, Eq, Or, Eq.mp, Eq.trans, congrArg, Commute.refl, Eq.symm, HMul.hMul, of_eq_true, True, congr, Matrix.single_mul_single_of_ne, of_decide_eq_true, id, Bool, Decidable.decide and 64 more

   137 instances, coercions and auxiliary constants left out.

   Tactic trace: 42 steps

   Open to load the checked before-and-after goal states.

   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
   …