algebra.lie.basic - mathlib docs

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.

Instances

source

@[class]

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

Type (max u v)

to_module : module 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 sub_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_sub {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 nsmul_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) (n : ℕ) :

⁅n • x,m⁆ = n • ⁅x,m⁆

source

@[simp]

theorem lie_nsmul {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) (n : ℕ) :

⁅x,n • m⁆ = n • ⁅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

@[instance]

def lie_ring.int_lie_algebra {L : Type v} [lie_ring L] :

lie_algebra ℤ L

Equations

lie_ring.int_lie_algebra = {to_module := add_comm_group.int_module L lie_ring.to_add_comm_group, lie_smul := _}

source

@[instance]

def linear_map.lie_ring_module {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] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] :

lie_ring_module L (M →ₗ[R] N)

Equations

linear_map.lie_ring_module = {to_has_bracket := {bracket := λ (x : L) (f : M →ₗ[R] N), {to_fun := λ (m : M), ⁅x,⇑f m⁆ - ⇑f ⁅x,m⁆, map_add' := _, map_smul' := _}}, add_lie := _, lie_add := _, leibniz_lie := _}

source

@[simp]

theorem lie_hom.lie_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] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ[R] N) (x : L) (m : M) :

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

source

@[instance]

def linear_map.lie_module {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] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] :

lie_module R L (M →ₗ[R] N)

Equations

linear_map.lie_module = {smul_lie := _, lie_smul := _}

source

@[nolint]

def lie_hom.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'] (self : L →ₗ⁅R⁆ L') :

L →ₗ[R] L'

source

structure lie_hom (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_hom.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_hom.linear_map.has_coe = {coe := lie_hom.to_linear_map _inst_6}

source

@[instance]

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

source

@[simp]

theorem lie_hom.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_hom.to_fun_eq_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₂] (f : L₁ →ₗ⁅R⁆ L₂) :

f.to_fun = ⇑f

source

@[simp]

theorem lie_hom.map_smul {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₂) (c : R) (x : L₁) :

⇑f (c • x) = c • ⇑f x

source

@[simp]

theorem lie_hom.map_add {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

@[simp]

theorem lie_hom.map_sub {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

@[simp]

theorem lie_hom.map_neg {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 : L₁) :

⇑f (-x) = -⇑f x

source

@[simp]

theorem lie_hom.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

@[simp]

theorem lie_hom.map_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₂] (f : L₁ →ₗ⁅R⁆ L₂) :

⇑f 0 = 0

source

def lie_hom.id {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :

L₁ →ₗ⁅R⁆ L₁

The identity map is a morphism of Lie algebras.

Equations

lie_hom.id = {to_fun := linear_map.id.to_fun, map_add' := _, map_smul' := _, map_lie' := _}

source

@[simp]

theorem lie_hom.coe_id {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :

⇑lie_hom.id = id

source

theorem lie_hom.id_apply {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (x : L₁) :

⇑lie_hom.id x = x

source

@[instance]

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

source

@[simp]

theorem lie_hom.coe_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₂] :

⇑0 = 0

source

theorem lie_hom.zero_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₂] (x : L₁) :

⇑0 x = 0

source

@[instance]

def lie_hom.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_hom.has_one = {one := lie_hom.id _inst_5}

source

@[simp]

theorem lie_hom.coe_one {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :

⇑1 = id

source

theorem lie_hom.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_hom.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_hom.inhabited = {default := 0}

source

theorem lie_hom.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 coe_fn

source

@[ext]

theorem lie_hom.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_hom.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

theorem lie_hom.congr_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₂] {f g : L₁ →ₗ⁅R⁆ L₂} (h : f = g) (x : L₁) :

⇑f x = ⇑g x

source

@[simp]

theorem lie_hom.mk_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₂] (f : L₁ →ₗ⁅R⁆ 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_hom.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_hom.coe_linear_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₁ →ₗ[R] 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₃} = {to_fun := ⇑f, map_add' := h₁, map_smul' := h₂}

source

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

theorem lie_hom.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

@[simp]

theorem lie_hom.coe_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₂) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem lie_hom.coe_linear_map_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₂) :

↑(f.comp g) = ↑f.comp ↑g

source

@[simp]

theorem lie_hom.comp_id {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.comp lie_hom.id = f

source

@[simp]

theorem lie_hom.id_comp {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₂) :

lie_hom.id.comp f = f

source

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

@[nolint]

def lie_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'] (self : L ≃ₗ⁅R⁆ L') :

L ≃ₗ[R] L'

source

@[nolint]

def lie_equiv.to_lie_hom {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'] (self : L ≃ₗ⁅R⁆ L') :

L →ₗ⁅R⁆ L'

source

structure lie_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

@[instance]

def lie_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_equiv.has_coe_to_lie_hom = {coe := lie_equiv.to_lie_hom _inst_6}

source

@[instance]

def lie_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_equiv.has_coe_to_linear_equiv = {coe := lie_equiv.to_linear_equiv _inst_6}

source

@[instance]

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

source

@[simp]

theorem lie_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_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_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_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_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_equiv.inhabited {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :

inhabited (L₁ ≃ₗ⁅R⁆ L₁)

Equations

lie_equiv.inhabited = {default := 1}

source

def lie_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_equiv.refl = 1

source

@[simp]

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

⇑lie_equiv.refl x = x

source

def lie_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_lie_hom.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_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_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_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_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_lie_hom.comp e₁.to_lie_hom).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_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_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

theorem lie_equiv.bijective {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₂) :

function.bijective ⇑↑e

source

theorem lie_equiv.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₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

function.injective ⇑↑e

source

theorem lie_equiv.surjective {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₂) :

function.surjective ⇑↑e

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] (self : 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_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_smul {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) (c : R) (x : M) :

⇑f (c • x) = c • ⇑f x

source

@[simp]

theorem lie_module_hom.map_add {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 y : M) :

⇑f (x + y) = ⇑f x + ⇑f y

source

@[simp]

theorem lie_module_hom.map_sub {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 y : M) :

⇑f (x - y) = ⇑f x - ⇑f y

source

@[simp]

theorem lie_module_hom.map_neg {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 : M) :

⇑f (-x) = -⇑f x

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

theorem lie_module_hom.map_lie₂ {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 : M →ₗ⁅R,L⁆ N →ₗ[R] P) (x : L) (m : M) (n : N) :

⁅x,⇑(⇑f m) n⁆ = ⇑(⇑f ⁅x,m⁆) n + ⇑(⇑f m) ⁅x,n⁆

source

@[simp]

theorem lie_module_hom.map_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] (f : M →ₗ⁅R,L⁆ N) :

⇑f 0 = 0

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

@[simp]

theorem lie_module_hom.coe_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] :

⇑0 = 0

source

theorem lie_module_hom.zero_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] (m : M) :

⇑0 m = 0

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 coe_fn

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

@[simp]

theorem lie_module_hom.mk_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] (f : M →ₗ⁅R,L⁆ 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_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_linear_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 →ₗ[R] 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₃} = {to_fun := ⇑f, map_add' := h₁, map_smul' := h₂}

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

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

@[simp]

theorem lie_module_hom.coe_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) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem lie_module_hom.coe_linear_map_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) :

↑(f.comp 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

@[instance]

def lie_module_hom.has_add {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_add (M →ₗ⁅R,L⁆ N)

Equations

lie_module_hom.has_add = {add := λ (f g : M →ₗ⁅R,L⁆ N), {to_fun := (↑f + ↑g).to_fun, map_add' := _, map_smul' := _, map_lie' := _}}

source

@[instance]

def lie_module_hom.has_sub {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_sub (M →ₗ⁅R,L⁆ N)

Equations

lie_module_hom.has_sub = {sub := λ (f g : M →ₗ⁅R,L⁆ N), {to_fun := (↑f - ↑g).to_fun, map_add' := _, map_smul' := _, map_lie' := _}}

source

@[instance]

def lie_module_hom.has_neg {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_neg (M →ₗ⁅R,L⁆ N)

Equations

lie_module_hom.has_neg = {neg := λ (f : M →ₗ⁅R,L⁆ N), {to_fun := (-↑f).to_fun, map_add' := _, map_smul' := _, map_lie' := _}}

source

@[simp]

theorem lie_module_hom.coe_add {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) = ⇑f + ⇑g

source

theorem lie_module_hom.add_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] (f g : M →ₗ⁅R,L⁆ N) (m : M) :

⇑(f + g) m = ⇑f m + ⇑g m

source

@[simp]

theorem lie_module_hom.coe_sub {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) = ⇑f - ⇑g

source

theorem lie_module_hom.sub_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] (f g : M →ₗ⁅R,L⁆ N) (m : M) :

⇑(f - g) m = ⇑f m - ⇑g m

source

@[simp]

theorem lie_module_hom.coe_neg {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

theorem lie_module_hom.neg_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] (f : M →ₗ⁅R,L⁆ N) (m : M) :

(⇑-f) m = -⇑f m

source

@[instance]

def lie_module_hom.add_comm_group {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] :

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

Equations

lie_module_hom.add_comm_group = {add := has_add.add lie_module_hom.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (f : M →ₗ⁅R,L⁆ N), {to_fun := (n • ↑f).to_fun, map_add' := _, map_smul' := _, map_lie' := _}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg lie_module_hom.has_neg, sub := has_sub.sub lie_module_hom.has_sub, sub_eq_add_neg := _, gsmul := add_comm_group.gsmul (function.injective.add_comm_group coe_fn lie_module_hom.coe_injective lie_module_hom.coe_zero lie_module_hom.coe_add lie_module_hom.coe_neg lie_module_hom.coe_sub), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _}

source

@[instance]

def lie_module_hom.has_scalar {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_scalar R (M →ₗ⁅R,L⁆ N)

Equations

lie_module_hom.has_scalar = {smul := λ (t : R) (f : M →ₗ⁅R,L⁆ N), {to_fun := (t • ↑f).to_fun, map_add' := _, map_smul' := _, map_lie' := _}}

source

@[simp]

theorem lie_module_hom.coe_smul {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] (t : R) (f : M →ₗ⁅R,L⁆ N) :

⇑(t • f) = t • ⇑f

source

theorem lie_module_hom.smul_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] (t : R) (f : M →ₗ⁅R,L⁆ N) (m : M) :

⇑(t • f) m = t • ⇑f m

source

@[instance]

def lie_module_hom.module {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] :

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

Equations

lie_module_hom.module = function.injective.module R {to_fun := lie_module_hom.to_fun _inst_14, map_zero' := _, map_add' := _} lie_module_hom.coe_injective lie_module_hom.coe_smul

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] (self : 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] (self : M ≃ₗ⁅R,L⁆ N) :

M →ₗ⁅R,L⁆ N

source

@[nolint]

def lie_module_equiv.to_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] (self : M ≃ₗ⁅R,L⁆ N) :

M ≃ N

source

@[instance]

def lie_module_equiv.has_coe_to_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 ≃ N)

Equations

lie_module_equiv.has_coe_to_equiv = {coe := lie_module_equiv.to_equiv _inst_14}

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_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) (F : N → M) (h₃ : function.left_inverse F f) (h₄ : function.right_inverse F f) (h₅ : ∀ {x : L} {m : M}, f ⁅x,m⁆ = ⁅x,f m⁆) :

⇑{to_fun := f, map_add' := h₁, map_smul' := h₂, inv_fun := F, left_inv := h₃, right_inv := h₄, map_lie' := h₅} = f

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

theorem lie_module_equiv.to_equiv_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 lie_module_equiv.to_equiv

source

@[ext]

theorem lie_module_equiv.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] (e₁ e₂ : M ≃ₗ⁅R,L⁆ N) (h : ∀ (m : M), ⇑e₁ m = ⇑e₂ m) :

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)

mathlib documentation

Lie algebras #

Main definitions #

Notation #

Implementation notes #

References #

Tags #