Derivations of a non-associative algebra

A derivation of an algebra A is a linear map D obeying the Leibniz rule D (x * y) = D x * y + x * D y. Nothing in that rule asks the multiplication to be associative, commutative or unital, and the derivations of any algebra are closed under the commutator ⁅D, E⁆ = D ∘ E - E ∘ D, so they always form a Lie algebra Der A. Mathlib has this construction twice over, but only in special cases: Derivation R A M needs A commutative and associative, and LieDerivation R L M needs the multiplication to be a Lie bracket. Two of the exceptional Lie algebras are derivation algebras of algebras of neither kind -- G₂ = Der 𝕆 for the octonions (Ado.Octonion) and F₄ = Der H₃(𝕆) for the Albert algebra -- so this file builds Der A for an arbitrary non-unital non-associative algebra, and records that both Mathlib constructions are instances of it.

Main definitions

• Ado.derivationLieAlgebra R A: the derivations of A, as a Lie subalgebra of Module.End R A.
• Ado.innerDerivation: for an associative algebra, the inner derivations z ↦ ⁅z, -⁆, as a homomorphism of Lie algebras A →ₗ⁅R⁆ Der A.
• Ado.stableDerivations: the Lie subalgebra of derivations preserving a fixed submodule.
• Ado.stableDerivations.lieSubmodule: that submodule, as a Lie module over the derivations preserving it.
• Ado.derivationLieAlgebraCongr: an isomorphism of algebras induces an isomorphism of their derivation Lie algebras, by conjugation.

Main results

• Ado.derivationLieAlgebra.leibniz: the Leibniz rule; Ado.derivationLieAlgebra.apply_one_eq_zero: a derivation of a unital algebra kills the unit; and Ado.derivationLieAlgebra.apply_mul_eq_zero: its constants are closed under multiplication.
• Ado.ad_mem_derivationLieAlgebra_commutatorRing: the adjoint action of a Lie algebra is by derivations -- the Jacobi identity in Leibniz form; and Ado.ad_mem_derivationLieAlgebra: the same for the commutator of an associative algebra.
• Ado.derivationEquivDerivationLieAlgebra: for a commutative associative algebra, Der A is Mathlib's Derivation R A A with its Lie structure.
• Ado.derivationLieAlgebraCommutatorRingEquivLieDerivation: for a Lie algebra L, the derivations of the underlying non-associative algebra CommutatorRing L are Mathlib's LieDerivation R L L.

Implementation notes

Der A is a bundled Lie subalgebra of Module.End R A rather than a fresh carrier type with hand-built instances: the LieRing and LieAlgebra R structures, the Module R-structure, the action of Der A on A as a Lie module, and the lattice API then all come from Mathlib's LieSubalgebra, and the only thing left to prove is that the commutator of two derivations is a derivation. This is also why the base is a CommRing and A a NonUnitalNonAssocRing: a Lie ring is an additive group, so the semiring-level hypotheses under which the Leibniz rule still makes sense do not suffice to make Der A one.

The Leibniz rule is preserved by sums and by scalar multiples because the multiplication of A is R-bilinear, and by the commutator because the "second derivative" terms D (E x) * y and x * D (E y) that the composite D ∘ E contributes cancel against those of E ∘ D.

The Lie bracket of Module.End R A is the ring commutator, which Mathlib deliberately keeps out of the global instance set (LieRing.ofAssociativeRing) because it clashes with the module action; it is a local instance here, exactly as in Mathlib/Algebra/Lie/OfAssociative.lean. A file consuming derivationLieAlgebra needs the same attribute [local instance 100] LieRing.ofAssociativeRing line in order to state facts about Module.End R A as a Lie algebra, but not in order to use ↥(derivationLieAlgebra R A), whose own Lie structure is carried by the subalgebra.

The simp-normal form of the action of a derivation is the application (D : Module.End R A) x of the underlying linear map: Mathlib's LieSubalgebra.coe_bracket_of_module and Module.End.lie_apply already rewrite the Lie bracket ⁅D, x⁆ into it, and those two lemmas together with LieHom.lie_apply likewise evaluate the commutator ⁅D, E⁆ of two derivations, so no lemma of this file needs to say so.

The _apply and _symm_apply lemmas of derivationEquivDerivationLieAlgebra and derivationLieAlgebraCommutatorRingEquivLieDerivation are proved by rfl, and no rewriting lemma could replace it: those two equivalences are defined to be the identity on the underlying linear map, so the right-hand side of each lemma is literally the toFun/invFun field of the structure instance just above it. Mathlib proves the same shape the same way (LieEquiv.ofSubalgebras_apply, LinearEquiv.lieConj_apply). The point of stating them is precisely that no consumer then has to unfold the definition. The parentheses in (rfl) are the module system's: the definitions' bodies are not @[expose]d, so a bare rfl -- whose proof term is exported -- fails with "not a definitional equality", while the parenthesised form elaborates inside this module, where the bodies are visible. By contrast derivationLieAlgebraCongr is not the identity but a composite of LieEquiv.ofSubalgebras and LinearEquiv.lieConj, so its two lemmas are proved from those constructions' own apply lemmas rather than by unfolding.

References

• Highest-weight roadmap, Layer 8, whose derivationLieAlgebra this is: the derivation algebra through which the split octonions and the Albert algebra produce G₂ and F₄.
• N. Jacobson, Lie Algebras (1962), Chapter I, §2, and Chapter VII.

def Ado.derivationLieAlgebra (R : Type u) (A : Type v) [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : LieSubalgebra R (Module.End R A)

The derivation Lie algebra Der A of a non-unital non-associative R-algebra A: the R-linear maps D : A → A satisfying the Leibniz rule D (x * y) = D x * y + x * D y, a Lie subalgebra of Module.End R A under the commutator bracket.

Equations

• Ado.derivationLieAlgebra R A = { carrier := {D : Module.End R A | ∀ (x y : A), D (x * y) = D x * y + x * D y}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }

@[simp]

theorem Ado.mem_derivationLieAlgebra {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {D : Module.End R A} : D ∈ derivationLieAlgebra R A ↔ ∀ (x y : A), D (x * y) = D x * y + x * D y

@[simp]

theorem Ado.derivationLieAlgebra.leibniz {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (D : ↥(derivationLieAlgebra R A)) (x y : A) : ↑D (x * y) = ↑D x * y + x * ↑D y

The Leibniz rule: a derivation differentiates each factor of a product.

theorem Ado.derivationLieAlgebra.apply_mul_eq_zero {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {D : ↥(derivationLieAlgebra R A)} {x y : A} (hx : ↑D x = 0) (hy : ↑D y = 0) : ↑D (x * y) = 0

The constants of a derivation are closed under multiplication: if D kills x and y then it kills x * y. Together with linearity this says that the kernel of a derivation is an R-submodule of A closed under multiplication -- a subalgebra where A is unital and associative enough for Subalgebra to be available.

theorem Ado.derivationLieAlgebra.ext {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {D E : ↥(derivationLieAlgebra R A)} (h : ∀ (x : A), ↑D x = ↑E x) : D = E

A derivation is determined by its values.

theorem Ado.derivationLieAlgebra.ext_iff {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {D E : ↥(derivationLieAlgebra R A)} : D = E ↔ ∀ (x : A), ↑D x = ↑E x

def Ado.stableDerivations (R : Type u) {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (S : Submodule R A) : LieSubalgebra R ↥(derivationLieAlgebra R A)

The derivations of A that preserve the submodule S, as a Lie subalgebra of Der(A).

Equations

• Ado.stableDerivations R S = { carrier := {D : ↥(Ado.derivationLieAlgebra R A) | ∀ x ∈ S, ↑D x ∈ S}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }

@[simp]

theorem Ado.mem_stableDerivations (R : Type u) {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (S : Submodule R A) (D : ↥(derivationLieAlgebra R A)) : D ∈ stableDerivations R S ↔ ∀ x ∈ S, ↑D x ∈ S

Membership in stableDerivations R S means pointwise preservation of S.

def Ado.stableDerivations.lieSubmodule (R : Type u) {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (S : Submodule R A) : LieSubmodule R (↥(stableDerivations R S)) A

The submodule S, as a Lie submodule of A over the derivations preserving it. Through this Lie submodule, Mathlib equips the quotient A ⧸ S with its action by stable derivations.

Equations

• Ado.stableDerivations.lieSubmodule R S = { toSubmodule := S, lie_mem := ⋯ }

@[simp]

theorem Ado.stableDerivations.coe_lieSubmodule (R : Type u) {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (S : Submodule R A) : ↑(lieSubmodule R S) = S

The underlying submodule of stableDerivations.lieSubmodule R S is S.

@[simp]

theorem Ado.stableDerivations.mem_lieSubmodule (R : Type u) {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (S : Submodule R A) (x : A) : x ∈ lieSubmodule R S ↔ x ∈ S

Membership in stableDerivations.lieSubmodule R S is membership in S.

@[simp]

theorem Ado.derivationLieAlgebra.apply_one_eq_zero {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (D : ↥(derivationLieAlgebra R A)) : ↑D 1 = 0

A derivation of a unital algebra kills the unit: 1 = 1 * 1 forces D 1 = D 1 + D 1. Only unitality is used, not associativity.

theorem Ado.ad_mem_derivationLieAlgebra (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (z : A) : (LieAlgebra.ad R A) z ∈ derivationLieAlgebra R A

The commutator of an associative algebra acts by derivations: ad z : a ↦ ⁅z, a⁆ obeys the Leibniz rule, which for the commutator bracket is the associativity of the multiplication.

def Ado.innerDerivation (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] : A →ₗ⁅R⁆ ↥(derivationLieAlgebra R A)

The inner derivations of an associative algebra A: the assignment z ↦ ⁅z, -⁆, as a homomorphism of Lie algebras from A under its commutator bracket to Der A. It is the adjoint action LieAlgebra.ad with its codomain cut down to the derivations.

Equations

• Ado.innerDerivation R = { toFun := fun (z : A) => ⟨(LieAlgebra.ad R A) z, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem Ado.coe_innerDerivation (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (z : A) : ↑((innerDerivation R) z) = (LieAlgebra.ad R A) z

theorem Ado.lieConj_mem_derivationLieAlgebra {R : Type u} {A : Type v} {B : Type w} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] {e : A ≃ₗ[R] B} (he : ∀ (x y : A), e (x * y) = e x * e y) {D : Module.End R A} (hD : D ∈ derivationLieAlgebra R A) : e.lieConj D ∈ derivationLieAlgebra R B

Conjugation by a multiplicative linear equivalence carries derivations to derivations.

def Ado.derivationLieAlgebraCongr {R : Type u} {A : Type v} {B : Type w} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (e : A ≃ₗ[R] B) (he : ∀ (x y : A), e (x * y) = e x * e y) : ↥(derivationLieAlgebra R A) ≃ₗ⁅R⁆ ↥(derivationLieAlgebra R B)

Derivation algebras are transported along isomorphisms of algebras. A multiplicative R-linear equivalence e : A ≃ₗ[R] B conjugates derivations of A to derivations of B, and the resulting map is an isomorphism of Lie algebras. This is the tool that transports Der between two models of the same algebra -- two constructions of the split octonions, say.

Equations

• Ado.derivationLieAlgebraCongr e he = LieEquiv.ofSubalgebras (Ado.derivationLieAlgebra R A) (Ado.derivationLieAlgebra R B) e.lieConj ⋯

@[simp]

theorem Ado.derivationLieAlgebraCongr_apply {R : Type u} {A : Type v} {B : Type w} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (e : A ≃ₗ[R] B) (he : ∀ (x y : A), e (x * y) = e x * e y) (D : ↥(derivationLieAlgebra R A)) (x : B) : ↑((derivationLieAlgebraCongr e he) D) x = e (↑D (e.symm x))

@[simp]

theorem Ado.derivationLieAlgebraCongr_symm_apply {R : Type u} {A : Type v} {B : Type w} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (e : A ≃ₗ[R] B) (he : ∀ (x y : A), e (x * y) = e x * e y) (D : ↥(derivationLieAlgebra R B)) (x : A) : ↑((derivationLieAlgebraCongr e he).symm D) x = e.symm (↑D (e x))

def Ado.derivationEquivDerivationLieAlgebra {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] : Derivation R A A ≃ₗ⁅R⁆ ↥(derivationLieAlgebra R A)

Mathlib's Derivation R A A is Der A. For a commutative associative algebra the two Leibniz rules D (x * y) = D x * y + x * D y and D (x * y) = x • D y + y • D x say the same thing, and both Lie structures are the commutator of Module.End R A, so the identity on underlying linear maps is an isomorphism of Lie algebras.

Equations

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

@[simp]

theorem Ado.derivationEquivDerivationLieAlgebra_apply {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (D : Derivation R A A) (x : A) : ↑(derivationEquivDerivationLieAlgebra D) x = D x

@[simp]

theorem Ado.derivationEquivDerivationLieAlgebra_symm_apply {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (D : ↥(derivationLieAlgebra R A)) (x : A) : (derivationEquivDerivationLieAlgebra.symm D) x = ↑D x

theorem Ado.leibniz_add_iff_leibniz_sub {L : Type v} [LieRing L] {D : L → L} : (∀ (x y : L), D ⁅x, y⁆ = ⁅D x, y⁆ + ⁅x, D y⁆) ↔ ∀ (x y : L), D ⁅x, y⁆ = ⁅x, D y⁆ - ⁅y, D x⁆

The two spellings of the Leibniz rule on a Lie ring agree: the symmetric form ⁅D x, y⁆ + ⁅x, D y⁆ that derivationLieAlgebra inherits from the multiplication of CommutatorRing L, and the form ⁅x, D y⁆ - ⁅y, D x⁆ that LieDerivation is stated with because a Lie algebra carries no right action. They differ by skew symmetry alone, so neither linearity of D nor the base ring plays any part.

@[simp]

theorem Ado.mem_derivationLieAlgebra_commutatorRing_iff_apply_lie_eq_sub {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {D : Module.End R L} : D ∈ derivationLieAlgebra R (CommutatorRing L) ↔ ∀ (x y : L), D ⁅x, y⁆ = ⁅x, D y⁆ - ⁅y, D x⁆

Membership in Der (CommutatorRing L) is exactly the defining condition of a LieDerivation R L L. Regarding a Lie algebra as a non-associative algebra with x * y = ⁅x, y⁆ turns the defining condition of derivationLieAlgebra into D ⁅x, y⁆ = ⁅D x, y⁆ + ⁅x, D y⁆, which Ado.leibniz_add_iff_leibniz_sub rewrites into the skew form.

theorem Ado.ad_mem_derivationLieAlgebra_commutatorRing {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : (LieAlgebra.ad R L) x ∈ derivationLieAlgebra R (CommutatorRing L)

The adjoint action is by derivations: ad x lies in Der (CommutatorRing L), which is exactly the Jacobi identity in Leibniz form.

def Ado.derivationLieAlgebraCommutatorRingEquivLieDerivation {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ↥(derivationLieAlgebra R (CommutatorRing L)) ≃ₗ⁅R⁆ LieDerivation R L L

Mathlib's LieDerivation R L L is Der (CommutatorRing L). For the non-associative algebra underlying a Lie algebra the two Leibniz rules agree by Ado.mem_derivationLieAlgebra_commutatorRing_iff_apply_lie_eq_sub, and both Lie structures are the commutator of the endomorphism ring, so the identity on underlying linear maps is an isomorphism of Lie algebras.

Equations

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

@[simp]

theorem Ado.derivationLieAlgebraCommutatorRingEquivLieDerivation_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (D : ↥(derivationLieAlgebra R (CommutatorRing L))) (x : L) : (derivationLieAlgebraCommutatorRingEquivLieDerivation D) x = ↑D x

@[simp]

theorem Ado.derivationLieAlgebraCommutatorRingEquivLieDerivation_symm_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (x : L) : ↑(derivationLieAlgebraCommutatorRingEquivLieDerivation.symm D) x = D x