Structures · Algebra

LieRinehartAlgebra

A Lie-Rinehart algebra with coefficients in a commutative ring R, is a pair consisting of a commutative R-algebra A and a Lie algebra L with coefficients in R, such that A and L are each a module over the other, satisfying compatibility conditions. As shown below, this data determines a linear map L → Derivation R A A satisfying a Leibniz-like compatibility condition. This could even be taken as a definition, however the definition here has the advantage of being Prop-valued, thus mitigating potential diamonds.

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Defs

Shape

3 explicit arguments