mathlib3 documentation

algebra.lie.of_associative

Lie algebras of associative algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[protected, instance]
def ring.has_bracket {A : Type v} [ring A] :
has_bracket A 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.

Equations
source
theorem ring.lie_def {A : Type v} [ring A] (x y : A) :
⁅x, y⁆ = x * y - y * x
source
theorem commute_iff_lie_eq {A : Type v} [ring A] {x y : A} :
commute x y ↔ ⁅x, y⁆ = 0
source
theorem commute.lie_eq {A : Type v} [ring A] {x y : A} (h : commute x y) :
⁅x, y⁆ = 0
source
@[protected, instance]
def lie_ring.of_associative_ring {A : Type v} [ring A] :
lie_ring A

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

Equations
source
theorem lie_ring.of_associative_ring_bracket {A : Type v} [ring A] (x y : A) :
⁅x, y⁆ = x * y - y * x
source
@[simp]
theorem lie_ring.lie_apply {A : Type v} [ring A] {α : Type u_1} (f g : α → A) (a : α) :
⁅f, g⁆ a = ⁅f a, g a⁆
source
@[reducible]
def lie_ring_module.of_associative_module {A : Type v} [ring A] {M : Type w} [add_comm_group M] [module A M] :
lie_ring_module A M

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 has_bracket A As:

  1. @ring.has_bracket A _ which says ⁅a, b⁆ = a * b - b * a
  2. (@lie_ring_module.of_associative_module A _ A _ _).to_has_bracket which says ⁅a, b⁆ = a • b (and thus ⁅a, b⁆ = a * b)

See note [reducible non-instances]

Equations
source
theorem lie_eq_smul {A : Type v} [ring A] {M : Type w} [add_comm_group M] [module A M] (a : A) (m : M) :
⁅a, m⁆ = a • m
source
@[protected, instance]
def lie_algebra.of_associative_algebra {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] :
lie_algebra R A

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

Equations
source
def lie_module.of_associative_module {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {M : Type w} [add_comm_group M] [module R M] [module A M] [is_scalar_tower R A M] :
lie_module 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 lie_ring_module.of_associative_module for why the possibility M = A means this cannot be a global instance.

Equations
source
@[protected, instance]
def module.End.lie_ring_module {R : Type u} [comm_ring R] {M : Type w} [add_comm_group M] [module R M] :
lie_ring_module (module.End R M) M
Equations
source
@[protected, instance]
def module.End.lie_module {R : Type u} [comm_ring R] {M : Type w} [add_comm_group M] [module R M] :
lie_module R (module.End R M) M
Equations
source
def alg_hom.to_lie_hom {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {B : Type w} [ring B] [algebra R B] (f : A →ₐ[R] B) :
A →ₗ⁅R⁆ B

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

Equations
source
@[protected, instance]
def alg_hom.lie_hom.has_coe {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {B : Type w} [ring B] [algebra R B] :
has_coe (A →ₐ[R] B) (A →ₗ⁅R⁆ B)
Equations
source
@[simp]
theorem alg_hom.to_lie_hom_coe {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {B : Type w} [ring B] [algebra R B] (f : A →ₐ[R] B) :
f.to_lie_hom = ↑f
source
@[simp]
theorem alg_hom.coe_to_lie_hom {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {B : Type w} [ring B] [algebra R B] (f : A →ₐ[R] B) :
⇑↑f = ⇑f
source
theorem alg_hom.to_lie_hom_apply {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {B : Type w} [ring B] [algebra R B] (f : A →ₐ[R] B) (x : A) :
⇑(f.to_lie_hom) x = ⇑f x
source
@[simp]
theorem alg_hom.to_lie_hom_id {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] :
↑(alg_hom.id R A) = lie_hom.id
source
@[simp]
theorem alg_hom.to_lie_hom_comp {A : Type v} [ring A] {R : Type u} [comm_ring 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) = ↑g.comp ↑f
source
theorem alg_hom.to_lie_hom_injective {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {B : Type w} [ring B] [algebra R B] {f g : A →ₐ[R] B} (h : ↑f = ↑g) :
f = g
source
def lie_module.to_endomorphism (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
L →ₗ⁅R⁆ module.End R M

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

See also lie_module.to_module_hom.

Equations
source
@[simp]
theorem lie_module.to_endomorphism_to_linear_map_apply_apply (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (x : L) (m : M) :
⇑(⇑((lie_module.to_endomorphism R L M).to_linear_map) x) m = ⁅x, m⁆
source
@[simp]
theorem lie_module.to_endomorphism_apply_apply (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (x : L) (m : M) :
⇑(⇑(lie_module.to_endomorphism R L M) x) m = ⁅x, m⁆
source
def lie_algebra.ad (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
L →ₗ⁅R⁆ module.End R L

The adjoint action of a Lie algebra on itself.

Equations
source
@[simp]
theorem lie_algebra.ad_apply (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (x y : L) :
⇑(⇑(lie_algebra.ad R L) x) y = ⁅x, y⁆
source
@[simp]
theorem lie_module.to_endomorphism_module_End (R : Type u) (M : Type w) [comm_ring R] [add_comm_group M] [module R M] :
lie_module.to_endomorphism R (module.End R M) M = lie_hom.id
source
theorem lie_subalgebra.to_endomorphism_eq (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (K : lie_subalgebra R L) {x : ↥K} :
⇑(lie_module.to_endomorphism R ↥K M) x = ⇑(lie_module.to_endomorphism R L M) ↑x
source
@[simp]
theorem lie_subalgebra.to_endomorphism_mk (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (K : lie_subalgebra R L) {x : L} (hx : x ∈ K) :
⇑(lie_module.to_endomorphism R ↥K M) ⟨x, hx⟩ = ⇑(lie_module.to_endomorphism R L M) x
source
theorem lie_submodule.coe_map_to_endomorphism_le {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N : lie_submodule R L M} {x : L} :
submodule.map (⇑(lie_module.to_endomorphism R L M) x) ↑N ≤ ↑N
source
theorem lie_submodule.to_endomorphism_comp_subtype_mem {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (x : L) (m : M) (hm : m ∈ ↑N) :
⇑(linear_map.comp (⇑(lie_module.to_endomorphism R L M) x) ↑N.subtype) ⟨m, hm⟩ ∈ ↑N
source
@[simp]
theorem lie_submodule.to_endomorphism_restrict_eq_to_endomorphism {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (x : L) (h : (∀ (m : M) (hm : m ∈ ↑N), ⇑(linear_map.comp (⇑(lie_module.to_endomorphism R L M) x) ↑N.subtype) ⟨m, hm⟩ ∈ ↑N) := _) :
linear_map.restrict (⇑(lie_module.to_endomorphism R L M) x) h = ⇑(lie_module.to_endomorphism R L ↥N) x
source
theorem lie_algebra.ad_eq_lmul_left_sub_lmul_right {R : Type u} [comm_ring R] (A : Type v) [ring A] [algebra R A] :
⇑(lie_algebra.ad R A) = linear_map.mul_left R - linear_map.mul_right R
source
theorem lie_subalgebra.ad_comp_incl_eq {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K : lie_subalgebra R L) (x : ↥K) :
linear_map.comp (⇑(lie_algebra.ad R L) ↑x) ↑(K.incl) = ↑(K.incl).comp (⇑(lie_algebra.ad R ↥K) x)
source
def lie_subalgebra_of_subalgebra (R : Type u) [comm_ring R] (A : Type v) [ring A] [algebra R A] (A' : subalgebra R A) :
lie_subalgebra R A

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

Equations
source
def linear_equiv.lie_conj {R : Type u} {M₁ : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (e : M₁ ≃ₗ[R] M₂) :
module.End R M₁ ≃ₗ⁅R⁆ module.End R M₂

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

Equations
source
@[simp]
theorem linear_equiv.lie_conj_apply {R : Type u} {M₁ : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : module.End R M₁) :
⇑(e.lie_conj) f = ⇑(e.conj) f
source
@[simp]
theorem linear_equiv.lie_conj_symm {R : Type u} {M₁ : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (e : M₁ ≃ₗ[R] M₂) :
e.lie_conj.symm = e.symm.lie_conj
source
def alg_equiv.to_lie_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring 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
source
@[simp]
theorem alg_equiv.to_lie_equiv_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
⇑(e.to_lie_equiv) x = ⇑e x
source
@[simp]
theorem alg_equiv.to_lie_equiv_symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂) :
⇑(e.to_lie_equiv.symm) x = ⇑(e.symm) x