mathlib documentation

algebra.lie.basic

Lie algebras

This file defines Lie rings, and Lie algebras over a commutative ring. It shows how these arise from associative rings and algebras via the ring commutator. In particular it defines the Lie algebra of endomorphisms of a module as well as of the algebra of square matrices over a commutative ring.

It also includes definitions of morphisms of Lie algebras, Lie subalgebras, Lie modules, Lie submodules, and the quotient of a Lie algebra by an ideal.

Notations

We introduce the notation ⁅x, y⁆ for the Lie bracket. Note that these are the Unicode "square with quill" brackets rather than the usual square brackets.

Working over a fixed commutative ring R, we introduce the notations:

Implementation notes

Lie algebras are defined as modules with a compatible Lie ring structure and thus, like modules, are partially unbundled.

References

Tags

lie bracket, ring commutator, jacobi identity, lie ring, lie algebra

@[class]
structure has_bracket (L : Type v) (M : Type w) :
Type (max v w)
  • bracket : L → M → M

The has_bracket class has two intended uses:

  1. for the product ⁅x, y⁆ of two elements x, y in a Lie algebra (analogous to has_mul in the associative setting),

  2. for the action ⁅x, m⁆ of an element x of a Lie algebra on an element m in one of its modules (analogous to has_scalar in the associative setting).

Instances
@[class]
structure lie_ring (L : Type v) :
Type v

A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity. The bracket is not associative unless it is identically zero.

Instances
@[class]
structure lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] :
Type (max u v)

A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.

Instances
@[class]
structure lie_ring_module (L : Type v) (M : Type w) [lie_ring L] [add_comm_group M] :
Type (max v w)

A Lie ring module is an additive group, together with an additive action of a Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms. (For representations of Lie algebras see lie_module.)

Instances
@[class]
structure lie_module (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] :
Type

A Lie module is a module over a commutative ring, together with a linear action of a Lie algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms.

Instances
@[simp]
theorem add_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x y : L) (m : M) :

@[simp]
theorem lie_add {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m n : M) :

@[simp]
theorem smul_lie {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] (t : R) (x : L) (m : M) :

@[simp]
theorem lie_smul {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] (t : R) (x : L) (m : M) :

theorem leibniz_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x y : L) (m : M) :

@[simp]
theorem lie_zero {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) :

@[simp]
theorem zero_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (m : M) :

@[simp]
theorem lie_self {L : Type v} [lie_ring L] (x : L) :

@[simp]
theorem lie_skew {L : Type v} [lie_ring L] (x y : L) :

@[instance]
def lie_algebra_self_module {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :

Every Lie algebra is a module over itself.

Equations
@[simp]
theorem neg_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) :

@[simp]
theorem lie_neg {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) :

@[simp]
theorem gsmul_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) (a : ) :

@[simp]
theorem lie_gsmul {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) (a : ) :

@[simp]
theorem lie_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x y : L) (m : M) :

theorem lie_jacobi {L : Type v} [lie_ring L] (x y z : L) :

@[nolint]
def lie_algebra.morphism.to_linear_map {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (s : L →ₗ⁅R L') :
L →ₗ[R] L'

structure lie_algebra.morphism (R : Type u) (L : Type v) (L' : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] :
Type (max v w)

A morphism of Lie algebras is a linear map respecting the bracket operations.

@[instance]
def lie_algebra.linear_map.has_coe {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] :
has_coe (L₁ →ₗ⁅R L₂) (L₁ →ₗ[R] L₂)

Equations
@[instance]
def lie_algebra.morphism.has_coe_to_fun {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] :

see Note [function coercion]

Equations
@[simp]
theorem lie_algebra.coe_mk {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (f : L₁ → L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : L₁), f (m x) = m f x) (h₃ : ∀ {x y : L₁}, f x,y = f x,f y) :
{to_fun := f, map_add' := h₁, map_smul' := h₂, map_lie := h₃} = f

@[simp]
theorem lie_algebra.coe_to_linear_map {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (f : L₁ →ₗ⁅R L₂) :

@[simp]
theorem lie_algebra.map_lie {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (f : L₁ →ₗ⁅R L₂) (x y : L₁) :

@[instance]
def lie_algebra.morphism.has_zero {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] :
has_zero (L₁ →ₗ⁅R L₂)

The constant 0 map is a Lie algebra morphism.

Equations
@[instance]
def lie_algebra.morphism.has_one {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :
has_one (L₁ →ₗ⁅R L₁)

The identity map is a Lie algebra morphism.

Equations
@[instance]
def lie_algebra.morphism.inhabited {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] :
inhabited (L₁ →ₗ⁅R L₂)

Equations
theorem lie_algebra.morphism.coe_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] :
function.injective (λ (f : L₁ →ₗ⁅R L₂), show L₁ → L₂, from f)

@[ext]
theorem lie_algebra.morphism.ext {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] {f g : L₁ →ₗ⁅R L₂} (h : ∀ (x : L₁), f x = g x) :
f = g

theorem lie_algebra.morphism.ext_iff {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] {f g : L₁ →ₗ⁅R L₂} :
f = g ∀ (x : L₁), f x = g x

def lie_algebra.morphism.comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) :
L₁ →ₗ⁅R L₃

The composition of morphisms is a morphism.

Equations
@[simp]
theorem lie_algebra.morphism.comp_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) (x : L₁) :
(f.comp g) x = f (g x)

theorem lie_algebra.morphism.comp_coe {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) :
f g = (f.comp g)

def lie_algebra.morphism.inverse {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (f : L₁ →ₗ⁅R L₂) (g : L₂ → L₁) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :
L₂ →ₗ⁅R L₁

The inverse of a bijective morphism is a morphism.

Equations
structure lie_algebra.equiv (R : Type u) (L : Type v) (L' : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] :
Type (max v w)

An equivalence of Lie algebras is a morphism which is also a linear equivalence. We could instead define an equivalence to be a morphism which is also a (plain) equivalence. However it is more convenient to define via linear equivalence to get .to_linear_equiv for free.

@[nolint]
def lie_algebra.equiv.to_linear_equiv {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (s : L ≃ₗ⁅R L') :
L ≃ₗ[R] L'

@[nolint]
def lie_algebra.equiv.to_morphism {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (s : L ≃ₗ⁅R L') :

@[instance]
def lie_algebra.equiv.has_coe_to_lie_hom {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] :
has_coe (L₁ ≃ₗ⁅R L₂) (L₁ →ₗ⁅R L₂)

Equations
@[instance]
def lie_algebra.equiv.has_coe_to_linear_equiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] :
has_coe (L₁ ≃ₗ⁅R L₂) (L₁ ≃ₗ[R] L₂)

Equations
@[instance]
def lie_algebra.equiv.has_coe_to_fun {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] :

see Note [function coercion]

Equations
@[simp]
theorem lie_algebra.equiv.coe_to_lie_equiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (e : L₁ ≃ₗ⁅R L₂) :

@[simp]
theorem lie_algebra.equiv.coe_to_linear_equiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (e : L₁ ≃ₗ⁅R L₂) :

@[instance]
def lie_algebra.equiv.has_one {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :
has_one (L₁ ≃ₗ⁅R L₁)

Equations
@[simp]
theorem lie_algebra.equiv.one_apply {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (x : L₁) :
1 x = x

@[instance]
def lie_algebra.equiv.inhabited {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :
inhabited (L₁ ≃ₗ⁅R L₁)

Equations
def lie_algebra.equiv.refl {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :
L₁ ≃ₗ⁅R L₁

Lie algebra equivalences are reflexive.

Equations
@[simp]
theorem lie_algebra.equiv.refl_apply {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (x : L₁) :

def lie_algebra.equiv.symm {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (e : L₁ ≃ₗ⁅R L₂) :
L₂ ≃ₗ⁅R L₁

Lie algebra equivalences are symmetric.

Equations
@[simp]
theorem lie_algebra.equiv.symm_symm {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (e : L₁ ≃ₗ⁅R L₂) :
e.symm.symm = e

@[simp]
theorem lie_algebra.equiv.apply_symm_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (e : L₁ ≃ₗ⁅R L₂) (x : L₂) :
e ((e.symm) x) = x

@[simp]
theorem lie_algebra.equiv.symm_apply_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (e : L₁ ≃ₗ⁅R L₂) (x : L₁) :
(e.symm) (e x) = x

def lie_algebra.equiv.trans {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] (e₁ : L₁ ≃ₗ⁅R L₂) (e₂ : L₂ ≃ₗ⁅R L₃) :
L₁ ≃ₗ⁅R L₃

Lie algebra equivalences are transitive.

Equations
@[simp]
theorem lie_algebra.equiv.trans_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] (e₁ : L₁ ≃ₗ⁅R L₂) (e₂ : L₂ ≃ₗ⁅R L₃) (x : L₁) :
(e₁.trans e₂) x = e₂ (e₁ x)

@[simp]
theorem lie_algebra.equiv.symm_trans_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] (e₁ : L₁ ≃ₗ⁅R L₂) (e₂ : L₂ ≃ₗ⁅R L₃) (x : L₃) :
((e₁.trans e₂).symm) x = (e₁.symm) ((e₂.symm) x)

structure lie_module_hom (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Type (max w w₁)

A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.

@[nolint]
def lie_module_hom.to_linear_map {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (s : M →ₗ⁅R,L N) :

@[instance]
def lie_module_hom.linear_map.has_coe {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :

Equations
@[instance]
def lie_module_hom.has_coe_to_fun {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :

see Note [function coercion]

Equations
@[simp]
theorem lie_module_hom.coe_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (f : M → N) (h₁ : ∀ (x y : M), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : M), f (m x) = m f x) (h₃ : ∀ {x : L} {m : M}, f x,m = x,f m) :
{to_fun := f, map_add' := h₁, map_smul' := h₂, map_lie := h₃} = f

@[simp]
theorem lie_module_hom.coe_to_linear_map {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (f : M →ₗ⁅R,L N) :

@[simp]
theorem lie_module_hom.map_lie' {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (f : M →ₗ⁅R,L N) (x : L) (m : M) :

@[instance]
def lie_module_hom.has_zero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :

The constant 0 map is a Lie module morphism.

Equations
@[instance]
def lie_module_hom.has_one {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] :

The identity map is a Lie module morphism.

Equations
@[instance]
def lie_module_hom.inhabited {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :

Equations
theorem lie_module_hom.coe_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
function.injective (λ (f : M →ₗ⁅R,L N), show M → N, from f)

@[ext]
theorem lie_module_hom.ext {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] {f g : M →ₗ⁅R,L N} (h : ∀ (m : M), f m = g m) :
f = g

theorem lie_module_hom.ext_iff {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] {f g : M →ₗ⁅R,L N} :
f = g ∀ (m : M), f m = g m

def lie_module_hom.comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (f : N →ₗ⁅R,L P) (g : M →ₗ⁅R,L N) :

The composition of Lie module morphisms is a morphism.

Equations
@[simp]
theorem lie_module_hom.comp_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (f : N →ₗ⁅R,L P) (g : M →ₗ⁅R,L N) (m : M) :
(f.comp g) m = f (g m)

theorem lie_module_hom.comp_coe {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (f : N →ₗ⁅R,L P) (g : M →ₗ⁅R,L N) :
f g = (f.comp g)

def lie_module_hom.inverse {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (f : M →ₗ⁅R,L N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :

The inverse of a bijective morphism of Lie modules is a morphism of Lie modules.

Equations
structure lie_module_equiv (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Type (max w w₁)

An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.

@[nolint]
def lie_module_equiv.to_linear_equiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (s : M ≃ₗ⁅R,L N) :

@[nolint]
def lie_module_equiv.to_lie_module_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (s : M ≃ₗ⁅R,L N) :

@[instance]
def lie_module_equiv.has_coe_to_lie_module_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :

Equations
@[instance]
def lie_module_equiv.has_coe_to_linear_equiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :

Equations
@[instance]
def lie_module_equiv.has_coe_to_fun {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :

see Note [function coercion]

Equations
@[simp]
theorem lie_module_equiv.coe_to_lie_module_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) :

@[simp]
theorem lie_module_equiv.coe_to_linear_equiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) :

@[instance]
def lie_module_equiv.has_one {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] :

Equations
@[simp]
theorem lie_module_equiv.one_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] (m : M) :
1 m = m

@[instance]
def lie_module_equiv.inhabited {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] :

Equations
def lie_module_equiv.refl {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] :

Lie module equivalences are reflexive.

Equations
@[simp]
theorem lie_module_equiv.refl_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] (m : M) :

def lie_module_equiv.symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) :

Lie module equivalences are syemmtric.

Equations
@[simp]
theorem lie_module_equiv.symm_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) :
e.symm.symm = e

@[simp]
theorem lie_module_equiv.apply_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) (x : N) :
e ((e.symm) x) = x

@[simp]
theorem lie_module_equiv.symm_apply_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) (x : M) :
(e.symm) (e x) = x

def lie_module_equiv.trans {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (e₁ : M ≃ₗ⁅R,L N) (e₂ : N ≃ₗ⁅R,L P) :

Lie module equivalences are transitive.

Equations
@[simp]
theorem lie_module_equiv.trans_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (e₁ : M ≃ₗ⁅R,L N) (e₂ : N ≃ₗ⁅R,L P) (m : M) :
(e₁.trans e₂) m = e₂ (e₁ m)

@[simp]
theorem lie_module_equiv.symm_trans_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (e₁ : M ≃ₗ⁅R,L N) (e₂ : N ≃ₗ⁅R,L P) (p : P) :
((e₁.trans e₂).symm) p = (e₁.symm) ((e₂.symm) p)

@[instance]
def ring_commutator.has_bracket {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.

Equations
theorem ring_commutator.commutator {A : Type v} [ring A] (x y : A) :
x,y = x * y - y * x

@[instance]
def lie_ring.of_associative_ring {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 lie_ring.of_associative_ring_bracket {A : Type v} [ring A] (x y : A) :
x,y = x * y - y * x

@[class]
structure is_lie_abelian (L : Type v) [has_bracket L L] [has_zero L] :
Prop
  • abelian : ∀ (x y : L), x,y = 0

An Abelian Lie algebra is one in which all brackets vanish.

@[instance]
def lie_algebra.of_associative_algebra {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] :

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

Equations
def lie_algebra.of_associative_algebra_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) :

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

Equations
@[simp]
theorem lie_algebra.of_associative_algebra_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) :

@[simp]
theorem lie_algebra.of_associative_algebra_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) :

def lie_module.to_endo_morphism (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] :

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

Equations
def lie_algebra.ad (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

The adjoint action of a Lie algebra on itself.

Equations
@[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) :

structure lie_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Type v

A Lie subalgebra of a Lie algebra is submodule that is closed under the Lie bracket. This is a sufficient condition for the subset itself to form a Lie algebra.

@[nolint]
def lie_subalgebra.to_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (s : lie_subalgebra R L) :

@[instance]
def lie_subalgebra.has_zero (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

The zero algebra is a subalgebra of any Lie algebra.

Equations
@[instance]
def lie_subalgebra.inhabited (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

Equations
@[instance]
def set.has_coe (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

Equations
@[instance]
def lie_subalgebra.has_mem (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

Equations
@[instance]
def lie_subalgebra_coe_submodule (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

Equations
@[instance]
def lie_subalgebra_lie_ring (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :

A Lie subalgebra forms a new Lie ring.

Equations
@[instance]
def lie_subalgebra_lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :

A Lie subalgebra forms a new Lie algebra.

Equations
@[simp]
theorem lie_subalgebra.mem_coe (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] {L' : lie_subalgebra R L} {x : L} :
x L' x L'

@[simp]
theorem lie_subalgebra.mem_coe' (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] {L' : lie_subalgebra R L} {x : L} :
x L' x L'

@[simp]
theorem lie_subalgebra.coe_bracket (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) (x y : L') :

@[ext]
theorem lie_subalgebra.ext (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (L₁' L₂' : lie_subalgebra R L) (h : ∀ (x : L), x L₁' x L₂') :
L₁' = L₂'

theorem lie_subalgebra.ext_iff (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (L₁' L₂' : lie_subalgebra R L) :
L₁' = L₂' ∀ (x : L), x L₁' x L₂'

def lie_subalgebra_of_subalgebra (R : Type u) [comm_ring 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
def lie_subalgebra.incl {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :

The embedding of a Lie subalgebra into the ambient space as a Lie morphism.

Equations
def lie_algebra.morphism.range {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) :

The range of a morphism of Lie algebras is a Lie subalgebra.

Equations
@[simp]
theorem lie_algebra.morphism.range_bracket {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (x y : (f.range)) :

def lie_subalgebra.map {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (L' : lie_subalgebra R L) :

The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the codomain.

Equations
@[simp]
theorem lie_subalgebra.mem_map_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (e : L ≃ₗ⁅R L₂) (L' : lie_subalgebra R L) (x : L₂) :

def lie_algebra.equiv.of_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (f : L₁ →ₗ⁅R L₂) (h : function.injective f) :

An injective Lie algebra morphism is an equivalence onto its range.

Equations
@[simp]
theorem lie_algebra.equiv.of_injective_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (f : L₁ →ₗ⁅R L₂) (h : function.injective f) (x : L₁) :

def lie_algebra.equiv.of_eq {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (L₁' L₁'' : lie_subalgebra R L₁) (h : L₁' = L₁'') :
L₁' ≃ₗ⁅R L₁''

Lie subalgebras that are equal as sets are equivalent as Lie algebras.

Equations
@[simp]
theorem lie_algebra.equiv.of_eq_apply {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (L L' : lie_subalgebra R L₁) (h : L = L') (x : L) :

def lie_algebra.equiv.of_subalgebra {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁'' : lie_subalgebra R L₁) (e : L₁ ≃ₗ⁅R L₂) :

An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image.

Equations
@[simp]
theorem lie_algebra.equiv.of_subalgebra_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁'' : lie_subalgebra R L₁) (e : L₁ ≃ₗ⁅R L₂) (x : L₁'') :

def lie_algebra.equiv.of_subalgebras {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁' : lie_subalgebra R L₁) (L₂' : lie_subalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : lie_subalgebra.map e L₁' = L₂') :
L₁' ≃ₗ⁅R L₂'

An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image.

Equations
@[simp]
theorem lie_algebra.equiv.of_subalgebras_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁' : lie_subalgebra R L₁) (L₂' : lie_subalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : lie_subalgebra.map e L₁' = L₂') (x : L₁') :

@[simp]
theorem lie_algebra.equiv.of_subalgebras_symm_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁' : lie_subalgebra R L₁) (L₂' : lie_subalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : lie_subalgebra.map e L₁' = L₂') (x : L₂') :

structure lie_submodule (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] :
Type w

A Lie submodule of a Lie module is a submodule that is closed under the Lie bracket. This is a sufficient condition for the subset itself to form a Lie module.

@[instance]
def lie_submodule.has_zero (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] :

The zero module is a Lie submodule of any Lie module.

Equations
@[instance]
def lie_submodule.inhabited (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] :

Equations
@[instance]
def lie_submodule_coe_submodule (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] :

Equations
@[instance]
def lie_submodule_has_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] :

Equations
@[instance]
def lie_submodule_act (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) :

Equations
@[instance]
def lie_submodule_lie_module (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) :

Equations
@[class]
structure lie_module.is_irreducible (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] :
Prop

A Lie module is irreducible if its only non-trivial Lie submodule is itself.

@[class]
structure lie_algebra.is_simple (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Prop

A Lie algebra is simple if it is irreducible as a Lie module over itself via the adjoint action, and it is non-Abelian.

def lie_ideal (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Type v

An ideal of a Lie algebra is a Lie submodule of the Lie algebra as a Lie module over itself.

theorem lie_mem_right (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) (x y : L) (h : y I) :

theorem lie_mem_left (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) (x y : L) (h : x I) :

def lie_ideal_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :

An ideal of a Lie algebra is a Lie subalgebra.

Equations
def lie_submodule.quotient {R : Type u} {L M : Type v} [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) :
Type v

The quotient of a Lie module by a Lie submodule. It is a Lie module.

def lie_submodule.quotient.mk {R : Type u} {L M : Type v} [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} :
M → N.quotient

Map sending an element of M to the corresponding element of M/N, when N is a lie_submodule of the lie_module N.

theorem lie_submodule.quotient.is_quotient_mk {R : Type u} {L M : Type v} [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} (m : M) :

Given a Lie module M over a Lie algebra L, together with a Lie submodule N ⊆ M, there is a natural linear map from L to the endomorphisms of M leaving N invariant.

Equations
def lie_submodule.quotient.action_as_endo_map {R : Type u} {L M : Type v} [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) :

Given a Lie module M over a Lie algebra L, together with a Lie submodule N ⊆ M, there is a natural Lie algebra morphism from L to the linear endomorphism of the quotient M/N.

Equations

Given a Lie module M over a Lie algebra L, together with a Lie submodule N ⊆ M, there is a natural bracket action of L on the quotient M/N.

Equations
@[instance]
def lie_submodule.quotient.lie_quotient_lie_module {R : Type u} {L M : Type v} [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) :

The quotient of a Lie module by a Lie submodule, is a Lie module.

Equations
@[instance]

Equations
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₂) :

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

Equations
@[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

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

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

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

### Matrices

An important class of Lie algebras are those arising from the associative algebra structure on square matrices over a commutative ring.

def lie_equiv_matrix' {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] :
module.End R (n → R) ≃ₗ⁅R matrix n n R

The natural equivalence between linear endomorphisms of finite free modules and square matrices is compatible with the Lie algebra structures.

Equations
@[simp]
theorem lie_equiv_matrix'_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (f : module.End R (n → R)) :

@[simp]
theorem lie_equiv_matrix'_symm_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (A : matrix n n R) :

def matrix.lie_conj {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (P : matrix n n R) (h : is_unit P) :

An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself.

Equations
@[simp]
theorem matrix.lie_conj_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (P A : matrix n n R) (h : is_unit P) :
(P.lie_conj h) A = P A P⁻¹

@[simp]
theorem matrix.lie_conj_symm_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (P A : matrix n n R) (h : is_unit P) :
((P.lie_conj h).symm) A = P⁻¹ A P

def matrix.reindex_lie_equiv {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] {m : Type w₁} [decidable_eq m] [fintype m] (e : n m) :

For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence of Lie algebras.

Equations
@[simp]
theorem matrix.reindex_lie_equiv_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] {m : Type w₁} [decidable_eq m] [fintype m] (e : n m) (M : matrix n n R) :
(matrix.reindex_lie_equiv e) M = λ (i j : m), M ((e.symm) i) ((e.symm) j)

@[simp]
theorem matrix.reindex_lie_equiv_symm_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] {m : Type w₁} [decidable_eq m] [fintype m] (e : n m) (M : matrix m m R) :
((matrix.reindex_lie_equiv e).symm) M = λ (i j : n), M (e i) (e j)