# mathlibdocumentation

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:

• L →ₗ⁅R⁆ L' for a morphism of Lie algebras,
• L ≃ₗ⁅R⁆ L' for an equivalence of Lie algebras,
• M →ₗ⁅R,L⁆ N for a morphism of Lie algebra modules M, N over a Lie algebra L,
• M ≃ₗ⁅R,L⁆ N for an equivalence of Lie algebra modules M, N over a Lie algebra L.

## Implementation notes

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

## References

• [N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3][bourbaki1975]

## 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]  :
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] [ L] [ M] [ 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] [ M] (x y : L) (m : M) :

@[simp]
theorem lie_add {L : Type v} {M : Type w} [lie_ring 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] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] (t : R) (x : L) (m : M) :

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

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

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

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

@[instance]
def lie_ring_self_module {L : Type v} [lie_ring L] :

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

Every Lie algebra is a module over itself.

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

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

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

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

@[simp]
theorem lie_lie {L : Type v} {M : Type w} [lie_ring 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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₂] [ L₁] [ 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₂] [ L₁] [ L₂] :
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₂] [ L₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₃] [ L₁] [ L₂] [ 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₃] [ L₁] [ L₂] [ 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₃] [ L₁] [ L₂] [ 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₂] [ L₁] [ L₂] (f : L₁ →ₗ⁅R L₂) (g : L₂ → L₁) (h₁ : f) (h₂ : 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ L₂] :
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₂] [ L₁] [ 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₂] [ L₁] [ L₂] (e : L₁ ≃ₗ⁅R L₂) :

@[instance]
def lie_algebra.equiv.has_one {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [ 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₁] [ L₁] (x : L₁) :
1 x = x

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

Equations
def lie_algebra.equiv.refl {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [ 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₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₂] [ L₁] [ 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₃] [ L₁] [ L₂] [ 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₃] [ L₁] [ L₂] [ 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₃] [ L₁] [ L₂] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ L N] :
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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ P] [ M] [ N] [ P] [ L M] [ L N] [ 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] [ L] [ M] [ N] [ P] [ M] [ N] [ P] [ L M] [ L N] [ 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] [ L] [ M] [ N] [ P] [ M] [ N] [ P] [ L M] [ L N] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ L N] (f : M →ₗ⁅R,L N) (g : N → M) (h₁ : f) (h₂ : 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ L N] :
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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] :

Equations
def lie_module_equiv.refl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ M] [ N] [ L M] [ 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] [ L] [ M] [ N] [ P] [ M] [ N] [ P] [ L M] [ L N] [ 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] [ L] [ M] [ N] [ P] [ M] [ N] [ P] [ L M] [ L N] [ 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] [ L] [ M] [ N] [ P] [ M] [ N] [ P] [ L M] [ L N] [ 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] :
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) [ L] [has_zero L] :
Prop
• abelian : ∀ (x y : L), x,y = 0

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

theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [ring A] :

@[instance]
def lie_algebra.of_associative_algebra {A : Type v} [ring A] {R : Type u} [comm_ring R] [ A] :
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] [ A] {B : Type w} [ring B] [ 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_id {A : Type v} [ring A] {R : Type u} [comm_ring R] [ A] :

@[simp]
theorem lie_algebra.of_associative_algebra_hom_apply {A : Type v} [ring A] {R : Type u} [comm_ring R] [ A] {B : Type w} [ring B] [ 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] [ A] {B : Type w} {C : Type w₁} [ring B] [ring C] [ B] [ 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] [ L] [ M] [ M] [ 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] [ 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] [ L] (x y : L) :
( L) x) y = x,y

structure lie_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ 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] [ L] (s : L) :
L

@[instance]
def lie_subalgebra.has_zero (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ 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] [ L] :

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

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

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

Equations
@[instance]
def lie_subalgebra_lie_ring (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (L' : 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] [ L] (L' : L) :
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] [ L] {L' : 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] [ L] {L' : 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] [ L] (L' : L) (x y : L') :

@[ext]
theorem lie_subalgebra.ext (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (L₁' L₂' : 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] [ L] (L₁' L₂' : 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] [ A] (A' : 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] [ L] (L' : 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] [ L] {L₂ : Type w} [lie_ring L₂] [ L₂] (f : L →ₗ⁅R L₂) :
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] [ L] {L₂ : Type w} [lie_ring L₂] [ 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] [ L] {L₂ : Type w} [lie_ring L₂] [ L₂] (f : L →ₗ⁅R L₂) (L' : L) :
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] [ L] {L₂ : Type w} [lie_ring L₂] [ L₂] (e : L ≃ₗ⁅R L₂) (L' : L) (x : L₂) :
x 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₂] [ L₁] [ 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₂] [ L₁] [ L₂] (f : L₁ →ₗ⁅R L₂) (h : function.injective f) (x : L₁) :
x) = f x

def lie_algebra.equiv.of_eq {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [ L₁] (L₁' L₁'' : 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₁] [ L₁] (L L' : L₁) (h : L = L') (x : L) :
( h) x) = x

def lie_algebra.equiv.of_subalgebra {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [ L₁] [ L₂] (L₁'' : L₁) (e : L₁ ≃ₗ⁅R 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_subalgebra_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [ L₁] [ L₂] (L₁'' : L₁) (e : L₁ ≃ₗ⁅R L₂) (x : L₁'') :
( e) x) = e x

def lie_algebra.equiv.of_subalgebras {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [ L₁] [ L₂] (L₁' : L₁) (L₂' : L₂) (e : L₁ ≃ₗ⁅R L₂) (h : 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₂] [ L₁] [ L₂] (L₁' : L₁) (L₂' : L₂) (e : L₁ ≃ₗ⁅R L₂) (h : L₁' = L₂') (x : L₁') :
( L₂' e h) x) = e x

@[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₂] [ L₁] [ L₂] (L₁' : L₁) (L₂' : L₂) (e : L₁ ≃ₗ⁅R L₂) (h : L₁' = L₂') (x : L₂') :
( L₂' e h).symm) x) = (e.symm) x

structure lie_submodule (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
Type w
• to_submodule : M
• lie_mem : ∀ {x : L} {m : M},

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] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] :

Equations
@[instance]
def lie_submodule_coe_submodule (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
has_coe L M) M)

Equations
@[instance]
def lie_submodule_has_mem (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
L M)

Equations
@[instance]
def lie_submodule_act (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :

Equations
@[instance]
def lie_submodule_lie_module (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
L N

Equations
@[class]
structure lie_module.is_irreducible (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
Prop
• irreducible : ∀ (M' : M), (∃ (m : M'), m 0)∀ (m : M), m M'

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] [ L] :
Prop
• simple :

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] [ 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] [ L] (I : L) (x y : L) (h : y I) :

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

def lie_ideal_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : 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] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] {N : 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] [ L] [ M] [ M] [ L M] {N : M} (m : M) :

def lie_submodule.quotient.lie_submodule_invariant {R : Type u} {L M : Type v} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : 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] [ L] [ M] [ M] [ L M] (N : 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
def lie_submodule.quotient.action_as_endo_map_bracket {R : Type u} {L M : Type v} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :

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_ring_module {R : Type u} {L M : Type v} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :

Equations
@[instance]
def lie_submodule.quotient.lie_quotient_lie_module {R : Type u} {L M : Type v} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :

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

Equations
@[instance]
def lie_submodule.quotient.lie_quotient_has_bracket {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} :

Equations
@[simp]
theorem lie_submodule.quotient.mk_bracket {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} (x y : L) :

@[instance]
def lie_submodule.quotient.lie_quotient_lie_ring {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} :

Equations
@[instance]
def lie_submodule.quotient.lie_quotient_lie_algebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} :

Equations
def linear_equiv.lie_conj {R : Type u} {M₁ : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₁] [ M₁] [add_comm_group M₂] [ M₂] (e : M₁ ≃ₗ[R] M₂) :
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₁] [ M₁] [add_comm_group M₂] [ M₂] (e : M₁ ≃ₗ[R] M₂) (f : 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₁] [ M₁] [add_comm_group M₂] [ 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₂] [ A₁] [ 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₂] [ A₁] [ 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₂] [ A₁] [ 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] :
(n → R) ≃ₗ⁅R 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 : (n → R)) :

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

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

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 : 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 : 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) :
n R ≃ₗ⁅R m R

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 : n R) :
= λ (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 : m R) :
M = λ (i j : n), M (e i) (e j)