Documentation

Mathlib.Algebra.Lie.OfAssociative

Lie algebras of associative algebras #

This file defines the Lie algebra structure that arises on an associative algebra via the ring commutator.

Since the linear endomorphisms of a Lie algebra form an associative algebra, one can define the adjoint action as a morphism of Lie algebras from a Lie algebra to its linear endomorphisms. We make such a definition in this file.

Main definitions #

Tags #

lie algebra, ring commutator, adjoint action

@[instance 100]
instance LieRing.ofAssociativeRing {A : Type v} [Ring A] :

An associative ring gives rise to a Lie ring by taking the bracket to be the ring commutator.

Equations
theorem LieRing.of_associative_ring_bracket {A : Type v} [Ring A] (x : A) (y : A) :
x, y = x * y - y * x
@[simp]
theorem LieRing.lie_apply {A : Type v} [Ring A] {α : Type u_1} (f : αA) (g : αA) (a : α) :
f, g a = f a, g a
@[reducible, inline]

We can regard a module over an associative ring A as a Lie ring module over A with Lie bracket equal to its ring commutator.

Note that this cannot be a global instance because it would create a diamond when M = A, specifically we can build two mathematically-different bracket A As:

  1. @Ring.bracket A _ which says ⁅a, b⁆ = a * b - b * a
  2. (@LieRingModule.ofAssociativeModule A _ A _ _).toBracket which says ⁅a, b⁆ = a • b (and thus ⁅a, b⁆ = a * b)

See note [reducible non-instances]

Equations
Instances For
    theorem lie_eq_smul {A : Type v} [Ring A] {M : Type w} [AddCommGroup M] [Module A M] (a : A) (m : M) :
    a, m = a m
    @[instance 100]
    instance LieAlgebra.ofAssociativeAlgebra {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] :

    An associative algebra gives rise to a Lie algebra by taking the bracket to be the ring commutator.

    Equations
    theorem LieModule.ofAssociativeModule {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {M : Type w} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] :
    LieModule R A M

    A representation of an associative algebra A is also a representation of A, regarded as a Lie algebra via the ring commutator.

    See the comment at LieRingModule.ofAssociativeModule for why the possibility M = A means this cannot be a global instance.

    Equations
    • Module.End.instLieRingModule = LieRingModule.ofAssociativeModule
    instance Module.End.instLieModule {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R M] :
    Equations
    • =
    @[simp]
    theorem Module.End.lie_apply {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R M] (f : Module.End R M) (m : M) :
    f, m = f m
    def AlgHom.toLieHom {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) :

    The map ofAssociativeAlgebra associating a Lie algebra to an associative algebra is functorial.

    Equations
    • f.toLieHom = { toLinearMap := f.toLinearMap, map_lie' := }
    Instances For
      instance AlgHom.instCoeLieHom {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] :
      Coe (A →ₐ[R] B) (A →ₗ⁅R B)
      Equations
      • AlgHom.instCoeLieHom = { coe := AlgHom.toLieHom }
      @[simp]
      theorem AlgHom.coe_toLieHom {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) :
      f.toLieHom = f
      theorem AlgHom.toLieHom_apply {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) (x : A) :
      f.toLieHom x = f x
      @[simp]
      theorem AlgHom.toLieHom_id {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] :
      (AlgHom.id R A).toLieHom = LieHom.id
      @[simp]
      theorem AlgHom.toLieHom_comp {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} {C : Type w₁} [Ring B] [Ring C] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
      (g.comp f).toLieHom = g.toLieHom.comp f.toLieHom
      theorem AlgHom.toLieHom_injective {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] {f : A →ₐ[R] B} {g : A →ₐ[R] B} (h : f.toLieHom = g.toLieHom) :
      f = g
      @[simp]
      theorem LieModule.toEnd_apply_apply (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) :
      ((LieModule.toEnd R L M) x) m = x, m
      def LieModule.toEnd (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

      A Lie module yields a Lie algebra morphism into the linear endomorphisms of the module.

      See also LieModule.toModuleHom.

      Equations
      • LieModule.toEnd R L M = { toFun := fun (x : L) => { toFun := fun (m : M) => x, m, map_add' := , map_smul' := }, map_add' := , map_smul' := , map_lie' := }
      Instances For
        def LieAlgebra.ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

        The adjoint action of a Lie algebra on itself.

        Equations
        Instances For
          @[simp]
          theorem LieAlgebra.ad_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (y : L) :
          ((LieAlgebra.ad R L) x) y = x, y
          @[simp]
          theorem LieModule.toEnd_module_end (R : Type u) (M : Type w) [CommRing R] [AddCommGroup M] [Module R M] :
          LieModule.toEnd R (Module.End R M) M = LieHom.id
          theorem LieSubalgebra.toEnd_eq (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (K : LieSubalgebra R L) {x : K} :
          (LieModule.toEnd R (↥K) M) x = (LieModule.toEnd R L M) x
          @[simp]
          theorem LieSubalgebra.toEnd_mk (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (K : LieSubalgebra R L) {x : L} (hx : x K) :
          (LieModule.toEnd R (↥K) M) x, hx = (LieModule.toEnd R L M) x
          theorem LieSubmodule.coe_toEnd (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (y : N) :
          (((LieModule.toEnd R L N) x) y) = ((LieModule.toEnd R L M) x) y
          theorem LieSubmodule.coe_toEnd_pow (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (y : N) (n : ) :
          (((LieModule.toEnd R L N) x ^ n) y) = ((LieModule.toEnd R L M) x ^ n) y
          theorem LieSubalgebra.coe_ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x : H) (y : H) :
          (((LieAlgebra.ad R H) x) y) = ((LieAlgebra.ad R L) x) y
          theorem LieSubalgebra.coe_ad_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x : H) (y : H) (n : ) :
          (((LieAlgebra.ad R H) x ^ n) y) = ((LieAlgebra.ad R L) x ^ n) y
          theorem LieModule.toEnd_lie (R : Type u) {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (z : M) :
          ((LieModule.toEnd R L M) x) y, z = ((LieAlgebra.ad R L) x) y, z + y, ((LieModule.toEnd R L M) x) z
          theorem LieAlgebra.ad_lie (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (y : L) (z : L) :
          ((LieAlgebra.ad R L) x) y, z = ((LieAlgebra.ad R L) x) y, z + y, ((LieAlgebra.ad R L) x) z
          theorem LieModule.toEnd_pow_lie (R : Type u) {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (z : M) (n : ) :
          ((LieModule.toEnd R L M) x ^ n) y, z = ijFinset.antidiagonal n, n.choose ij.1 ((LieAlgebra.ad R L) x ^ ij.1) y, ((LieModule.toEnd R L M) x ^ ij.2) z
          theorem LieAlgebra.ad_pow_lie (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (y : L) (z : L) (n : ) :
          ((LieAlgebra.ad R L) x ^ n) y, z = ijFinset.antidiagonal n, n.choose ij.1 ((LieAlgebra.ad R L) x ^ ij.1) y, ((LieAlgebra.ad R L) x ^ ij.2) z
          theorem LieModule.toEnd_pow_comp_lieHom {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L M₂) (k : ) (x : L) :
          ((LieModule.toEnd R L M₂) x ^ k) ∘ₗ f = f ∘ₗ (LieModule.toEnd R L M) x ^ k
          theorem LieModule.toEnd_pow_apply_map {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L M₂) (k : ) (x : L) (m : M) :
          ((LieModule.toEnd R L M₂) x ^ k) (f m) = f (((LieModule.toEnd R L M) x ^ k) m)
          theorem LieSubmodule.coe_map_toEnd_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L M} {x : L} :
          Submodule.map ((LieModule.toEnd R L M) x) N N
          theorem LieSubmodule.toEnd_comp_subtype_mem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (m : M) (hm : m N) :
          ((LieModule.toEnd R L M) x ∘ₗ (↑N).subtype) m, hm N
          @[simp]
          theorem LieSubmodule.toEnd_restrict_eq_toEnd {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (h : optParam (∀ (m : M) (hm : m N), ((LieModule.toEnd R L M) x ∘ₗ (↑N).subtype) m, hm N) ) :
          theorem LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) {φ : R} {k : } {x : L} :
          Set.MapsTo (((LieModule.toEnd R L M) x - (algebraMap R (Module.End R M)) φ) ^ k) N N
          theorem LieSubalgebra.ad_comp_incl_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (x : K) :
          (LieAlgebra.ad R L) x ∘ₗ K.incl = K.incl ∘ₗ (LieAlgebra.ad R K) x
          def lieSubalgebraOfSubalgebra (R : Type u) [CommRing R] (A : Type v) [Ring A] [Algebra R A] (A' : Subalgebra R A) :

          A subalgebra of an associative algebra is a Lie subalgebra of the associated Lie algebra.

          Equations
          Instances For
            def LinearEquiv.lieConj {R : Type u} {M₁ : Type v} {M₂ : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) :

            A linear equivalence of two modules induces a Lie algebra equivalence of their endomorphisms.

            Equations
            • e.lieConj = { toLinearMap := e.conj, map_lie' := , invFun := e.conj.invFun, left_inv := , right_inv := }
            Instances For
              @[simp]
              theorem LinearEquiv.lieConj_apply {R : Type u} {M₁ : Type v} {M₂ : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : Module.End R M₁) :
              e.lieConj f = e.conj f
              @[simp]
              theorem LinearEquiv.lieConj_symm {R : Type u} {M₁ : Type v} {M₂ : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) :
              e.lieConj.symm = e.symm.lieConj
              def AlgEquiv.toLieEquiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [CommRing R] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
              A₁ ≃ₗ⁅R A₂

              An equivalence of associative algebras is an equivalence of associated Lie algebras.

              Equations
              • e.toLieEquiv = { toFun := e.toFun, map_add' := , map_smul' := , map_lie' := , invFun := e.toLinearEquiv.invFun, left_inv := , right_inv := }
              Instances For
                @[simp]
                theorem AlgEquiv.toLieEquiv_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [CommRing R] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
                e.toLieEquiv x = e x
                @[simp]
                theorem AlgEquiv.toLieEquiv_symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [CommRing R] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂) :
                e.toLieEquiv.symm x = e.symm x
                @[simp]
                theorem LieAlgebra.conj_ad_apply {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R L') (x : L) :
                e.toLinearEquiv.conj ((LieAlgebra.ad R L) x) = (LieAlgebra.ad R L') (e x)

                Given an equivalence e of Lie algebras from L to L', and an element x : L, the conjugate of the endomorphism ad(x) of L by e is the endomorphism ad(e x) of L'.