Results

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

Lie structures

instance Derivation.instBracketDerivationToCommSemiringToCommSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToModuleOfAssociativeRingToRingOfAssociativeAlgebraIdToModuleOfAssociativeAlgebra {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

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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 = let src := Derivation.instModule; LieAlgebra.mk (_ : ∀ (r : R) (d e : Derivation R A A), ⁅d, r • e⁆ = r • ⁅d, e⁆)