Semisimple derivation algebras are sums of orthogonal algebras

Abstract

Semisimple derivation algebras are sums of orthogonal algebras.

Theorem 1.1 (Zero diagonal coefficients).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)][\mathrm{CharZero}\left(k\right)]\forall (n:\mathrm{Type}),([\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall (A:\mathrm{LieAlgebra}.\mathrm{Orthogonal}.\mathrm{so}\left(n,k\right)),(\forall (i:n),(\mathrm{val}\left(A,i,i\right)=(0)))))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.diagonal_zero (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ivan Kaygorodov; Cándido Martín González; Antonio Viruel (2026). Evolution algebras: a survey of results and a list of open problems. DOI: 10.48550/arXiv.2610.22248. URL: https://arxiv.org/abs/2610.22248v1.

Commentary.

Every diagonal coefficient of an orthogonal Lie algebra matrix vanishes in characteristic zero.

Theorem 1.2 (Skew transpose coefficients).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)][\mathrm{CharZero}\left(k\right)]\forall (n:\mathrm{Type}),([\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall (A:\mathrm{LieAlgebra}.\mathrm{Orthogonal}.\mathrm{so}\left(n,k\right)),(\forall (i:n),(\forall (j:n),(\mathrm{val}\left(A,j,i\right)=(-\mathrm{val}\left(A,i,j\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.coefficient_skew (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ivan Kaygorodov; Cándido Martín González; Antonio Viruel (2026). Evolution algebras: a survey of results and a list of open problems. DOI: 10.48550/arXiv.2610.22248. URL: https://arxiv.org/abs/2610.22248v1.

Commentary.

Transposing the indices negates each coefficient of an orthogonal Lie algebra matrix.

Definition 1.3 (claim).

$$\mathrm{claim}=(\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)][\mathrm{IsAlgClosed}\left(k\right)][\mathrm{CharZero}\left(k\right)]\forall (V:\mathrm{Type}),([\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)][\mathrm{FiniteDimensional}\left(k,V\right)]\forall (\mu :\mathrm{LinearMap}\left(k,V,\mathrm{LinearMap}\left(k,V,V\right)\right)),((\mathrm{IsEvolutionAlgebra}\left(\mu \right))\Rightarrow ((\mathrm{LieAlgebra}.\mathrm{IsSemisimple}\left(k,\mathrm{derivations}\left(\mu \right)\right))\Rightarrow (\exists (r:\mathbb{N}),(\exists (m:(\mathrm{Fin}\left(r\right)\to \mathbb{N})),((\forall (i:\mathrm{Fin}\left(r\right)),(3\le m\left(i\right)))\wedge (\mathrm{Nonempty}\left(\mathrm{LieEquiv}\left(k,\mathrm{derivations}\left(\mu \right),\mathrm{DirectSum}\left(\mathrm{Fin}\left(r\right),(\mathrm{fun}i\mapsto \mathrm{LieAlgebra}.\mathrm{Orthogonal}.\mathrm{so}\left(\mathrm{Fin}\left(m\left(i\right)\right),k\right))\right)\right)\right))))))))))$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.claim (✓ std3).

Citation. Ivan Kaygorodov; Cándido Martín González; Antonio Viruel (2026). Evolution algebras: a survey of results and a list of open problems. DOI: 10.48550/arXiv.2610.22248. URL: https://arxiv.org/abs/2610.22248v1.

Commentary.

Conjecture 5 (Semisimple derivation algebras), p. 28: “Let k be algebraically closed of characteristic 0. If Der(A) is semisimple for a finite-dimensional evolution algebra A, then Der(A) ≅ ⊕ᵢ so_{mᵢ} with mᵢ ≥ 3.” The field k and vector space V are arbitrary; μ is the bilinear product, and r = 0 permits the zero Lie algebra.

Theorem 1.4 (result).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)][\mathrm{IsAlgClosed}\left(k\right)][\mathrm{CharZero}\left(k\right)]\forall (V:\mathrm{Type}),([\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)][\mathrm{FiniteDimensional}\left(k,V\right)]\forall (\mu :\mathrm{LinearMap}\left(k,V,\mathrm{LinearMap}\left(k,V,V\right)\right)),((\mathrm{IsEvolutionAlgebra}\left(\mu \right))\Rightarrow ((\mathrm{LieAlgebra}.\mathrm{IsSemisimple}\left(k,\mathrm{derivations}\left(\mu \right)\right))\Rightarrow (\exists (r:\mathbb{N}),(\exists (m:(\mathrm{Fin}\left(r\right)\to \mathbb{N})),((\forall (i:\mathrm{Fin}\left(r\right)),(3\le m\left(i\right)))\wedge (\mathrm{Nonempty}\left(\mathrm{LieEquiv}\left(k,\mathrm{derivations}\left(\mu \right),\mathrm{DirectSum}\left(\mathrm{Fin}\left(r\right),(\mathrm{fun}i\mapsto \mathrm{LieAlgebra}.\mathrm{Orthogonal}.\mathrm{so}\left(\mathrm{Fin}\left(m\left(i\right)\right),k\right))\right)\right)\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.result (✓ std3). ∎

Resolves. Problems/kaygorodov-martin-gonzalez-viruel-2026-evolution-algebra-derivations-conjecture-5 (proved) by D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.result.

Source. Repository-derived.

Acknowledgement. Ivan Kaygorodov; Cándido Martín González; Antonio Viruel (2026). Evolution algebras: a survey of results and a list of open problems. DOI: 10.48550/arXiv.2610.22248. URL: https://arxiv.org/abs/2610.22248v1.

Commentary.

The annihilator obstruction removes zero natural squares. The block decomposition identifies all derivations with independent orthogonal pointwise stabilizers. Their radical quotients give standard orthogonal algebras. Dimensions zero and one contribute zero, and dimension two is excluded by its nonzero abelian algebra. The remaining factors have dimension at least three.

References

• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.claim
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.coefficient_skew
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.diagonal_zero
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/SemisimpleDerivationClassification.result
• Dependency: D5/S3/QuadraticForms/EvolutionAlgebras/DerivationAnnihilatorObstruction
• Dependency: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks
• Dependency: D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers