Results

• 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.

Equations

• Derivation.instBracket = { bracket := fun (D1 D2 : Derivation R A A) => Derivation.mk' ⁅↑D1, ↑D2⁆ ⋯ }

@[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] : LieRing (Derivation R A A)

Equations

• Derivation.instLieRing = LieRing.mk ⋯ ⋯ ⋯ ⋯

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

Equations

• Derivation.instLieAlgebra = LieAlgebra.mk ⋯