Papers With

← All papers
First page of Inhomogeneous deformations of $\mathfrak{osp}(N|2n)$: triviality for any number of odd parameters

Inhomogeneous deformations of $\mathfrak{osp}(N|2n)$: triviality for any number of odd parameters

Hisashi Aoi

math.RT Nov 8, 2026 · v1
formalization algebra mathlib
Read PDF arXiv abstract Code
TL;DR
The main results on odd deformations of osp(N|2n) are formalized in Lean 4 with Mathlib, defining the algebras by generators and relations, with a public GitHub artifact.
Abstract
We treat a symmetrized mixed-oscillator deformation family of the orthosymplectic Lie superalgebras $\mathfrak{osp}(N|2n)$, $N,n\geq1$, with even mixed coefficients $β_{u,i}$ and one odd square-zero parameter. We derive the deformed bracket from an oscillator realization, show that its coefficient is determined by the realization, and exhibit an explicit odd primitive, normalized by its vanishing on $\mathfrak{sp}(2n)$. Every odd primitive differs from it by a unique inner derivation. For $N=1$ this is the case $\mathfrak{osp}(1|2n)$ treated earlier. With multiple odd parameters the deformed bracket is the sum of the single-parameter deformations and is again trivial. The trivialization, however, is not additive: it is the product of the single-parameter trivializations followed by a nonsymplectic change of the bosonic generators. The main results are formalized in Lean 4, with the algebras constructed by generators and relations; what is not formalized is stated in the appendix.
Problem

The paper studies a symmetrized mixed-oscillator deformation family of the orthosymplectic Lie superalgebras osp(N|2n) with even mixed coefficients and odd square-zero parameters. It asks whether the resulting odd deformations are trivial and how they can be trivialized explicitly.

Approach

The deformed bracket is derived from an oscillator realization in an associative superalgebra presented by Weyl, Clifford and mixed relations. An untwisting isomorphism changes the generators, and comparing lifts gives the deformation coefficient as a coboundary. An explicit odd primitive is constructed, normalized to vanish on sp(2n), and extended to multiple odd parameters over a Grassmann algebra. Mathlib has no Lie superalgebras, so the Lean 4 development builds the algebras by generators and relations in its own terms.

Results

The deformation is trivial for every N, n and any number of odd parameters. Every odd primitive differs from the normalized one by a unique inner derivation. With several parameters the deformed bracket is additive, but the trivialization is not: it is a product of single-parameter trivializations followed by a nonsymplectic change of bosonic generators. These results are machine-checked in Lean v4.35.0 with Mathlib, and the parts not formalized are listed in an appendix.