Theorems · Definition · nonassociative algebras

LieRinehartAlgebra.anchor

(R : Type u_1) →
  (A₁ : Type u_2) →
    (L₁ : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A₁] →
          [inst_2 : LieRing L₁] →
            [inst_3 : Module A₁ L₁] →
              [inst_4 : LieRingModule L₁ A₁] →
                [inst_5 : Algebra R A₁] →
                  [inst_6 : LieAlgebra R L₁] →
                    [inst_7 : LieRinehartRing A₁ L₁] →
                      [LieRinehartAlgebra R A₁ L₁] → LieRinehartAlgebra.Hom (AlgHom.id R A₁) L₁ (Derivation R A₁ A₁)

The anchor of a given Lie-Rinehart algebra L over A interpreted as a Lie-Rinehart morphism to the module of derivations of A.

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Defs

Cited by

2 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingLieRingModuleLieRingModuleAlgebraLieAlgebraLieRinehartRingLieRinehartAlgebra