Lie Algebra Structure on Derivations

Main statements

• Derivation.instLieAlgebra: The R-derivations from A to A form a Lie algebra over R.

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.

@[simp]

theorem Derivation.commutator_coe_linear_map {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {D1 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 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] : LieRing (Derivation R A A)

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

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

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

@[simp]

theorem Derivation.bracket_eq_fun {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] (X : Derivation R A A) (a : A) : ⁅X, a⁆ = X a