Derivations on quotient algebras

A derivation of an associative algebra descends to a quotient by a two-sided ideal exactly when it preserves that ideal. This file constructs that descent, out of the Lie subalgebra Ado.stableDerivations of derivations preserving the ideal, as a homomorphism of Lie algebras

Der(A, I) → Der(A ⧸ I).

The Lie-algebra packaging records that sums, scalar multiples, and commutators of derivations preserving I still preserve I. It lets a Lie algebra acting on A by derivations descend its action to A ⧸ I as soon as stability of I has been proved. In particular, derivations of a universal enveloping algebra can act on the finite quotients used to extend Lie representations.

Main definitions

• Ado.derivationQuotientHom: descent of stable derivations to the quotient algebra.
• Ado.stableInnerDerivation: the inner derivations, as a homomorphism of Lie algebras into the derivations preserving a two-sided ideal.

Implementation notes

The stabilizer Ado.stableDerivations of a submodule only uses the module structure of A, so it belongs to the core derivation API alongside derivationLieAlgebra; this file specialises it to I.restrictScalars R for a two-sided ideal I. Descent itself is Mathlib's action of a Lie algebra on the quotient of a Lie module by a stable Lie submodule, LieSubmodule.Quotient.actionAsEndoMap, with its codomain cut down to the derivations of A ⧸ I, in the same way that innerDerivation cuts down LieAlgebra.ad.

theorem Ado.innerDerivation_mem_stableDerivations (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] (z : A) : (innerDerivation R) z ∈ stableDerivations R (Submodule.restrictScalars R I)

Every inner derivation preserves a two-sided ideal.

def Ado.stableInnerDerivation (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] : A →ₗ⁅R⁆ ↥(stableDerivations R (Submodule.restrictScalars R I))

The inner derivations preserve a two-sided ideal: innerDerivation with its codomain cut down to the derivations preserving I, as a homomorphism of Lie algebras.

Equations

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

@[simp]

theorem Ado.coe_stableInnerDerivation (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] (z : A) : ↑((stableInnerDerivation R I) z) = (innerDerivation R) z

The stable inner derivation has the same underlying derivation as the ordinary inner derivation.

def Ado.derivationQuotientHom (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] : ↥(stableDerivations R (Submodule.restrictScalars R I)) →ₗ⁅R⁆ ↥(derivationLieAlgebra R (A ⧸ I))

Stable derivations descend to the quotient. The assignment sending a derivation of A that preserves the two-sided ideal I to its induced derivation of A ⧸ I, as a homomorphism of Lie algebras.

Equations

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

theorem Ado.derivationQuotientHom_comp_mkQ (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] (D : ↥(stableDerivations R (Submodule.restrictScalars R I))) : ↑((derivationQuotientHom R I) D) ∘ₗ (Submodule.restrictScalars R I).mkQ = (Submodule.restrictScalars R I).mkQ ∘ₗ ↑↑D

Descent commutes with the quotient map: applying a stable derivation before or after passing to A ⧸ I gives the same result.

@[simp]

theorem Ado.derivationQuotientHom_apply_mk (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] (D : ↥(stableDerivations R (Submodule.restrictScalars R I))) (x : A) : ↑((derivationQuotientHom R I) D) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk I) (↑↑D x)

The descended derivation evaluates on a quotient class by applying the original derivation to a representative.

@[simp]

theorem Ado.derivationQuotientHom_stableInnerDerivation (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] (z : A) : (derivationQuotientHom R I) ((stableInnerDerivation R I) z) = (innerDerivation R) ((Ideal.Quotient.mk I) z)

Descending the inner derivation by z gives the inner derivation by the image of z in the quotient.