Commit 2026-01-25 15:24 069a2e0c
View on Github →feat: Defining Lie Rinehart algebras (#33690) This PR provides the basics of Lie-Rinehart algebras:
- Definition of the objects and homomorphism
- Composition of LR-homomorphisms is a homomorphisms
- Derivations of a commutative algebra are a Lie-Rinehart algebra
- The anchor map of a Lie Rinehart algebra is a Lie Rinehart morphism Lie Rinehart algebras are an important structure: They naturally appear in the context of Lie algebroids and singular foliations in differential geometry. They also permit do define de-Rham type cohomology theories in all of these cases. We are working on more of the theory of Lie-Rinehart algebras with Sven Holtrop (@stholtrop). (Maybe it would make sense to have a mathlib branch for further developments?)