Papers With

← All papers
First page of On the triviality of inhomogeneous deformations of $\mathfrak{osp}(1|2n)$

On the triviality of inhomogeneous deformations of $\mathfrak{osp}(1|2n)$

Hisashi Aoi

math.RT Apr 6, 2026 · v2
formalization algebra mathlib
Read PDF arXiv abstract Code
TL;DR
The main results are formalized and machine-checked in Lean 4 against a pinned Mathlib commit, with a public GitHub repository. Lie superalgebras are developed from scratch because Mathlib lacks them.
Abstract
We specify a symmetrized mixed-oscillator deformation family of $B(0,n)=\operatorname{osp}(1|2n)$, with even mixed coefficients and one odd square-zero parameter. For every $n\geq1$, we derive its bracket from a faithful oscillator realization and exhibit an odd cochain whose coboundary is the recovered deformation coefficient. The resulting even change of generators is an exact isomorphism over the exterior parameter algebra. For $n=1$, the cochain agrees with the normalization of Bakalov-Sullivan. We give the source relations and the even-central specialization explicitly, together with a Lean 4 formalization.
Problem

Bakalov–Sullivan gave a trivial deformation of osp(1|2) arising from inhomogeneous supersymmetric bilinear forms with an odd central parameter. The question is whether the analogous mixed-oscillator deformation of osp(1|2n) is trivial for every n, with an explicit primitive.

Approach

A deformation family over the universal ring R = P ⊕ κP is defined, with even parameters β_u and an odd square-zero κ. The deformed bracket is recovered from a faithful oscillator realization by untwisting the source algebra into a Weyl algebra tensor a Clifford-type factor. An explicit odd cochain f_β is then shown to have coboundary equal to the deformation coefficient. The results are formalized in Lean 4 with Mathlib, defining the needed Lie superalgebra structures since Mathlib has none.

Results

For every n ≥ 1 the deformation coefficient Γ_β equals δf_β. The map id + κf_β is an exact even isomorphism over the exterior parameter algebra. For n = 1 this recovers the Bakalov–Sullivan normalization. The Lean development is machine-checked using only the standard axioms, with stated exceptions.