Documentation

Mathlib.RingTheory.Derivation.Lie

Results #

Lie structures #

instance Derivation.instBracket {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] :
Bracket (Derivation R A A) (Derivation R A A)

The commutator of derivations is again a derivation.

Equations
@[simp]
theorem Derivation.commutator_coe_linear_map {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {D1 : Derivation R A A} {D2 : Derivation R A A} :
D1, D2 = D1, D2
theorem Derivation.commutator_apply {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {D1 : Derivation R A A} {D2 : Derivation R A A} (a : A) :
D1, D2 a = D1 (D2 a) - D2 (D1 a)
instance Derivation.instLieRing {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] :
Equations
instance Derivation.instLieAlgebra {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] :
Equations
  • Derivation.instLieAlgebra = let __src := Derivation.instModule; LieAlgebra.mk