Orthogonal pointwise stabilizers

Abstract

Orthogonal pointwise stabilizers.

Definition 1.1 (stabilizer).

$$\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 (B:\mathrm{LinearMap}.\mathrm{BilinForm}\left(k,V\right)),(\forall (W:\mathrm{Submodule}\left(k,V\right)),(\mathrm{stabilizer}\left(B,W\right)=(\{f:\mathrm{Module}.\mathrm{End}\left(k,V\right)\mid (f\in \mathrm{skewAdjointLieSubalgebra}\left(B\right))\wedge (\forall (w:V),((w\in W)\Rightarrow (f\left(w\right)=(0))))\})))))$$

Formalization. D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.stabilizer (✓ 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.

This Lie subalgebra consists of skew-adjoint endomorphisms that vanish on the specified subspace.

Theorem 1.2 (quotientForm symm).

$$\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 (B:\mathrm{LinearMap}.\mathrm{BilinForm}\left(k,V\right)),(\forall (W:\mathrm{Submodule}\left(k,V\right)),(\forall (hB:B.\mathrm{IsSymm}\left(\right)),((\mathrm{LinearMap}.\mathrm{IsRefl}.{\mathrm{liftQ}}_2\left(B.\mathrm{restrict}\left(B.\mathrm{orthogonal}\left(W\right)\right),\mathrm{LinearMap}.\ker \left(B.\mathrm{restrict}\left(B.\mathrm{orthogonal}\left(W\right)\right)\right),(\mathrm{fun}x\mapsto (\mathrm{fun}y\mapsto hB.\mathrm{isRefl}\left(\mathrm{val}\left(x\right),\mathrm{val}\left(y\right)\right)))\right)).\mathrm{IsSymm}\left(\right))))))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.quotientForm_symm (✓ 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 form induced on the orthogonal subspace modulo its restricted radical is symmetric.

Theorem 1.3 (quotientForm nondegenerate).

$$\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 (B:\mathrm{LinearMap}.\mathrm{BilinForm}\left(k,V\right)),(\forall (W:\mathrm{Submodule}\left(k,V\right)),(\forall (hB:B.\mathrm{IsSymm}\left(\right)),((\mathrm{LinearMap}.\mathrm{IsRefl}.{\mathrm{liftQ}}_2\left(B.\mathrm{restrict}\left(B.\mathrm{orthogonal}\left(W\right)\right),\mathrm{LinearMap}.\ker \left(B.\mathrm{restrict}\left(B.\mathrm{orthogonal}\left(W\right)\right)\right),(\mathrm{fun}x\mapsto (\mathrm{fun}y\mapsto hB.\mathrm{isRefl}\left(\mathrm{val}\left(x\right),\mathrm{val}\left(y\right)\right)))\right)).\mathrm{Nondegenerate}\left(\right))))))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.quotientForm_nondegenerate (✓ 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 form induced on the orthogonal subspace modulo its restricted radical is nondegenerate.

Theorem 1.4 (stabilizer equiv of trivialRadical).

$$\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 (B:\mathrm{LinearMap}.\mathrm{BilinForm}\left(k,V\right)),(\forall (W:\mathrm{Submodule}\left(k,V\right)),(\forall (hB:B.\mathrm{IsSymm}\left(\right)),([\mathrm{FiniteDimensional}\left(k,V\right)](B.\mathrm{Nondegenerate}\left(\right))\Rightarrow ([\mathrm{LieAlgebra}.\mathrm{HasTrivialRadical}\left(k,\mathrm{stabilizer}\left(B,W\right)\right)]\mathrm{Nonempty}\left(\mathrm{LieEquiv}\left(k,\mathrm{stabilizer}\left(B,W\right),\mathrm{skewAdjointLieSubalgebra}\left(\mathrm{LinearMap}.\mathrm{IsRefl}.{\mathrm{liftQ}}_2\left(B.\mathrm{restrict}\left(B.\mathrm{orthogonal}\left(W\right)\right),\mathrm{LinearMap}.\ker \left(B.\mathrm{restrict}\left(B.\mathrm{orthogonal}\left(W\right)\right)\right),(\mathrm{fun}x\mapsto (\mathrm{fun}y\mapsto hB.\mathrm{isRefl}\left(\mathrm{val}\left(x\right),\mathrm{val}\left(y\right)\right)))\right)\right)\right)\right)))))))$$

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

Restriction to the orthogonal subspace and passage to its radical quotient give a Lie equivalence when the stabilizer has trivial solvable radical. The restriction kernel has vanishing triple products, and every quotient skew endomorphism extends by an orthogonal projection.

Theorem 1.5 (standardForm symm).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)]\forall (n:\mathrm{Type}),([\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)](\mathrm{Matrix}.{\mathrm{toLinearMap}}_2^{\prime }\left(k,1:\mathrm{Matrix}\left(n,n,k\right)\right)).\mathrm{IsSymm}\left(\right)))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.standardForm_symm (✓ 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 bilinear form of the identity matrix is symmetric.

Theorem 1.6 (skewAdjoint equiv so).

$$\forall (k:\mathrm{Type}),([\mathrm{Field}\left(k\right)]\forall (V:\mathrm{Type}),([\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(k,V\right)][\mathrm{FiniteDimensional}\left(k,V\right)][\mathrm{IsAlgClosed}\left(k\right)][\mathrm{CharZero}\left(k\right)]\forall (B:\mathrm{LinearMap}.\mathrm{BilinForm}\left(k,V\right)),((B.\mathrm{IsSymm}\left(\right))\Rightarrow ((B.\mathrm{Nondegenerate}\left(\right))\Rightarrow (\mathrm{Nonempty}\left(\mathrm{LieEquiv}\left(k,\mathrm{skewAdjointLieSubalgebra}\left(B\right),\mathrm{LieAlgebra}.\mathrm{Orthogonal}.\mathrm{so}\left(\mathrm{Fin}\left(\mathrm{Module}.\mathrm{finrank}\left(k,V\right)\right),k\right)\right)\right))))))$$

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

Over an algebraically closed field of characteristic zero, a finite-dimensional nondegenerate symmetric form has the standard orthogonal Lie algebra of its dimension.

References

• Truth anchor: D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.quotientForm_nondegenerate
• Truth anchor: D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.quotientForm_symm
• Truth anchor: D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.skewAdjoint_equiv_so
• Truth anchor: D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.stabilizer
• Truth anchor: D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.stabilizer_equiv_of_trivialRadical
• Truth anchor: D5/S3/QuadraticForms/OrthogonalPointwiseStabilizers.standardForm_symm