mathlib docs: algebra.lie.basic

source

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

for the product ⁅x, y⁆ of two elements x, y in a Lie algebra (analogous to has_mul in the associative setting),
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

source

@[class]

structure lie_ring (L : Type v) :

Type v

to_add_comm_group : add_comm_group L
to_has_bracket : has_bracket L L
add_lie : ∀ (x y z : L), ⁅x + y,z⁆ = ⁅x,z⁆ + ⁅y,z⁆
lie_add : ∀ (x y z : L), ⁅x,y + z⁆ = ⁅x,y⁆ + ⁅x,z⁆
lie_self : ∀ (x : L), ⁅x,x⁆ = 0
leibniz_lie : ∀ (x y z : L), ⁅x,⁅y,z⁆⁆ = ⁅⁅x,y⁆,z⁆ + ⁅y,⁅x,z⁆⁆

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

source

@[class]

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

Type (max u v)

to_semimodule : semimodule R L
lie_smul : ∀ (t : R) (x y : L), ⁅x,t • y⁆ = t • ⁅x,y⁆

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

source

@[class]

structure lie_ring_module (L : Type v) (M : Type w) [lie_ring L] [add_comm_group M] :

Type (max v w)

to_has_bracket : has_bracket L M
add_lie : ∀ (x y : L) (m : M), ⁅x + y,m⁆ = ⁅x,m⁆ + ⁅y,m⁆
lie_add : ∀ (x : L) (m n : M), ⁅x,m + n⁆ = ⁅x,m⁆ + ⁅x,n⁆
leibniz_lie : ∀ (x y : L) (m : M), ⁅x,⁅y,m⁆⁆ = ⁅⁅x,y⁆,m⁆ + ⁅y,⁅x,m⁆⁆

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

source

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

smul_lie : ∀ (t : R) (x : L) (m : M), ⁅t • x,m⁆ = t • ⁅x,m⁆
lie_smul : ∀ (t : R) (x : L) (m : M), ⁅x,t • m⁆ = t • ⁅x,m⁆

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

source

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

⁅x + y,m⁆ = ⁅x,m⁆ + ⁅y,m⁆

source

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

⁅x,m + n⁆ = ⁅x,m⁆ + ⁅x,n⁆

source

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

⁅t • x,m⁆ = t • ⁅x,m⁆

source

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

⁅x,t • m⁆ = t • ⁅x,m⁆

source

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

⁅x,⁅y,m⁆⁆ = ⁅⁅x,y⁆,m⁆ + ⁅y,⁅x,m⁆⁆

source

@[simp]

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

⁅x,0⁆ = 0

source

@[simp]

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

⁅0,m⁆ = 0

source

@[simp]

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

⁅x,x⁆ = 0

source

@[instance]

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

lie_ring_module L L

Equations

lie_ring_self_module = {to_has_bracket := lie_ring.to_has_bracket infer_instance, add_lie := _, lie_add := _, leibniz_lie := _}

source

@[simp]

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

-⁅y,x⁆ = ⁅x,y⁆

source

@[instance]

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

lie_module R L L

Every Lie algebra is a module over itself.

Equations

lie_algebra_self_module = {smul_lie := _, lie_smul := _}

source

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

⁅-x,m⁆ = -⁅x,m⁆

source

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

⁅x,-m⁆ = -⁅x,m⁆

source

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

⁅a • x,m⁆ = a • ⁅x,m⁆

source

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

⁅x,a • m⁆ = a • ⁅x,m⁆

source

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

⁅⁅x,y⁆,m⁆ = ⁅x,⁅y,m⁆⁆ - ⁅y,⁅x,m⁆⁆

source

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

⁅x,⁅y,z⁆⁆ + ⁅y,⁅z,x⁆⁆ + ⁅z,⁅x,y⁆⁆ = 0

source

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

source

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)

to_fun : L → L'
map_add' : ∀ (x y : L), c.to_fun (x + y) = c.to_fun x + c.to_fun y
map_smul' : ∀ (m : R) (x : L), c.to_fun (m • x) = m • c.to_fun x
map_lie : ∀ {x y : L}, c.to_fun ⁅x,y⁆ = ⁅c.to_fun x,c.to_fun y⁆

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

source

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

lie_algebra.linear_map.has_coe = {coe := lie_algebra.morphism.to_linear_map _inst_6}

source

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

has_coe_to_fun (L₁ →ₗ⁅R⁆ L₂)

see Note [function coercion]

Equations

lie_algebra.morphism.has_coe_to_fun = {F := λ (x : L₁ →ₗ⁅R⁆ L₂), L₁ → L₂, coe := lie_algebra.morphism.to_fun _inst_6}

source

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

source

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

⇑↑f = ⇑f

source

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

⇑f ⁅x,y⁆ = ⁅⇑f x,⇑f y⁆

source

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

lie_algebra.morphism.has_zero = {zero := {to_fun := 0.to_fun, map_add' := _, map_smul' := _, map_lie := _}}

source

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

lie_algebra.morphism.has_one = {one := {to_fun := 1.to_fun, map_add' := _, map_smul' := _, map_lie := _}}

source

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

lie_algebra.morphism.inhabited = {default := 0}

source

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)

source

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

source

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

source

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

f.comp g = {to_fun := (f.to_linear_map.comp g.to_linear_map).to_fun, map_add' := _, map_smul' := _, map_lie := _}

source

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

source

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)

source

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

f.inverse g h₁ h₂ = {to_fun := (f.to_linear_map.inverse g h₁ h₂).to_fun, map_add' := _, map_smul' := _, map_lie := _}

source

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)

to_fun : L → L'
map_add' : ∀ (x y : L), c.to_fun (x + y) = c.to_fun x + c.to_fun y
map_smul' : ∀ (m : R) (x : L), c.to_fun (m • x) = m • c.to_fun x
map_lie : ∀ {x y : L}, c.to_fun ⁅x,y⁆ = ⁅c.to_fun x,c.to_fun y⁆
inv_fun : L' → L
left_inv : function.left_inverse c.inv_fun c.to_fun
right_inv : function.right_inverse c.inv_fun c.to_fun

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.

source

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

source

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

L →ₗ⁅R⁆ L'

source

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

lie_algebra.equiv.has_coe_to_lie_hom = {coe := lie_algebra.equiv.to_morphism _inst_6}

source

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

lie_algebra.equiv.has_coe_to_linear_equiv = {coe := lie_algebra.equiv.to_linear_equiv _inst_6}

source

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

has_coe_to_fun (L₁ ≃ₗ⁅R⁆ L₂)

see Note [function coercion]

Equations

lie_algebra.equiv.has_coe_to_fun = {F := λ (x : L₁ ≃ₗ⁅R⁆ L₂), L₁ → L₂, coe := lie_algebra.equiv.to_fun _inst_6}

source

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

⇑↑e = ⇑e

source

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

⇑↑e = ⇑e

source

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

lie_algebra.equiv.has_one = {one := {to_fun := 1.to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := 1.inv_fun, left_inv := _, right_inv := _}}

source

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

source

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

lie_algebra.equiv.inhabited = {default := 1}

source

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

lie_algebra.equiv.refl = 1

source

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

⇑lie_algebra.equiv.refl x = x

source

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

e.symm = {to_fun := (e.to_morphism.inverse e.inv_fun _ _).to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := e.to_linear_equiv.symm.inv_fun, left_inv := _, right_inv := _}

source

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

source

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

source

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

source

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

e₁.trans e₂ = {to_fun := (e₂.to_morphism.comp e₁.to_morphism).to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}

source

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

source

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

source

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₁)

to_fun : M → N
map_add' : ∀ (x y : M), c.to_fun (x + y) = c.to_fun x + c.to_fun y
map_smul' : ∀ (m : R) (x : M), c.to_fun (m • x) = m • c.to_fun x
map_lie : ∀ {x : L} {m : M}, c.to_fun ⁅x,m⁆ = ⁅x,c.to_fun m⁆

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

source

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

M →ₗ[R] N

source

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

has_coe (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N)

Equations

lie_module_hom.linear_map.has_coe = {coe := lie_module_hom.to_linear_map _inst_14}

source

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

has_coe_to_fun (M →ₗ⁅R,L⁆ N)

see Note [function coercion]

Equations

lie_module_hom.has_coe_to_fun = {F := λ (x : M →ₗ⁅R,L⁆ N), M → N, coe := lie_module_hom.to_fun _inst_14}

source

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

source

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

⇑↑f = ⇑f

source

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

⇑f ⁅x,m⁆ = ⁅x,⇑f m⁆

source

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

has_zero (M →ₗ⁅R,L⁆ N)

The constant 0 map is a Lie module morphism.

Equations

lie_module_hom.has_zero = {zero := {to_fun := 0.to_fun, map_add' := _, map_smul' := _, map_lie := _}}

source

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

has_one (M →ₗ⁅R,L⁆ M)

The identity map is a Lie module morphism.

Equations

lie_module_hom.has_one = {one := {to_fun := 1.to_fun, map_add' := _, map_smul' := _, map_lie := _}}

source

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

inhabited (M →ₗ⁅R,L⁆ N)

Equations

lie_module_hom.inhabited = {default := 0}

source

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)

source

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

source

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

source

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

M →ₗ⁅R,L⁆ P

The composition of Lie module morphisms is a morphism.

Equations

f.comp g = {to_fun := (f.to_linear_map.comp g.to_linear_map).to_fun, map_add' := _, map_smul' := _, map_lie := _}

source

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

source

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)

source

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

N →ₗ⁅R,L⁆ M

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

Equations

f.inverse g h₁ h₂ = {to_fun := (f.to_linear_map.inverse g h₁ h₂).to_fun, map_add' := _, map_smul' := _, map_lie := _}

source

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₁)

to_fun : M → N
map_add' : ∀ (x y : M), c.to_fun (x + y) = c.to_fun x + c.to_fun y
map_smul' : ∀ (m : R) (x : M), c.to_fun (m • x) = m • c.to_fun x
inv_fun : N → M
left_inv : function.left_inverse c.inv_fun c.to_fun
right_inv : function.right_inverse c.inv_fun c.to_fun
map_lie : ∀ {x : L} {m : M}, c.to_fun ⁅x,m⁆ = ⁅x,c.to_fun m⁆

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

source

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

M ≃ₗ[R] N

source

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

M →ₗ⁅R,L⁆ N

source

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

has_coe (M ≃ₗ⁅R,L⁆ N) (M →ₗ⁅R,L⁆ N)

Equations

lie_module_equiv.has_coe_to_lie_module_hom = {coe := lie_module_equiv.to_lie_module_hom _inst_14}

source

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

has_coe (M ≃ₗ⁅R,L⁆ N) (M ≃ₗ[R] N)

Equations

lie_module_equiv.has_coe_to_linear_equiv = {coe := lie_module_equiv.to_linear_equiv _inst_14}

source

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

has_coe_to_fun (M ≃ₗ⁅R,L⁆ N)

see Note [function coercion]

Equations

lie_module_equiv.has_coe_to_fun = {F := λ (x : M ≃ₗ⁅R,L⁆ N), M → N, coe := lie_module_equiv.to_fun _inst_14}

source

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

⇑↑e = ⇑e

source

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

⇑↑e = ⇑e

source

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

has_one (M ≃ₗ⁅R,L⁆ M)

Equations

lie_module_equiv.has_one = {one := {to_fun := 1.to_fun, map_add' := _, map_smul' := _, inv_fun := 1.inv_fun, left_inv := _, right_inv := _, map_lie := _}}

source

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

source

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

inhabited (M ≃ₗ⁅R,L⁆ M)

Equations

lie_module_equiv.inhabited = {default := 1}

source

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] :

M ≃ₗ⁅R,L⁆ M

Lie module equivalences are reflexive.

Equations

lie_module_equiv.refl = 1

source

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

⇑lie_module_equiv.refl m = m

source

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

N ≃ₗ⁅R,L⁆ M

Lie module equivalences are syemmtric.

Equations

e.symm = {to_fun := (e.to_lie_module_hom.inverse e.inv_fun _ _).to_fun, map_add' := _, map_smul' := _, inv_fun := ↑e.symm.inv_fun, left_inv := _, right_inv := _, map_lie := _}

source

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

source

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

source

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

source

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

M ≃ₗ⁅R,L⁆ P

Lie module equivalences are transitive.

Equations

e₁.trans e₂ = {to_fun := (e₂.to_lie_module_hom.comp e₁.to_lie_module_hom).to_fun, map_add' := _, map_smul' := _, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _, map_lie := _}

source

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

source

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

source

@[instance]

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

ring_commutator.has_bracket = {bracket := λ (x y : A), x * y - y * x}

source

theorem ring_commutator.commutator {A : Type v} [ring A] (x y : A) :

⁅x,y⁆ = x * y - y * x

source

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

lie_ring.of_associative_ring = {to_add_comm_group := ring.to_add_comm_group A _inst_1, to_has_bracket := ring_commutator.has_bracket _inst_1, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}

source

theorem lie_ring.of_associative_ring_bracket {A : Type v} [ring A] (x y : A) :

⁅x,y⁆ = x * y - y * x

source

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

source

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

is_commutative A has_mul.mul ↔ is_lie_abelian A

source

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

lie_algebra.of_associative_algebra = {to_semimodule := algebra.to_semimodule _inst_3, lie_smul := _}

source

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

A →ₗ⁅R⁆ B

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

Equations

lie_algebra.of_associative_algebra_hom f = {to_fun := f.to_linear_map.to_fun, map_add' := _, map_smul' := _, map_lie := _}

source

@[simp]

theorem lie_algebra.of_associative_algebra_hom_id {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] :

lie_algebra.of_associative_algebra_hom (alg_hom.id R A) = 1

source

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

⇑(lie_algebra.of_associative_algebra_hom f) x = ⇑f x

source

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

lie_algebra.of_associative_algebra_hom (g.comp f) = (lie_algebra.of_associative_algebra_hom g).comp (lie_algebra.of_associative_algebra_hom f)

source

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] :

L →ₗ⁅R⁆ module.End R M

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

Equations

lie_module.to_endo_morphism R L M = {to_fun := λ (x : L), {to_fun := λ (m : M), ⁅x,m⁆, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _, map_lie := _}

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

lie_algebra.ad R L = lie_module.to_endo_morphism R L L

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

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

Type v

carrier : set L
zero_mem' : 0 ∈ c.carrier
add_mem' : ∀ {a b : L}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
smul_mem' : ∀ (c_1 : R) {x : L}, x ∈ c.carrier → c_1 • x ∈ c.carrier
lie_mem : ∀ {x y : L}, x ∈ c.carrier → y ∈ c.carrier → ⁅x,y⁆ ∈ c.carrier

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.

source

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

submodule R L

source

@[instance]

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

has_zero (lie_subalgebra R L)

The zero algebra is a subalgebra of any Lie algebra.

Equations

lie_subalgebra.has_zero R L = {zero := {carrier := 0.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}}

source

@[instance]

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

inhabited (lie_subalgebra R L)

Equations

lie_subalgebra.inhabited R L = {default := 0}

source

@[instance]

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

has_coe (lie_subalgebra R L) (set L)

Equations

set.has_coe R L = {coe := lie_subalgebra.carrier _inst_3}

source

@[instance]

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

has_mem L (lie_subalgebra R L)

Equations

lie_subalgebra.has_mem R L = {mem := λ (x : L) (L' : lie_subalgebra R L), x ∈ ↑L'}

source

@[instance]

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

has_coe (lie_subalgebra R L) (submodule R L)

Equations

lie_subalgebra_coe_submodule R L = {coe := lie_subalgebra.to_submodule _inst_3}

source

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

lie_ring ↥L'

A Lie subalgebra forms a new Lie ring.

Equations

lie_subalgebra_lie_ring R L L' = {to_add_comm_group := (has_coe_t_aux.coe L').add_comm_group, to_has_bracket := {bracket := λ (x y : ↥L'), ⟨⁅x.val ,y.val ⁆, _⟩}, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}

source

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

lie_algebra R ↥L'

A Lie subalgebra forms a new Lie algebra.

Equations

lie_subalgebra_lie_algebra R L L' = {to_semimodule := submodule.restricted_module R R L (has_coe_t_aux.coe L'), lie_smul := _}

source

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

source

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

source

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

↑⁅x,y⁆ = ⁅↑x,↑y⁆

source

@[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₂'

source

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₂'

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

lie_subalgebra_of_subalgebra R A A' = {carrier := A'.to_submodule.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}

source

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

↥L' →ₗ⁅R⁆ L

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

Equations

L'.incl = {to_fun := L'.to_submodule.subtype.to_fun, map_add' := _, map_smul' := _, map_lie := _}

source

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

lie_subalgebra R L₂

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

Equations

f.range = {carrier := f.to_linear_map.range.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}

source

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

↑⁅x,y⁆ = ⁅↑x,↑y⁆

source

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

lie_subalgebra R L₂

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

Equations

lie_subalgebra.map f L' = {carrier := (submodule.map ↑f ↑L').carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}

source

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

x ∈ lie_subalgebra.map ↑e L' ↔ x ∈ submodule.map ↑e ↑L'

source

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

L₁ ≃ₗ⁅R⁆ ↥(f.range)

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

Equations

lie_algebra.equiv.of_injective f h = have h' : ↑f.ker = ⊥, from _, {to_fun := (linear_equiv.of_injective ↑f h').to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := (linear_equiv.of_injective ↑f h').inv_fun, left_inv := _, right_inv := _}

source

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

↑(⇑(lie_algebra.equiv.of_injective f h) x) = ⇑f x

source

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

lie_algebra.equiv.of_eq L₁' L₁'' h = {to_fun := (linear_equiv.of_eq ↑L₁' ↑L₁'' _).to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := (linear_equiv.of_eq ↑L₁' ↑L₁'' _).inv_fun, left_inv := _, right_inv := _}

source

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

↑(⇑(lie_algebra.equiv.of_eq L L' h) x) = ↑x

source

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

↥L₁'' ≃ₗ⁅R⁆ ↥(lie_subalgebra.map ↑e L₁'')

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

Equations

lie_algebra.equiv.of_subalgebra L₁'' e = {to_fun := (↑e.of_submodule ↑L₁'').to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := (↑e.of_submodule ↑L₁'').inv_fun, left_inv := _, right_inv := _}

source

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

↑(⇑(lie_algebra.equiv.of_subalgebra L₁'' e) x) = ⇑e ↑x

source

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

lie_algebra.equiv.of_subalgebras L₁' L₂' e h = {to_fun := (↑e.of_submodules ↑L₁' ↑L₂' _).to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := (↑e.of_submodules ↑L₁' ↑L₂' _).inv_fun, left_inv := _, right_inv := _}

source

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

↑(⇑(lie_algebra.equiv.of_subalgebras L₁' L₂' e h) x) = ⇑e ↑x

source

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

↑(⇑((lie_algebra.equiv.of_subalgebras L₁' L₂' e h).symm) x) = ⇑(e.symm) ↑x

source

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

to_submodule : submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ c.to_submodule.carrier → ⁅x,m⁆ ∈ c.to_submodule.carrier

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.

source

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

has_zero (lie_submodule R L M)

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

Equations

lie_submodule.has_zero R L M = {zero := {to_submodule := {carrier := 0.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _}, lie_mem := _}}

source

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

inhabited (lie_submodule R L M)

Equations

lie_submodule.inhabited R L M = {default := 0}

source

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

has_coe (lie_submodule R L M) (submodule R M)

Equations

lie_submodule_coe_submodule R L M = {coe := lie_submodule.to_submodule _inst_7}

source

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

has_mem M (lie_submodule R L M)

Equations

lie_submodule_has_mem R L M = {mem := λ (x : M) (N : lie_submodule R L M), x ∈ ↑N}

source

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

lie_ring_module L ↥N

Equations

lie_submodule_act R L M N = {to_has_bracket := {bracket := λ (x : L) (m : ↥N), ⟨⁅x,m.val ⁆, _⟩}, add_lie := _, lie_add := _, leibniz_lie := _}

source

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

lie_module R L ↥N

Equations

lie_submodule_lie_module R L M N = {smul_lie := _, lie_smul := _}

source

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

irreducible : ∀ (M' : lie_submodule R L M), (∃ (m : ↥M'), m ≠ 0) → ∀ (m : M), m ∈ M'

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

source

@[class]

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

Prop

simple : lie_module.is_irreducible R L L ∧ ¬is_lie_abelian L

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

source

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.

source

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

⁅x,y⁆ ∈ I

source

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

⁅x,y⁆ ∈ I

source

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

lie_subalgebra R L

An ideal of a Lie algebra is a Lie subalgebra.

Equations

lie_ideal_subalgebra R L I = {carrier := I.to_submodule.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}

source

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.

source

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.

source

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

quotient.mk' m = lie_submodule.quotient.mk m

source

def lie_submodule.quotient.lie_submodule_invariant {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} :

L →ₗ[R] ↥(N.to_submodule.compatible_maps N.to_submodule)

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

lie_submodule.quotient.lie_submodule_invariant = linear_map.cod_restrict (N.to_submodule.compatible_maps N.to_submodule) ↑(lie_module.to_endo_morphism R L M) _

source

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

L →ₗ⁅R⁆ module.End R N.quotient

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

lie_submodule.quotient.action_as_endo_map N = {to_fun := ((↑N.mapq_linear ↑N).comp lie_submodule.quotient.lie_submodule_invariant).to_fun, map_add' := _, map_smul' := _, map_lie := _}

source

def lie_submodule.quotient.action_as_endo_map_bracket {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) :

has_bracket L N.quotient

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

lie_submodule.quotient.action_as_endo_map_bracket N = {bracket := λ (x : L) (n : N.quotient), ⇑(⇑(lie_submodule.quotient.action_as_endo_map N) x) n}

source

@[instance]

def lie_submodule.quotient.lie_quotient_lie_ring_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) :

lie_ring_module L N.quotient

Equations

lie_submodule.quotient.lie_quotient_lie_ring_module N = {to_has_bracket := {bracket := λ (x : L) (n : N.quotient), ⇑(⇑↑(lie_submodule.quotient.action_as_endo_map N) x) n}, add_lie := _, lie_add := _, leibniz_lie := _}

source

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

lie_module R L N.quotient

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

Equations

lie_submodule.quotient.lie_quotient_lie_module N = {smul_lie := _, lie_smul := _}

source

@[instance]

def lie_submodule.quotient.lie_quotient_has_bracket {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {I : lie_ideal R L} :

has_bracket (lie_submodule.quotient I) (lie_submodule.quotient I)

Equations

lie_submodule.quotient.lie_quotient_has_bracket = {bracket := λ (x y : lie_submodule.quotient I), quotient.lift_on₂' x y (λ (x' y' : L), lie_submodule.quotient.mk ⁅x',y'⁆) lie_submodule.quotient.lie_quotient_has_bracket._proof_1}

source

@[simp]

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

lie_submodule.quotient.mk ⁅x,y⁆ = ⁅lie_submodule.quotient.mk x,lie_submodule.quotient.mk y⁆

source

@[instance]

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

lie_ring (lie_submodule.quotient I)

Equations

lie_submodule.quotient.lie_quotient_lie_ring = {to_add_comm_group := submodule.quotient.add_comm_group I.to_submodule, to_has_bracket := lie_submodule.quotient.lie_quotient_has_bracket I, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}

source

@[instance]

def lie_submodule.quotient.lie_quotient_lie_algebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {I : lie_ideal R L} :

lie_algebra R (lie_submodule.quotient I)

Equations

lie_submodule.quotient.lie_quotient_lie_algebra = {to_semimodule := submodule.quotient.semimodule I.to_submodule, lie_smul := _}

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

e.lie_conj = {to_fun := e.conj.to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := e.conj.inv_fun, left_inv := _, right_inv := _}

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

e.to_lie_equiv = {to_fun := e.to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := e.to_linear_equiv.inv_fun, left_inv := _, right_inv := _}

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

source

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

lie_equiv_matrix' = {to_fun := linear_map.to_matrix'.to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := linear_map.to_matrix'.inv_fun, left_inv := _, right_inv := _}

source

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

⇑lie_equiv_matrix' f = ⇑linear_map.to_matrix' f

source

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

⇑(lie_equiv_matrix'.symm) A = ⇑matrix.to_lin' A

source

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

matrix n n R ≃ₗ⁅R⁆ matrix n n R

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

Equations

P.lie_conj h = (lie_equiv_matrix'.symm.trans (P.to_linear_equiv h).lie_conj).trans lie_equiv_matrix'

source

@[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⁻¹

source

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

source

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

matrix n n R ≃ₗ⁅R⁆ matrix m 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

matrix.reindex_lie_equiv e = {to_fun := (matrix.reindex_linear_equiv e e).to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := (matrix.reindex_linear_equiv e e).inv_fun, left_inv := _, right_inv := _}

source

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

source

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

mathlib documentation

Lie algebras

Notations

Implementation notes

References

Tags