Derivation blocks of nondegenerate evolution algebras

Abstract

Derivation blocks of nondegenerate evolution algebras.

Theorem 1.1 (Multiplication by a natural basis vector on the right).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)]\forall (V:\mathrm{Type}),([\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)]\forall (\mu :\mathrm{LinearMap}\left(k,V,\mathrm{LinearMap}\left(k,V,V\right)\right)),(\forall (\iota :\mathrm{Type}),(\forall (b:\mathrm{Module}.\mathrm{Basis}\left(\iota ,k,V\right)),((\forall (i:\iota ),(\forall (j:\iota ),((i\ne j)\Rightarrow (\mu \left(b\left(i\right),b\left(j\right)\right)=(0)))))\Rightarrow ([\mathrm{Fintype}\left(\iota \right)]\forall (x:V),(\forall (j:\iota ),(\mu \left(x,b\left(j\right)\right)=(b.\mathrm{repr}\left(x,j\right)\cdot \mu \left(b\left(j\right),b\left(j\right)\right))))))))))$$

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

Source. Repository-derived.

Commentary.

For a field k, a k-vector space V, a bilinear product mu and a finite natural basis b indexed by I, mu(x,b(j)) is the j-th coordinate of x times mu(b(j),b(j)). Expanding x in b eliminates every mixed product. The derivation equations and ideal arguments use this formula.

Theorem 1.2 (Multiplication by a natural basis vector on the left).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)]\forall (V:\mathrm{Type}),([\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)]\forall (\mu :\mathrm{LinearMap}\left(k,V,\mathrm{LinearMap}\left(k,V,V\right)\right)),(\forall (\iota :\mathrm{Type}),(\forall (b:\mathrm{Module}.\mathrm{Basis}\left(\iota ,k,V\right)),((\forall (i:\iota ),(\forall (j:\iota ),((i\ne j)\Rightarrow (\mu \left(b\left(i\right),b\left(j\right)\right)=(0)))))\Rightarrow ([\mathrm{Fintype}\left(\iota \right)]\forall (x:V),(\forall (i:\iota ),(\mu \left(b\left(i\right),x\right)=(b.\mathrm{repr}\left(x,i\right)\cdot \mu \left(b\left(i\right),b\left(i\right)\right))))))))))$$

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

Source. Repository-derived.

Commentary.

Under the same field, vector-space, bilinear-product, finite-index and natural-basis hypotheses, mu(b(i),x) is the i-th coordinate of x times mu(b(i),b(i)). This uses zero mixed products without assuming associativity or a unit.

Definition 1.3 (piLieRing).

$$\forall (\alpha :\mathrm{Type}),(\forall (H:(\alpha \to \mathrm{Type})),([\forall (a:\alpha ),(\mathrm{LieRing}\left(H\left(a\right)\right))]\mathrm{Pi}.\mathrm{piLieRing}\left(H\right):\mathrm{LieRing}\left(\forall (a:\alpha ),(H\left(a\right))\right)=(\{\mathrm{inferInstance}\left(\right):\mathrm{AddCommGroup}\left(\forall (a:\alpha ),(H\left(a\right))\right)\mathrm{with}\mathrm{bracket}:=(\mathrm{fun}f\mapsto (\mathrm{fun}g\mapsto (\mathrm{fun}a\mapsto \mathrm{Bracket}.\mathrm{bracket}\left(f\left(a\right),g\left(a\right)\right))))\})))$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.piLieRing (✓ 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.

The dependent product has the pointwise Lie bracket and the existing pointwise additive group. Its Lie identities hold at every coordinate.

Definition 1.4 (piLieAlgebra).

$$\forall (k:\mathrm{Type}),([\mathrm{CommRing}\left(k\right)]\forall (\alpha :\mathrm{Type}),(\forall (H:(\alpha \to \mathrm{Type})),([\forall (a:\alpha ),(\mathrm{LieRing}\left(H\left(a\right)\right))][\forall (a:\alpha ),(\mathrm{LieAlgebra}\left(k,H\left(a\right)\right))]\mathrm{Pi}.\mathrm{piLieAlgebra}\left(k,H\right):\mathrm{LieAlgebra}\left(k,\forall (a:\alpha ),(H\left(a\right))\right)=(\{(\mathrm{inferInstance}\left(\right):\mathrm{Module}\left(k,\forall (a:\alpha ),(H\left(a\right))\right))\mathrm{with}\}))))$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.piLieAlgebra (✓ 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.

The dependent product extends the existing pointwise module with the coordinatewise proof of compatibility between the Lie bracket and scalar multiplication. The record has no additional data fields.

Definition 1.5 (piDirectSumEquiv).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)]\forall (\beta :\mathrm{Type}),([\mathrm{Fintype}\left(\beta \right)]\forall (H:(\beta \to \mathrm{Type})),([\forall (a:\beta ),(\mathrm{LieRing}\left(H\left(a\right)\right))][\forall (a:\beta ),(\mathrm{LieAlgebra}\left(k,H\left(a\right)\right))]\mathrm{BlockLinear}.\mathrm{piDirectSumEquiv}\left(H\right)=(\{\mathrm{toLinearEquiv}:=\mathrm{DirectSum}.\mathrm{linearEquivFunOnFintype}\left(k,\beta ,H\right).\mathrm{symm}\}))))$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.piDirectSumEquiv (✓ 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.

For a finite index type, the standard linear equivalence from products to direct sums preserves the componentwise Lie bracket.

Definition 1.6 (blockW).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)]\forall (V:\mathrm{Type}),([\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)]\forall (\iota :\mathrm{Type}),(\forall (b:\mathrm{Module}.\mathrm{Basis}\left(\iota ,k,V\right)),(\forall (\alpha :\mathrm{Type}),(\forall (label:(\iota \to \alpha )),(\forall (w:(\alpha \to V)),(\forall (a:\alpha ),(\mathrm{Decomposition}.\mathrm{blockW}\left(b,label,w,a\right)=(\mathrm{Submodule}.\mathrm{span}\left(k,\mathrm{Set}.\mathrm{range}\left((\mathrm{fun}c\mapsto (\mathrm{fun}(i:\{i:\iota \mid label\left(i\right)=(a)\})\mapsto b.\mathrm{repr}\left(w\left(c\right),\mathrm{val}\left(i\right)\right)))\right)\right))))))))))$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.blockW (✓ 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.

The subspace in each block is spanned by the coordinate restrictions of all square representatives.

Definition 1.7 (squareRepresentative).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)]\forall (V:\mathrm{Type}),([\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)]\forall (\mu :\mathrm{LinearMap}\left(k,V,\mathrm{LinearMap}\left(k,V,V\right)\right)),(\forall (\iota :\mathrm{Type}),(\forall (b:\mathrm{Module}.\mathrm{Basis}\left(\iota ,k,V\right)),(\forall (a:\mathrm{Set}.\mathrm{range}\left((\mathrm{fun}i\mapsto k\cdot \mu \left(b\left(i\right),b\left(i\right)\right))\right)),(\mathrm{Rescaling}.\mathrm{squareRepresentative}\left(\mu ,b\right)\left(a\right)=(\mu \left(b\left(\mathrm{Classical}.\mathrm{choose}\left(a.\mathrm{property}\left(\right)\right)\right),b\left(\mathrm{Classical}.\mathrm{choose}\left(a.\mathrm{property}\left(\right)\right)\right)\right))))))))$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.squareRepresentative (✓ 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.

For each line spanned by a natural square, choose one basis index generating that line and take its square.

Theorem 1.8 (nonzero square block decomposition).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)]\forall (V:\mathrm{Type}),([\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)]\forall (\mu :\mathrm{LinearMap}\left(k,V,\mathrm{LinearMap}\left(k,V,V\right)\right)),([\mathrm{IsAlgClosed}\left(k\right)]\forall (\iota :\mathrm{Type}),([\mathrm{Fintype}\left(\iota \right)]\forall (b:\mathrm{Module}.\mathrm{Basis}\left(\iota ,k,V\right)),([\mathrm{LieAlgebra}.\mathrm{IsSemisimple}\left(k,\mathrm{derivations}\left(\mu \right)\right)](\forall (i:\iota ),(\forall (j:\iota ),((i\ne j)\Rightarrow (\mu \left(b\left(i\right),b\left(j\right)\right)=(0)))))\Rightarrow ((\forall (i:\iota ),(\mu \left(b\left(i\right),b\left(i\right)\right)\ne 0))\Rightarrow (\exists (b^{\prime }:\mathrm{Module}.\mathrm{Basis}\left(\iota ,k,V\right)),((\forall (i:\iota ),(\forall (j:\iota ),((i\ne j)\Rightarrow (\mu \left(b^{\prime }\left(i\right),b^{\prime }\left(j\right)\right)=(0)))))\wedge ((\forall (i:\iota ),(\mu \left(b^{\prime }\left(i\right),b^{\prime }\left(i\right)\right)=(\mathrm{Rescaling}.\mathrm{squareRepresentative}\left(\mu ,b\right)\left(\mathrm{Set}.\mathrm{rangeFactorization}\left((\mathrm{fun}i\mapsto k\cdot \mu \left(b\left(i\right),b\left(i\right)\right))\right)\left(i\right)\right))))\wedge (\mathrm{Nonempty}\left(\mathrm{LieEquiv}\left(k,\mathrm{derivations}\left(\mu \right),\mathrm{DirectSum}\left(\mathrm{Set}.\mathrm{range}\left((\mathrm{fun}i\mapsto k\cdot \mu \left(b\left(i\right),b\left(i\right)\right))\right),(\mathrm{fun}a\mapsto \mathrm{stabilizer}\left(\mathrm{Matrix}.{\mathrm{toLinearMap}}_2^{\prime }\left(k,1:\mathrm{Matrix}\left(\{i:\iota \mid \mathrm{Set}.\mathrm{rangeFactorization}\left((\mathrm{fun}i\mapsto k\cdot \mu \left(b\left(i\right),b\left(i\right)\right))\right)\left(i\right)=(a)\},\{i:\iota \mid \mathrm{Set}.\mathrm{rangeFactorization}\left((\mathrm{fun}i\mapsto k\cdot \mu \left(b\left(i\right),b\left(i\right)\right))\right)\left(i\right)=(a)\},k\right)\right),\mathrm{Decomposition}.\mathrm{blockW}\left(b^{\prime },\mathrm{Set}.\mathrm{rangeFactorization}\left((\mathrm{fun}i\mapsto k\cdot \mu \left(b\left(i\right),b\left(i\right)\right))\right),\mathrm{Rescaling}.\mathrm{squareRepresentative}\left(\mu ,b\right),a\right)\right))\right)\right)\right)))))))))))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.nonzero_square_block_decomposition (✓ 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.

Rescaling the natural basis makes squares identical within each proportionality class. Perfectness eliminates diagonal coefficients of derivations. Independent skew maps killing the projected squares then give all derivations, including the converse construction.

References

• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.blockW
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.mul_basis_left
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.mul_basis_right
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.nonzero_square_block_decomposition
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.piDirectSumEquiv
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.piLieAlgebra
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.piLieRing
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NondegenerateDerivationBlocks.squareRepresentative
• Dependency: D5/S3/QuadraticForms/EvolutionAlgebras/DerivationAnnihilatorObstruction
• Dependency: D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers