Lie Algebra Structure on Derivations

Main statements

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

Lie structures

@[implicit_reducible]

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 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)

@[implicit_reducible]

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 = { toAddCommGroup := Derivation.instAddCommGroup, toBracket := Derivation.instBracket, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

@[implicit_reducible]

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 = { toModule := Derivation.instModule, lie_smul := ⋯ }

@[implicit_reducible]

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

Equations

• Derivation.instLieRingModule = { bracket := fun (X : Derivation R A A) (a : A) => X a, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

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

def Derivation.couple (R : Type u_1) [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] (A' : Type u_3) [CommRing A'] [Algebra R A'] [Algebra A A'] [IsScalarTower R A A'] : LieSubalgebra R (Derivation R A' A' × Derivation R A A)

Let σ : A → A' be a an homomorphism. A derivation d : A → A and a derivation d' : A' → A' are called compatible if d' ∘ σ = σ ∘ d. Couples of derivations with this property form a Lie subalgebra of all couples of derivations.

Equations

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

theorem Derivation.Compatible.mem {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {A' : Type u_3} [CommRing A'] [Algebra R A'] [Algebra A A'] [IsScalarTower R A A'] (x : Derivation R A' A' × Derivation R A A) : x ∈ couple R A A' ↔ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2

def Derivation.Compatible.mk {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {A' : Type u_3} [CommRing A'] [Algebra R A'] [Algebra A A'] [IsScalarTower R A A'] (x : Derivation R A' A') (y : Derivation R A A) (h : ⇑x ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑y) : ↥(couple R A A')

Generate an element of couple from x y satisfying the compatibility equation.

Equations

• Derivation.Compatible.mk x y h = ⟨(x, y), ⋯⟩

theorem Derivation.Compatible.mk_left {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {A' : Type u_3} [CommRing A'] [Algebra R A'] [Algebra A A'] [IsScalarTower R A A'] (x : Derivation R A' A') (y : Derivation R A A) (h : ⇑x ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑y) : (↑(mk x y h)).1 = x

theorem Derivation.Compatible.mk_right {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {A' : Type u_3} [CommRing A'] [Algebra R A'] [Algebra A A'] [IsScalarTower R A A'] (x : Derivation R A' A') (y : Derivation R A A) (h : ⇑x ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑y) : (↑(mk x y h)).2 = y

theorem Derivation.Compatible.apply {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {A' : Type u_3} [CommRing A'] [Algebra R A'] [Algebra A A'] [IsScalarTower R A A'] (x : ↥(couple R A A')) (a : A) : (↑x).1 ((Algebra.ofId A A') a) = (Algebra.ofId A A') ((↑x).2 a)