mathlib3 documentation

ring_theory.derivation.lie

Results #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Lie structures #

source
@[protected, instance]
def derivation.has_bracket {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] :
has_bracket (derivation R A A) (derivation R A A)

The commutator of derivations is again a derivation.

Equations
source
@[simp]
theorem derivation.commutator_coe_linear_map {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {D1 D2 : derivation R A A} :
↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆
source
theorem derivation.commutator_apply {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {D1 D2 : derivation R A A} (a : A) :
⇑⁅D1, D2⁆ a = ⇑D1 (⇑D2 a) - ⇑D2 (⇑D1 a)
source
@[protected, instance]
def derivation.lie_ring {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] :
lie_ring (derivation R A A)
Equations
source
@[protected, instance]
def derivation.lie_algebra {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] :
lie_algebra R (derivation R A A)
Equations