Documentation

Mathlib.Algebra.Lie.Derivation.Basic

Lie derivations #

This file defines Lie derivations and establishes some basic properties.

Main definitions #

Main statements #

Implementation notes #

structure LieDerivation (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] extends LinearMap :
Type (max u_2 u_3)

A Lie derivation D from the Lie R-algebra L to the L-module M is an R-linear map that satisfies the Leibniz rule D [a, b] = [a, D b] - [b, D a].

  • toFun : LM
  • map_add' : ∀ (x y : L), (self).toFun (x + y) = (self).toFun x + (self).toFun y
  • map_smul' : ∀ (m : R) (x : L), (self).toFun (m x) = (RingHom.id R) m (self).toFun x
  • leibniz' : ∀ (a b : L), self a, b = a, self b - b, self a
Instances For
    theorem LieDerivation.leibniz' {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (self : LieDerivation R L M) (a : L) (b : L) :
    self a, b = a, self b - b, self a
    instance LieDerivation.instFunLike {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
    Equations
    • LieDerivation.instFunLike = { coe := fun (D : LieDerivation R L M) => (D).toFun, coe_injective' := }
    instance LieDerivation.instLinearMapClass {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
    Equations
    • =
    theorem LieDerivation.toFun_eq_coe {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
    (D).toFun = D
    def LieDerivation.Simps.apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
    LM

    See Note [custom simps projection]

    Equations
    Instances For
      instance LieDerivation.instCoeToLinearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      Coe (LieDerivation R L M) (L →ₗ[R] M)
      Equations
      • LieDerivation.instCoeToLinearMap = { coe := fun (D : LieDerivation R L M) => D }
      @[simp]
      theorem LieDerivation.mk_coe {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (f : L →ₗ[R] M) (h₁ : ∀ (a b : L), f a, b = a, f b - b, f a) :
      { toLinearMap := f, leibniz' := h₁ } = f
      @[simp]
      theorem LieDerivation.coeFn_coe {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (f : LieDerivation R L M) :
      f = f
      theorem LieDerivation.coe_injective {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      Function.Injective DFunLike.coe
      theorem LieDerivation.ext {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 : LieDerivation R L M} {D2 : LieDerivation R L M} (H : ∀ (a : L), D1 a = D2 a) :
      D1 = D2
      theorem LieDerivation.congr_fun {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 : LieDerivation R L M} {D2 : LieDerivation R L M} (h : D1 = D2) (a : L) :
      D1 a = D2 a
      @[simp]
      theorem LieDerivation.apply_lie_eq_sub {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (a : L) (b : L) :
      D a, b = a, D b - b, D a
      theorem LieDerivation.apply_lie_eq_add {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (a : L) (b : L) :
      D a, b = a, D b + D a, b

      For a Lie derivation from a Lie algebra to itself, the usual Leibniz rule holds.

      theorem LieDerivation.eqOn_lieSpan {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 : LieDerivation R L M} {D2 : LieDerivation R L M} {s : Set L} (h : Set.EqOn (D1) (D2) s) :
      Set.EqOn D1 D2 (LieSubalgebra.lieSpan R L s)

      Two Lie derivations equal on a set are equal on its Lie span.

      theorem LieDerivation.ext_of_lieSpan_eq_top {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 : LieDerivation R L M} {D2 : LieDerivation R L M} (s : Set L) (hs : LieSubalgebra.lieSpan R L s = ) (h : Set.EqOn (D1) (D2) s) :
      D1 = D2

      If the Lie span of a set is the whole Lie algebra, then two Lie derivations equal on this set are equal on the whole Lie algebra.

      instance LieDerivation.instZero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      Equations
      • LieDerivation.instZero = { zero := { toLinearMap := 0, leibniz' := } }
      @[simp]
      theorem LieDerivation.coe_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      0 = 0
      @[simp]
      theorem LieDerivation.coe_zero_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      0 = 0
      theorem LieDerivation.zero_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (a : L) :
      0 a = 0
      instance LieDerivation.instInhabited {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      Equations
      • LieDerivation.instInhabited = { default := 0 }
      instance LieDerivation.instAdd {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      Equations
      • LieDerivation.instAdd = { add := fun (D1 D2 : LieDerivation R L M) => { toLinearMap := D1 + D2, leibniz' := } }
      @[simp]
      theorem LieDerivation.coe_add {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D1 : LieDerivation R L M) (D2 : LieDerivation R L M) :
      (D1 + D2) = D1 + D2
      @[simp]
      theorem LieDerivation.coe_add_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D1 : LieDerivation R L M) (D2 : LieDerivation R L M) :
      (D1 + D2) = D1 + D2
      theorem LieDerivation.add_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 : LieDerivation R L M} {D2 : LieDerivation R L M} (a : L) :
      (D1 + D2) a = D1 a + D2 a
      theorem LieDerivation.map_neg {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (a : L) :
      D (-a) = -D a
      theorem LieDerivation.map_sub {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (a : L) (b : L) :
      D (a - b) = D a - D b
      instance LieDerivation.instNeg {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      Equations
      • LieDerivation.instNeg = { neg := fun (D : LieDerivation R L M) => { toLinearMap := -D, leibniz' := } }
      @[simp]
      theorem LieDerivation.coe_neg {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
      (-D) = -D
      @[simp]
      theorem LieDerivation.coe_neg_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
      (-D) = -D
      theorem LieDerivation.neg_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (a : L) :
      (-D) a = -D a
      instance LieDerivation.instSub {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      Equations
      • LieDerivation.instSub = { sub := fun (D1 D2 : LieDerivation R L M) => { toLinearMap := D1 - D2, leibniz' := } }
      @[simp]
      theorem LieDerivation.coe_sub {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D1 : LieDerivation R L M) (D2 : LieDerivation R L M) :
      (D1 - D2) = D1 - D2
      @[simp]
      theorem LieDerivation.coe_sub_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D1 : LieDerivation R L M) (D2 : LieDerivation R L M) :
      (D1 - D2) = D1 - D2
      theorem LieDerivation.sub_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (a : L) {D1 : LieDerivation R L M} {D2 : LieDerivation R L M} :
      (D1 - D2) a = D1 a - D2 a
      class LieDerivation.SMulBracketCommClass (S : Type u_4) (L : Type u_5) (α : Type u_6) [SMul S α] [LieRing L] [AddCommGroup α] [LieRingModule L α] :

      A typeclass mixin saying that scalar multiplication and Lie bracket are left commutative.

      • smul_bracket_comm : ∀ (s : S) (l : L) (a : α), s l, a = l, s a

        and ⁅⬝, ⬝⁆ are left commutative

      Instances
        theorem LieDerivation.SMulBracketCommClass.smul_bracket_comm {S : Type u_4} {L : Type u_5} {α : Type u_6} [SMul S α] [LieRing L] [AddCommGroup α] [LieRingModule L α] [self : LieDerivation.SMulBracketCommClass S L α] (s : S) (l : L) (a : α) :
        s l, a = l, s a

        and ⁅⬝, ⬝⁆ are left commutative

        instance LieDerivation.instSMul {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [LieDerivation.SMulBracketCommClass S L M] :
        Equations
        • LieDerivation.instSMul = { smul := fun (r : S) (D : LieDerivation R L M) => { toLinearMap := r D, leibniz' := } }
        @[simp]
        theorem LieDerivation.coe_smul {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) :
        (r D) = r D
        @[simp]
        theorem LieDerivation.coe_smul_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) :
        (r D) = r D
        theorem LieDerivation.smul_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (a : L) {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) :
        (r D) a = r D a
        instance LieDerivation.instSMulBase {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
        Equations
        • =
        instance LieDerivation.instAddCommGroup {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
        Equations
        def LieDerivation.coeFnAddMonoidHom {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
        LieDerivation R L M →+ LM

        coe_fn as an AddMonoidHom.

        Equations
        • LieDerivation.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
        Instances For
          Equations
          instance LieDerivation.instIsScalarTower {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} {T : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [LieDerivation.SMulBracketCommClass S L M] [Monoid T] [DistribMulAction T M] [SMulCommClass R T M] [LieDerivation.SMulBracketCommClass T L M] [SMul S T] [IsScalarTower S T M] :
          Equations
          • =
          Equations
          • =
          instance LieDerivation.instModule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] [LieDerivation.SMulBracketCommClass S L M] :
          Equations
          instance LieDerivation.instBracket {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] :

          The commutator of two Lie derivations on a Lie algebra is a Lie derivation.

          Equations
          • LieDerivation.instBracket = { bracket := fun (D1 D2 : LieDerivation R L L) => { toLinearMap := D1, D2, leibniz' := } }
          @[simp]
          theorem LieDerivation.commutator_coe_linear_map {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {D1 : LieDerivation R L L} {D2 : LieDerivation R L L} :
          D1, D2 = D1, D2
          theorem LieDerivation.commutator_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {D1 : LieDerivation R L L} {D2 : LieDerivation R L L} (a : L) :
          D1, D2 a = D1 (D2 a) - D2 (D1 a)
          instance LieDerivation.instLieRing {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] :
          Equations
          instance LieDerivation.instLieAlgebra {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] :

          The set of Lie derivations from a Lie algebra L to itself is a Lie algebra.

          Equations
          @[simp]
          theorem LieDerivation.lie_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D₁ : LieDerivation R L L) (D₂ : LieDerivation R L L) (x : L) :
          D₁, D₂ x = D₁ (D₂ x) - D₂ (D₁ x)

          The Lie algebra morphism from Lie derivations into linear endormophisms.

          Equations
          Instances For

            The map from Lie derivations to linear endormophisms is injective.

            instance LieDerivation.instNoetherian (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] :

            Lie derivations over a Noetherian Lie algebra form a Noetherian module.

            Equations
            • =
            @[simp]
            theorem LieDerivation.inner_apply_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (m : M) (m : L) :
            ((LieDerivation.inner R L M) m✝) m = m, m✝
            def LieDerivation.inner (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

            The natural map from a Lie module to the derivations taking values in it.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              instance LieDerivation.instLieRingModule (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
              Equations
              @[simp]
              theorem LieDerivation.lie_lieDerivation_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (D : LieDerivation R L M) :
              x, D y = y, D x
              @[simp]
              theorem LieDerivation.lie_coe_lieDerivation_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (D : LieDerivation R L M) :
              x, D = x, D
              instance LieDerivation.instLieModule (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
              Equations
              • =
              theorem LieDerivation.leibniz_lie (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (D₁ : LieDerivation R L L) (D₂ : LieDerivation R L L) :
              x, D₁, D₂ = x, D₁, D₂ + D₁, x, D₂