Evolution automorphisms and the tangent Lie algebra

Abstract

A natural SL3 realization identifies all infinitesimal automorphisms with derivations.

Definition 1.1 (automorphisms).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall V\in \mathrm{Type},[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(R,V\right)]\forall mu\in \mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(R\right),V,\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(R\right),V,V\right)\right),\mathrm{automorphisms}\left(mu\right)=\{g:\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(R\right),V,V\right)\mid \forall x\in V,\forall y\in V,g\left(mu\left(x,y\right)\right)=mu\left(g\left(x\right),g\left(y\right)\right)\}$$

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

All invertible linear maps preserving the given bilinear multiplication form a subgroup. No identity element or associativity of the multiplication is required.

Definition 1.2 (glCoordinates).

$$\forall degree\in \mathrm{Nat},\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall g\in \mathrm{Matrix}.\mathrm{GeneralLinearGroup}\left(\mathrm{Fin}\left(degree\right),R\right),\left(\forall i\in \mathrm{Fin}\left(degree\right),\forall j\in \mathrm{Fin}\left(degree\right),\mathrm{glCoordinates}\left(g\right)\left(\mathrm{Sum}.\mathrm{inl}\left((i,j)\right)\right)=(g:\mathrm{Matrix}\left(\mathrm{Fin}\left(degree\right),\mathrm{Fin}\left(degree\right),R\right))\left(i,j\right)\right)\wedge \left(\forall u\in \mathrm{Unit},\mathrm{glCoordinates}\left(g\right)\left(\mathrm{Sum}.\mathrm{inr}\left(u\right)\right)=\mathrm{val}\left(\mathrm{Inv}.\mathrm{inv}\left(\mathrm{Matrix}.\mathrm{GeneralLinearGroup}.\det \left(g\right)\right)\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionAutomorphismTangentBridge.glCoordinates (✓ 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 affine coordinates of GL consist of every matrix entry and the inverse determinant. The sum type adds one coordinate indexed by Unit.

Definition 1.3 (LinearAlgebraicGroup).

$$\forall k\in \mathrm{Type},[\mathrm{Field}\left(k\right)]\mathrm{LinearAlgebraicGroup}\left(k\right)=\{degree:\mathrm{Nat},equations:\mathrm{Set}\left(\mathrm{MvPolynomial}\left(\mathrm{Sum}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(degree\right),\mathrm{Fin}\left(degree\right)\right),\mathrm{Unit}\right),k\right)\right),points:\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)][\mathrm{Algebra}\left(k,R\right)]\mathrm{Subgroup}\left(\mathrm{Matrix}.\mathrm{GeneralLinearGroup}\left(\mathrm{Fin}\left(degree\right),R\right)\right)\mid (\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)][\mathrm{Algebra}\left(k,R\right)]\forall g\in \mathrm{Matrix}.\mathrm{GeneralLinearGroup}\left(\mathrm{Fin}\left(degree\right),R\right),g\in points\left(R\right)\iff \left(\forall p\in \mathrm{MvPolynomial}\left(\mathrm{Sum}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(degree\right),\mathrm{Fin}\left(degree\right)\right),\mathrm{Unit}\right),k\right),p\in equations\Rightarrow \mathrm{MvPolynomial}.{\mathrm{eval}}_2\left(\mathrm{algebraMap}\left(k,R\right),\mathrm{glCoordinates}\left(g\right),p\right)=0\right))\wedge (\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)][\mathrm{Algebra}\left(k,R\right)]\forall S\in \mathrm{Type},[\mathrm{CommRing}\left(S\right)][\mathrm{Algebra}\left(k,S\right)]\forall f\in \mathrm{AlgHom}\left(k,R,S\right),\forall g\in \mathrm{Matrix}.\mathrm{GeneralLinearGroup}\left(\mathrm{Fin}\left(degree\right),R\right),g\in points\left(R\right)\Rightarrow \mathrm{Matrix}.\mathrm{GeneralLinearGroup}.\mathrm{map}\left(f.\mathrm{toRingHom},g\right)\in points\left(S\right))\}$$

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

A closed matrix group consists of a degree, polynomial equations and subgroups over every commutative coefficient algebra. Membership is exactly their common zero locus, and matrix maps preserve membership. The two conditions after the vertical bar are the zero-locus and change-of-algebra fields.

Definition 1.4 (Realizes).

$$\forall k\in \mathrm{Type},[\mathrm{Field}\left(k\right)]\forall V\in \mathrm{Type},[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)]\forall G\in \mathrm{LinearAlgebraicGroup}\left(k\right),\forall mu\in \mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(k\right),V,\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(k\right),V,V\right)\right),\mathrm{Realizes}\left(G,mu\right)=\{equiv:\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)][\mathrm{Algebra}\left(k,R\right)]\mathrm{MulEquiv}\left(G.\mathrm{points}\left(R\right),\mathrm{automorphisms}\left(\mathrm{LinearMap}.\mathrm{BilinMap}.\mathrm{baseChange}\left(R,mu\right)\right)\right)\mid \forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)][\mathrm{Algebra}\left(k,R\right)]\forall S\in \mathrm{Type},[\mathrm{CommRing}\left(S\right)][\mathrm{Algebra}\left(k,S\right)]\forall f\in \mathrm{AlgHom}\left(k,R,S\right),\forall g\in G.\mathrm{points}\left(R\right),\forall x\in \mathrm{TensorProduct}\left(k,R,V\right),\mathrm{TensorProduct}.\mathrm{map}\left(f.\mathrm{toLinearMap},\mathrm{LinearMap}.\mathrm{id}\right)\left(\mathrm{val}\left(equiv\left(R,g\right)\right)\left(x\right)\right)=\mathrm{val}\left(equiv\left(S,⟨\mathrm{Matrix}.\mathrm{GeneralLinearGroup}.\mathrm{map}\left(f.\mathrm{toRingHom},\mathrm{val}\left(g\right)\right),G.\mathrm{mapMem}\left(R,S,f,\mathrm{val}\left(g\right),g.\mathrm{property}\right)⟩\right)\right)\left(\mathrm{TensorProduct}.\mathrm{map}\left(f.\mathrm{toLinearMap},\mathrm{LinearMap}.\mathrm{id}\right)\left(x\right)\right)\}$$

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

A realization consists of group equivalences over every commutative coefficient algebra, commuting with every algebra homomorphism on every tensor. TensorProduct.map uses the identity on V. This expresses an isomorphism of the full group-valued functors, including algebras with nilpotents.

Definition 1.5 (slGroup).

$$\forall n\in \mathrm{Nat},\mathrm{slGroup}\left(n\right)=\{\mathrm{degree}:=n,\mathrm{equations}:=\{\mathrm{Matrix}.\det \left((\mathrm{fun}i\mapsto (\mathrm{fun}j\mapsto \mathrm{MvPolynomial}.X\left(\mathrm{Sum}.\mathrm{inl}\left((i,j)\right)\right)))\right)-1\},\mathrm{points}:=\mathrm{fun}(R:\mathrm{Type})[\mathrm{CommRing}\left(R\right)][\mathrm{Algebra}\left(\mathrm{Complex},R\right)]\mapsto \mathrm{MonoidHom}.\ker \left(\mathrm{Matrix}.\mathrm{GeneralLinearGroup}.\det :\mathrm{MonoidHom}\left(\mathrm{Matrix}.\mathrm{GeneralLinearGroup}\left(\mathrm{Fin}\left(n\right),R\right),\mathrm{Units}\left(R\right)\right)\right)\}$$

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

The single equation det(X) − 1 defines SL at every coefficient algebra. Its points are the kernel of the determinant homomorphism on Matrix.GeneralLinearGroup. The remaining structure fields prove the zero-locus characterization and preservation under matrix maps.

Theorem 1.6 (tangent_lie_equivalence).

$$\forall V\in \mathrm{Type},[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(\mathrm{Complex},V\right)]\forall mu\in \mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(\mathrm{Complex}\right),V,\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(\mathrm{Complex}\right),V,V\right)\right),(\mathrm{Realizes}\left(\mathrm{slGroup}\left(3\right),mu\right)\to \mathrm{Nonempty}\left(\mathrm{LieEquiv}\left(\mathrm{Complex},\mathrm{LieAlgebra}.\mathrm{SpecialLinear}.\mathrm{sl}\left(\mathrm{Fin}\left(3\right),\mathrm{Complex}\right),\mathrm{derivations}\left(mu\right)\right)\right))$$

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

Dual-number coefficients reconstruct every derivation from a tangent automorphism. Addition is composition, scalar multiplication is substitution of epsilon, and the commutator over iterated dual numbers recovers the Lie bracket. Naturality therefore gives a complex Lie equivalence from trace-zero 3 by 3 matrices to all derivations.

References

• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionAutomorphismTangentBridge.LinearAlgebraicGroup
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionAutomorphismTangentBridge.Realizes
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionAutomorphismTangentBridge.automorphisms
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionAutomorphismTangentBridge.glCoordinates
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionAutomorphismTangentBridge.slGroup
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionAutomorphismTangentBridge.tangent_lie_equivalence
• Dependency: D5/S3/QuadraticForms/EvolutionAlgebras/DerivationAnnihilatorObstruction