Theorems · Inductive type · nonassociative algebras

LieRinehartAlgebra

(R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing A] →
        [inst_1 : LieRing L] →
          [inst_2 : Module A L] →
            [inst_3 : LieRingModule L A] →
              [LieRinehartRing A L] → [inst_5 : CommRing R] → [Algebra R A] → [LieAlgebra R L] → Prop

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

Cited by

6 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

CommRingLieRingModuleLieRingModuleLieRinehartRingCommRingAlgebraLieAlgebra