mathlib docs: algebra.lie

source

@[class]

structure has_bracket :

Type v → Type v

bracket : L → L → L

A binary operation, intended use in Lie algebras and similar structures.

Instances

source

@[class]

structure lie_algebra.is_abelian (L : Type v) [has_bracket L] [has_zero L] :

Prop

abelian : ∀ (x y : L), ⁅x,y⁆ = 0

An Abelian Lie algebra is one in which all brackets vanish. Arguably this class belongs in the has_bracket namespace but it seems much more user-friendly to compromise slightly and put it in the lie_algebra namespace.

source

@[instance]

def ring_commutator.has_bracket {A : Type v} [ring A] :

has_bracket 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

@[class]

structure lie_ring :

Type v → Type v

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

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

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

⁅x,x⁆ = 0

source

@[simp]

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

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

source

@[simp]

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

⁅x,0⁆ = 0

source

@[simp]

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

⁅0,x⁆ = 0

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem gsmul_lie {L : Type v} [lie_ring L] (x y : L) (n : ℤ) :

⁅n • x,y⁆ = n • ⁅x,y⁆

source

@[simp]

theorem lie_gsmul {L : Type v} [lie_ring L] (x y : L) (n : ℤ) :

⁅x,n • y⁆ = n • ⁅x,y⁆

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 A = {to_add_comm_group := ring.to_add_comm_group A _inst_2, to_has_bracket := ring_commutator.has_bracket _inst_2, add_lie := _, lie_add := _, lie_self := _, jacobi := _}

source

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

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

source

theorem commutative_ring_iff_abelian_lie_ring (A : Type v) [ring A] :

is_commutative A has_mul.mul ↔ lie_algebra.is_abelian A

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

@[simp]

theorem lie_smul (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (t : R) (x y : L) :

⁅x,t • y⁆ = t • ⁅x,y⁆

source

@[simp]

theorem smul_lie (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (t : R) (x y : L) :

⁅t • x,y⁆ = t • ⁅x,y⁆

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' : ∀ (c_1 : R) (x : L), c.to_fun (c_1 • x) = c_1 • 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

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

(L →ₗ⁅R⁆ L') → (L →ₗ[R] L')

source

@[instance]

def lie_algebra.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.has_coe = {coe := lie_algebra.morphism.to_linear_map _inst_6}

source

@[instance]

def lie_algebra.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.has_coe_to_fun = {F := λ (x : L₁ →ₗ⁅R⁆ L₂), L₁ → L₂, coe := lie_algebra.morphism.to_fun _inst_6}

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.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.has_zero = {zero := {to_fun := 0.to_fun, map_add' := _, map_smul' := _, map_lie := _}}

source

@[instance]

def lie_algebra.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.has_one = {one := {to_fun := 1.to_fun, map_add' := _, map_smul' := _, map_lie := _}}

source

@[instance]

def lie_algebra.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.inhabited = {default := 0}

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

(L₂ →ₗ⁅R⁆ L₃) → (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

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

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

function.left_inverse g ⇑f → 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' : ∀ (c_1 : R) (x : L), c.to_fun (c_1 • x) = c_1 • 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_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'] :

(L ≃ₗ⁅R⁆ L') → (L →ₗ⁅R⁆ L')

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

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

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

(L₁ ≃ₗ⁅R⁆ L₂) → (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

@[instance]

def lie_algebra.direct_sum.lie_ring {ι : Type v} [decidable_eq ι] {L : ι → Type w} [Π (i : ι), lie_ring (L i)] :

lie_ring (direct_sum ι (λ (i : ι), L i))

The direct sum of Lie rings carries a natural Lie ring structure.

Equations

lie_algebra.direct_sum.lie_ring = {to_add_comm_group := {add := add_comm_group.add infer_instance, add_assoc := _, zero := add_comm_group.zero infer_instance, zero_add := _, add_zero := _, neg := add_comm_group.neg infer_instance, add_left_neg := _, add_comm := _}, to_has_bracket := {bracket := dfinsupp.zip_with (λ (i : ι) (x y : (λ (i : ι), L i) i), ⁅x,y⁆) lie_algebra.direct_sum.lie_ring._proof_6}, add_lie := _, lie_add := _, lie_self := _, jacobi := _}

source

@[simp]

theorem lie_algebra.direct_sum.bracket_apply {ι : Type v} [decidable_eq ι] {L : ι → Type w} [Π (i : ι), lie_ring (L i)] {x y : direct_sum ι (λ (i : ι), L i)} {i : ι} :

⇑⁅x,y⁆ i = ⁅⇑x i,⇑y i⁆

source

@[instance]

def lie_algebra.direct_sum.lie_algebra {R : Type u} [comm_ring R] {ι : Type v} [decidable_eq ι] {L : ι → Type w} [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] :

lie_algebra R (direct_sum ι (λ (i : ι), L i))

The direct sum of Lie algebras carries a natural Lie algebra structure.

Equations

lie_algebra.direct_sum.lie_algebra = {to_semimodule := {to_distrib_mul_action := semimodule.to_distrib_mul_action infer_instance, add_smul := _, zero_smul := _}, lie_smul := _}

source

@[instance]

def lie_algebra.lie_algebra.of_associative_algebra {R : Type u} [comm_ring R] {A : Type v} [ring A] [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.lie_algebra.of_associative_algebra = {to_semimodule := algebra.to_semimodule _inst_5, lie_smul := _}

source

@[instance]

def lie_algebra.lie_ring {R : Type u} [comm_ring R] (M : Type v) [add_comm_group M] [module R M] :

lie_ring (module.End R M)

Equations

lie_algebra.lie_ring M = lie_ring.of_associative_ring (module.End R M)

source

def lie_algebra.of_associative_algebra_hom {R : Type u} {A : Type v} {B : Type w} [comm_ring R] [ring A] [ring B] [algebra R A] [algebra R B] :

(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 {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] :

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

source

@[simp]

theorem lie_algebra.of_associative_algebra_hom_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [comm_ring R] [ring A] [ring B] [ring C] [algebra R A] [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

theorem lie_algebra.endo_algebra_bracket {R : Type u} [comm_ring R] (M : Type v) [add_comm_group M] [module R M] (f g : module.End R M) :

⁅f,g⁆ = linear_map.comp f g - linear_map.comp g f

An important class of Lie algebras are those arising from the associative algebra structure on module endomorphisms. We state a lemma and give a definition concerning them.

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 = {to_fun := λ (x : L), {to_fun := has_bracket.bracket x, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _, map_lie := _}

source

@[nolint]

def lie_subalgebra.to_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :

lie_subalgebra R L → submodule R L

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

@[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 := _, jacobi := _}

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 := (has_coe_t_aux.coe L').semimodule, 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) :

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

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

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

(L →ₗ⁅R⁆ 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₂) :

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

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

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

@[class]

structure lie_module (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R M] :

Type v

to_linear_action : linear_action R L M
lie_act : ∀ (l l' : L) (m : M), linear_action.act R ⁅l,l'⁆ m = linear_action.act R l (linear_action.act R l' m) - linear_action.act R l' (linear_action.act R l 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 lie_act (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R M] [lie_module R L M] (l l' : L) (m : M) :

linear_action.act R ⁅l,l'⁆ m = linear_action.act R l (linear_action.act R l' m) - linear_action.act R l' (linear_action.act R l m)

source

theorem of_endo_map_action (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R M] (α : L →ₗ⁅R⁆ module.End R M) (x : L) (m : M) :

linear_action.act R x m = ⇑(⇑α x) m

source

def lie_module.of_endo_morphism (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R M] :

(L →ₗ⁅R⁆ module.End R M) → lie_module R L M

A Lie morphism from a Lie algebra to the endomorphism algebra of a module yields a Lie module structure.

Equations

lie_module.of_endo_morphism R L M α = {to_linear_action := {act := linear_action.act R (linear_action.of_endo_map R L M ↑α), add_act := _, act_add := _, act_smul := _, smul_act := _}, lie_act := _}

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 R L = lie_module.of_endo_morphism R L L lie_algebra.Ad

source

structure lie_submodule (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R M] [lie_module R L M] :

Type v

to_submodule : submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ c.to_submodule.carrier → linear_action.act R 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) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R 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) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R 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) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R 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_6}

source

@[instance]

def lie_submodule_has_mem (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R 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_lie_module (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R 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 = {to_linear_action := {act := λ (x : L) (m : ↥N), ⟨linear_action.act R x m.val, _⟩, add_act := _, act_add := _, act_smul := _, smul_act := _}, lie_act := _}

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

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

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

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

@[class]

structure lie_module.is_irreducible (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type v) [add_comm_group M] [module R 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 ∧ ¬lie_algebra.is_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_submodule.quotient {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type v} [add_comm_group M] [module R M] [α : lie_module R L M] :

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 : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type v} [add_comm_group M] [module R 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 : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type v} [add_comm_group M] [module R 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 : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type v} [add_comm_group M] [module R 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) (linear_action.to_endo_map R L M lie_module.to_linear_action) _

source

@[instance]

def lie_submodule.quotient.lie_quotient_action {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type v} [add_comm_group M] [module R M] [α : lie_module R L M] {N : lie_submodule R L M} :

linear_action R L N.quotient

Equations

lie_submodule.quotient.lie_quotient_action = linear_action.of_endo_map R L N.quotient ((↑N.mapq_linear ↑N).comp lie_submodule.quotient.lie_submodule_invariant)

source

theorem lie_submodule.quotient.lie_quotient_action_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type v} [add_comm_group M] [module R M] [α : lie_module R L M] {N : lie_submodule R L M} (z : L) (m : M) :

linear_action.act R z (lie_submodule.quotient.mk m) = lie_submodule.quotient.mk (linear_action.act R z m)

source

@[instance]

def lie_submodule.quotient.lie_quotient_lie_module {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type v} [add_comm_group M] [module R 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 = {to_linear_action := {act := linear_action.act R lie_submodule.quotient.lie_quotient_action, add_act := _, act_add := _, act_smul := _, smul_act := _}, lie_act := _}

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)

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 := _, jacobi := _}

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

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

(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_equiv_matrix'.to_fun, map_add' := _, map_smul' := _, map_lie := _, inv_fun := linear_equiv_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 = A.to_lin

source

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

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.mul A).mul 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⁻¹.mul A).mul 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] :

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)

source

theorem bilin_form.is_skew_adjoint_bracket {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (B : bilin_form R M) (f g : module.End R M) :

f ∈ B.skew_adjoint_submodule → g ∈ B.skew_adjoint_submodule → ⁅f,g⁆ ∈ B.skew_adjoint_submodule

source

def skew_adjoint_lie_subalgebra {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :

bilin_form R M → lie_subalgebra R (module.End R M)

Given an R-module M, equipped with a bilinear form, the skew-adjoint endomorphisms form a Lie subalgebra of the Lie algebra of endomorphisms.

Equations

skew_adjoint_lie_subalgebra B = {carrier := B.skew_adjoint_submodule.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}

source

def skew_adjoint_lie_subalgebra_equiv {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (B : bilin_form R M) {N : Type w} [add_comm_group N] [module R N] (e : N ≃ₗ[R] M) :

↥(skew_adjoint_lie_subalgebra (B.comp ↑e ↑e)) ≃ₗ⁅R⁆ ↥(skew_adjoint_lie_subalgebra B)

An equivalence of modules with bilinear forms gives equivalence of Lie algebras of skew-adjoint endomorphisms.

Equations

skew_adjoint_lie_subalgebra_equiv B e = lie_algebra.equiv.of_subalgebras (skew_adjoint_lie_subalgebra (B.comp ↑e ↑e)) (skew_adjoint_lie_subalgebra B) e.lie_conj _

source

@[simp]

theorem skew_adjoint_lie_subalgebra_equiv_apply {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (B : bilin_form R M) {N : Type w} [add_comm_group N] [module R N] (e : N ≃ₗ[R] M) (f : ↥(skew_adjoint_lie_subalgebra (B.comp ↑e ↑e))) :

↑(⇑(skew_adjoint_lie_subalgebra_equiv B e) f) = ⇑(e.lie_conj) ↑f

source

@[simp]

theorem skew_adjoint_lie_subalgebra_equiv_symm_apply {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (B : bilin_form R M) {N : Type w} [add_comm_group N] [module R N] (e : N ≃ₗ[R] M) (f : ↥(skew_adjoint_lie_subalgebra B)) :

↑(⇑((skew_adjoint_lie_subalgebra_equiv B e).symm) f) = ⇑(e.symm.lie_conj) ↑f

source

theorem matrix.lie_transpose {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (A B : matrix n n R) :

⁅A,B⁆.transpose = ⁅B.transpose ,A.transpose ⁆

source

theorem matrix.is_skew_adjoint_bracket {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J A B : matrix n n R) :

A ∈ skew_adjoint_matrices_submodule J → B ∈ skew_adjoint_matrices_submodule J → ⁅A,B⁆ ∈ skew_adjoint_matrices_submodule J

source

def skew_adjoint_matrices_lie_subalgebra {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] :

matrix n n R → lie_subalgebra R (matrix n n R)

The Lie subalgebra of skew-adjoint square matrices corresponding to a square matrix J.

Equations

skew_adjoint_matrices_lie_subalgebra J = {carrier := (skew_adjoint_matrices_submodule J).carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}

source

@[simp]

theorem mem_skew_adjoint_matrices_lie_subalgebra {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J A : matrix n n R) :

A ∈ skew_adjoint_matrices_lie_subalgebra J ↔ A ∈ skew_adjoint_matrices_submodule J

source

def skew_adjoint_matrices_lie_subalgebra_equiv {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J P : matrix n n R) :

is_unit P → (↥(skew_adjoint_matrices_lie_subalgebra J) ≃ₗ⁅R⁆ ↥(skew_adjoint_matrices_lie_subalgebra ((P.transpose.mul J).mul P)))

An invertible matrix P gives a Lie algebra equivalence between those endomorphisms that are skew-adjoint with respect to a square matrix J and those with respect to PᵀJP.

Equations