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 Ring.instBracket {A : Type v} [Ring A] :

The bracket operation for rings is the ring commutator, which captures the extent to which a ring is commutative. It is identically zero exactly when the ring is commutative.

theorem Ring.lie_def {A : Type v} [Ring A] (x : A) (y : A) :
x, y = x * y - y * x
theorem commute_iff_lie_eq {A : Type v} [Ring A] {x : A} {y : A} :
Commute x y x, y = 0
theorem Commute.lie_eq {A : Type v} [Ring A] {x : A} {y : A} (h : Commute x y) :
x, y = 0
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.

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 : α) :
αA, αA LieRingModule.toBracket f g a = f a, g a
@[reducible]

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]

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 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.

    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.

    instance Module.End.lieModule {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R 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.

    Instances For
      @[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) :
      ↑(AlgHom.toLieHom f) = 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) :
      ↑(AlgHom.toLieHom f) x = f x
      @[simp]
      theorem AlgHom.toLieHom_id {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] :
      AlgHom.toLieHom (AlgHom.id R A) = 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) :
      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 : AlgHom.toLieHom f = AlgHom.toLieHom g) :
      f = g
      @[simp]
      theorem LieModule.toEndomorphism_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.toEndomorphism R L M) x) m = x, m
      def LieModule.toEndomorphism (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.

      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.

        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 LieSubalgebra.toEndomorphism_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 : { x // x K }} :
          ↑(LieModule.toEndomorphism R { x // x K } M) x = ↑(LieModule.toEndomorphism R L M) x
          @[simp]
          theorem LieSubalgebra.toEndomorphism_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.toEndomorphism R { x // x K } M) { val := x, property := hx } = ↑(LieModule.toEndomorphism R L M) x
          theorem LieSubmodule.coe_map_toEndomorphism_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.toEndomorphism R L M) x) N N
          theorem LieSubmodule.toEndomorphism_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) :
          ↑(LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (Submodule.subtype N)) { val := m, property := hm } N
          @[simp]
          theorem LieSubmodule.toEndomorphism_restrict_eq_toEndomorphism {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), ↑(LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (Submodule.subtype N)) { val := m, property := hm } N) (_ : ∀ (m : M) (hm : m N), ↑(LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (Submodule.subtype N)) { val := m, property := hm } N)) :
          LinearMap.restrict (↑(LieModule.toEndomorphism R L M) x) h = ↑(LieModule.toEndomorphism R L { x // x N }) x
          theorem LieSubalgebra.ad_comp_incl_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (x : { x // x K }) :
          LinearMap.comp (↑(LieAlgebra.ad R L) x) ↑(LieSubalgebra.incl K) = LinearMap.comp (↑(LieSubalgebra.incl K)) (↑(LieAlgebra.ad R { x // x 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.

          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.

            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₁) :
              @[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₂) :
              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.

              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₁) :
                ↑(AlgEquiv.toLieEquiv e) 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₂) :