Formalising Weyl Algebras / D-Modules

Stream: maths

[Hongyu Wang]

Hi everyone!

I'm an undergraduate working on a thesis about $\mathcal{D}$-module theory (algebraic geometry / representation theory side). I'd like to formalise core definitions and basic properties in Lean 4 as a thesis appendix, using Coutinho's A Primer of Algebraic D-Modules as my primary reference.

Given time constraints and the current Mathlib status, I am planning to focus on the affine case (the Weyl algebra $A_n(k)$) rather than the full sheaf-theoretic setting.

I found Mathlib.RingTheory.Derivation, but this covers first-order derivations rather than the full ring of differential operators. I haven't found an existing formalisation of the Weyl algebra itself.

Design options I'm weighing:

1.  Define $A_1(k) = k\langle x, \partial \rangle / (\partial x - x\partial - 1)$ using FreeAlgebra and RingQuot.

2.  Define $A_1(k)$ as the subalgebra of Module.End k (Polynomial k) generated by multiplication-by-$X$ and formal differentiation. (Note: This representation is not faithful when $\operatorname{char}(k) > 0$.)

3.  Define $A_1(k)$ as a skew polynomial ring $k[x][\partial; \sigma, \delta]$ (where $\delta$ is the standard derivative).

Questions:

1. Is formalising the Weyl algebra currently achievable in Lean/Mathlib? Are there any known blockers (e.g., gaps in infrastructure for non-commutative quotients via RingQuot)?
2. Is formalising just the affine case (Weyl algebra + modules over it) a meaningful contribution for the community, or would it be too narrow without the sheaf-theoretic generality?
3. Which option above (or alternative abstraction) would be easiest to work with and most amenable to future generalisation (e.g., $A_n(k)$, or eventually $\mathcal{D}_X$ on schemes)?
4. Are there any experimental branches, ongoing projects, or files I should look at before starting?

Any advice on scoping or entry points would be very helpful. Thanks!

[Scott Carnahan]

I would be very happy to see a formalization of the Weyl algebra in Mathlib4. You may want to look at the existing work on Clifford algebras for hints.

[Eric Wieser]

Perhaps something like

import Mathlib


variable {R V} [CommRing R] [AddCommGroup V] [Module R V] (B : V →ₗ[R] V →ₗ[R] R)

open TensorAlgebra in
inductive WeylAlgebra.Rel : TensorAlgebra R V → TensorAlgebra R V → Prop where
  | intro (v w : V) : Rel (ι R v * ι R w - ι R w * ι R v) (algebraMap R _ (B v w))

def WeylAlgebra := RingQuot (WeylAlgebra.Rel B)