Documentation

LeanPool.Ado.Algebra.Lie.UniversalEnveloping.Derivation.Basic

Lifting a Lie derivation to the enveloping algebra #

A derivation D of a Lie algebra L extends uniquely to a derivation Dᵁ of the associative algebra U(L), characterised by Dᵁ (ι x) = ι (D x) on the canonical Lie generators. This file constructs that extension and identifies the assignment D ↦ Dᵁ as a homomorphism of Lie algebras into the derivation algebra of U(L).

The construction #

Nothing but the universal property of U(L) is used. Write A[ε] = A ⊕ Aε for the dual numbers over an algebra A (Mathlib's DualNumber, the square-zero extension of A by itself), and send

x ↦ ι x + ε · ι (D x) : L → U(L)[ε].

The Leibniz rule D ⁅x, y⁆ = ⁅x, D y⁆ + ⁅D x, y⁆ says exactly that this map is a homomorphism of Lie algebras, because the ε-component of a commutator in A[ε] is the sum of the two commutators obtained by differentiating one factor at a time. So it lifts to an algebra homomorphism F : U(L) → U(L)[ε]; its 1-component is an algebra endomorphism of U(L) fixing the generators, hence the identity, and multiplicativity of F then reads, on ε-components, as the associative Leibniz rule for a ↦ (F a).snd. That map is Dᵁ.

The extension is unique because the canonical generators generate U(L) as an algebra (Ado.UniversalEnvelopingAlgebra.adjoin_range_ι) and the elements on which two derivations agree are closed under products and contain the scalars; this is Ado.UniversalEnvelopingAlgebra.derivation_ext, and it is what makes D ↦ Dᵁ additive, R-linear and bracket-preserving without any further computation.

Main definitions #

Main results #

Implementation notes #

envelopingDerivation is valued in the bundled derivation algebra Ado.derivationLieAlgebra R (U L) of TauCeti/Algebra/Lie/Derivation/Basic.lean rather than in the bare U L →ₗ[R] U L: that is the noncommutative derivation API this construction is meant to be read in (Mathlib's Derivation needs a commutative algebra, and LieDerivation needs a Lie bracket, so neither applies to U(L)). The bundling is also what lets D ↦ Dᵁ be a LieHom, since the target is a Lie algebra on the nose.

The canonical simp rule for Dᵁ (a * b) is the generic Ado.derivationLieAlgebra.leibniz, which holds of every bundled derivation; Ado.UniversalEnvelopingAlgebra.envelopingDerivation_mul is its specialisation to Dᵁ, stated under a name a reader of this file will look for because the Leibniz rule is the defining property of the extension, and carrying no simp tag of its own.

No lemma with UniversalEnvelopingAlgebra.ι on the left-hand side is a simp lemma here, for the reason recorded in TauCeti/Algebra/Lie/UniversalEnveloping/Basic.lean: simp rewrites ι through Mathlib's UniversalEnvelopingAlgebra.ι_apply, so such a left-hand side is not in simp-normal form. The primed variants are the simp-normal ones.

References #

Uniqueness of an extension #

source
theorem Ado.UniversalEnvelopingAlgebra.derivation_ext (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {D E : ↥(derivationLieAlgebra R (UniversalEnvelopingAlgebra R L))} (h : ∀ (x : L), ↑D ((UniversalEnvelopingAlgebra.ι R) x) = ↑E ((UniversalEnvelopingAlgebra.ι R) x)) :
D = E

A derivation of U(L) is determined by its values on the canonical Lie generators.

source
theorem Ado.UniversalEnvelopingAlgebra.derivation_ext_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {D E : ↥(derivationLieAlgebra R (UniversalEnvelopingAlgebra R L))} :
D = E ↔ ∀ (x : L), ↑D ((UniversalEnvelopingAlgebra.ι R) x) = ↑E ((UniversalEnvelopingAlgebra.ι R) x)

The extension #

source
noncomputable def Ado.UniversalEnvelopingAlgebra.envelopingDerivation (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) :
↥(derivationLieAlgebra R (UniversalEnvelopingAlgebra R L))

The extension of a Lie derivation to the enveloping algebra: the derivation Dᵁ of the associative algebra U(L) with Dᵁ (ι x) = ι (D x), the unique such derivation by Ado.UniversalEnvelopingAlgebra.derivation_ext.

Equations
Instances For
    source
    theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_mul (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (a b : UniversalEnvelopingAlgebra R L) :
    ↑(envelopingDerivation R L D) (a * b) = ↑(envelopingDerivation R L D) a * b + a * ↑(envelopingDerivation R L D) b

    The associative Leibniz rule for the extension: Dᵁ (a * b) = Dᵁ a * b + a * Dᵁ b.

    source
    theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (x : L) :
    ↑(envelopingDerivation R L D) ((UniversalEnvelopingAlgebra.ι R) x) = (UniversalEnvelopingAlgebra.ι R) (D x)

    The extension property: Dᵁ agrees with D on the canonical Lie generators. This is what pins down which derivation of U(L) the extension is, by Ado.UniversalEnvelopingAlgebra.derivation_ext.

    source
    @[simp]
    theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_ι' (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (x : L) :
    ↑(envelopingDerivation R L D) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = (UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) (D x))

    The simp-normal form of Ado.UniversalEnvelopingAlgebra.envelopingDerivation_ι, stated for the canonical generators as simp writes them.

    Ideals containing the range #

    source
    theorem Ado.UniversalEnvelopingAlgebra.derivation_range_le_iff (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (D : ↥(derivationLieAlgebra R (UniversalEnvelopingAlgebra R L))) (I : Ideal (UniversalEnvelopingAlgebra R L)) [I.IsTwoSided] :
    LinearMap.range ↑D ≤ Submodule.restrictScalars R I ↔ ∀ (x : L), ↑D ((UniversalEnvelopingAlgebra.ι R) x) ∈ I

    A derivation of U(L) has range in a two-sided ideal exactly when its values on the canonical generators do.

    source
    @[simp]
    theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_range_le_iff (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (I : Ideal (UniversalEnvelopingAlgebra R L)) [I.IsTwoSided] :
    LinearMap.range ↑(envelopingDerivation R L D) ≤ Submodule.restrictScalars R I ↔ ∀ (x : L), (UniversalEnvelopingAlgebra.ι R) (D x) ∈ I

    The range of a lifted derivation lies in a two-sided ideal exactly when its values on the canonical generators do. This reduces a range containment in U(L) to a condition checked on L alone.

    source
    theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_mem_stableDerivations_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (I : Ideal (UniversalEnvelopingAlgebra R L)) [I.IsTwoSided] (h : ∀ (x : L), (UniversalEnvelopingAlgebra.ι R) (D x) ∈ I) (n : ℕ) :
    envelopingDerivation R L D ∈ stableDerivations R (Submodule.restrictScalars R (I ^ n))

    If a two-sided ideal contains the values of a Lie derivation on the canonical enveloping generators, every power of that ideal is stable under the lifted derivation -- so the lift descends to each quotient U(L) ⧸ I ^ n along Ado.derivationQuotientHom.

    Functoriality in the derivation #

    source
    noncomputable def Ado.UniversalEnvelopingAlgebra.envelopingDerivationHom (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
    LieDerivation R L L →ₗ⁅R⁆ ↥(derivationLieAlgebra R (UniversalEnvelopingAlgebra R L))

    Lifting a Lie derivation to the enveloping algebra is a homomorphism of Lie algebras.

    Equations
    Instances For
      source
      @[simp]
      theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivationHom_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) :
      (envelopingDerivationHom R L) D = envelopingDerivation R L D

      Naturality #

      source
      theorem Ado.UniversalEnvelopingAlgebra.map_envelopingDerivation (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type w} [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (D : LieDerivation R L L) (E : LieDerivation R L' L') (hf : ∀ (x : L), f (D x) = E (f x)) (a : UniversalEnvelopingAlgebra R L) :
      (map R f) (↑(envelopingDerivation R L D) a) = ↑(envelopingDerivation R L' E) ((map R f) a)

      Naturality of the extension: a homomorphism of Lie algebras f : L → L' intertwining D with E induces an algebra homomorphism U(L) → U(L') intertwining Dᵁ with Eᵁ. Both sides are additive and multiplicative in the same way, so the identity is read off the extension property on the canonical generators.

      Inner derivations #

      source
      theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_inner (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
      envelopingDerivation R L ((LieDerivation.inner R L L) x) = -(innerDerivation R) ((UniversalEnvelopingAlgebra.ι R) x)

      The extension of an inner derivation is inner: the derivation of U(L) extending y ↦ ⁅y, x⁆ is the negative of the inner derivation of U(L) at the corresponding canonical generator. The sign is the one by which the two conventions differ: Mathlib's LieDerivation.inner is the right commutator ⁅-, x⁆ and Ado.innerDerivation is the left commutator ⁅ι x, -⁆. So the adjoint action of L on itself is carried to the adjoint action of U(L) on itself, and the extension is not merely some derivation agreeing with D on the generators.

      source
      theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_inner_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (a : UniversalEnvelopingAlgebra R L) :
      ↑(envelopingDerivation R L ((LieDerivation.inner R L L) x)) a = ⁅a, (UniversalEnvelopingAlgebra.ι R) x⁆

      The pointwise form of Ado.UniversalEnvelopingAlgebra.envelopingDerivation_inner: the derivation of U(L) extending y ↦ ⁅y, x⁆ is a ↦ ⁅a, ι x⁆.