mathlib documentation

algebra.lie.basic

Lie algebras #

This file defines Lie rings and Lie algebras over a commutative ring together with their modules, morphisms and equivalences, as well as various lemmas to make these definitions usable.

Main definitions #

Notation #

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

Implementation notes #

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

References #

Tags #

lie bracket, jacobi identity, lie ring, lie algebra, lie module

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

A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity.

Instances of this typeclass
Instances of other typeclasses for lie_ring
  • lie_ring.has_sizeof_inst
@[class]
structure lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] :
Type (max u v)

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

Instances of this typeclass
Instances of other typeclasses for lie_algebra
  • lie_algebra.has_sizeof_inst
@[class]
structure lie_ring_module (L : Type v) (M : Type w) [lie_ring L] [add_comm_group M] :
Type (max v w)

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

Instances of this typeclass
Instances of other typeclasses for lie_ring_module
  • lie_ring_module.has_sizeof_inst
@[class]
structure lie_module (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] :
Type

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

Instances of this typeclass
Instances of other typeclasses for lie_module
  • lie_module.has_sizeof_inst
@[simp]
theorem add_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x y : L) (m : M) :
@[simp]
theorem lie_add {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m n : M) :
@[simp]
theorem smul_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (t : R) (x : L) (m : M) :
@[simp]
theorem lie_smul {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (t : R) (x : L) (m : M) :
theorem leibniz_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x y : L) (m : M) :
@[simp]
theorem lie_zero {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) :
@[simp]
theorem zero_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (m : M) :
@[simp]
theorem lie_self {L : Type v} [lie_ring L] (x : L) :
@[simp]
theorem lie_skew {L : Type v} [lie_ring L] (x y : L) :
@[protected, instance]
def lie_algebra_self_module {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :

Every Lie algebra is a module over itself.

Equations
@[simp]
theorem neg_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) :
@[simp]
theorem lie_neg {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) :
@[simp]
theorem 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) :
@[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) :
@[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 : ) :
@[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 : ) :
@[simp]
theorem zsmul_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) (a : ) :
@[simp]
theorem lie_zsmul {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x : L) (m : M) (a : ) :
@[simp]
theorem lie_lie {L : Type v} {M : Type w} [lie_ring L] [add_comm_group M] [lie_ring_module L M] (x y : L) (m : M) :
theorem lie_jacobi {L : Type v} [lie_ring L] (x y z : L) :
@[protected, 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] :
Equations
@[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) :
@[protected, 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
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)

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

Instances for lie_hom
@[protected, instance]
def lie_hom.linear_map.has_coe {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₂] :
has_coe (L₁ →ₗ⁅R L₂) (L₁ →ₗ[R] L₂)
Equations
@[protected, instance]
def lie_hom.has_coe_to_fun {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₂] :
has_coe_to_fun (L₁ →ₗ⁅R L₂) (λ (_x : L₁ →ₗ⁅R L₂), L₁ → L₂)

see Note [function coercion]

Equations
def lie_hom.simps.apply {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₂] (h : L₁ →ₗ⁅R L₂) :
L₁ → L₂

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
@[simp, norm_cast]
theorem lie_hom.coe_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₂] (f : L₁ →ₗ⁅R L₂) :
@[simp]
theorem lie_hom.to_fun_eq_coe {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₂] (f : L₁ →ₗ⁅R L₂) :
@[simp]
theorem lie_hom.map_smul {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₂] (f : L₁ →ₗ⁅R L₂) (c : R) (x : L₁) :
f (c x) = c f x
@[simp]
theorem lie_hom.map_add {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₂] (f : L₁ →ₗ⁅R L₂) (x y : L₁) :
f (x + y) = f x + f y
@[simp]
theorem lie_hom.map_sub {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₂] (f : L₁ →ₗ⁅R L₂) (x y : L₁) :
f (x - y) = f x - f y
@[simp]
theorem lie_hom.map_neg {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₂] (f : L₁ →ₗ⁅R L₂) (x : L₁) :
f (-x) = -f x
@[simp]
theorem lie_hom.map_lie {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₂] (f : L₁ →ₗ⁅R L₂) (x y : L₁) :
@[simp]
theorem lie_hom.map_zero {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₂] (f : L₁ →ₗ⁅R L₂) :
f 0 = 0
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
@[simp]
theorem lie_hom.coe_id {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :
theorem lie_hom.id_apply {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (x : L₁) :
@[protected, instance]
def lie_hom.has_zero {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₂] :
has_zero (L₁ →ₗ⁅R L₂)

The constant 0 map is a Lie algebra morphism.

Equations
@[simp, norm_cast]
theorem lie_hom.coe_zero {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₂] :
0 = 0
theorem lie_hom.zero_apply {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₂] (x : L₁) :
0 x = 0
@[protected, 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
@[simp]
theorem lie_hom.coe_one {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :
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
@[protected, instance]
def lie_hom.inhabited {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₂] :
inhabited (L₁ →ₗ⁅R L₂)
Equations
theorem lie_hom.coe_injective {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₂] :
@[ext]
theorem lie_hom.ext {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₂] {f g : L₁ →ₗ⁅R L₂} (h : ∀ (x : L₁), f x = g x) :
f = g
theorem lie_hom.ext_iff {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₂] {f g : L₁ →ₗ⁅R L₂} :
f = g ∀ (x : L₁), f x = g x
theorem lie_hom.congr_fun {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₂] {f g : L₁ →ₗ⁅R L₂} (h : f = g) (x : L₁) :
f x = g x
@[simp]
theorem lie_hom.mk_coe {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₂] (f : L₁ →ₗ⁅R L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y) (h₂ : ∀ (r : R) (x : L₁), f (r x) = (ring_hom.id R) r f x) (h₃ : ∀ {x y : L₁}, {to_fun := f, map_add' := h₁, map_smul' := h₂}.to_fun x,y = {to_fun := f, map_add' := h₁, map_smul' := h₂}.to_fun x,{to_fun := f, map_add' := h₁, map_smul' := h₂}.to_fun y) :
{to_linear_map := {to_fun := f, map_add' := h₁, map_smul' := h₂}, map_lie' := h₃} = f
@[simp]
theorem lie_hom.coe_mk {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₂] (f : L₁ → L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y) (h₂ : ∀ (r : R) (x : L₁), f (r x) = (ring_hom.id R) r f x) (h₃ : ∀ {x y : L₁}, {to_fun := f, map_add' := h₁, map_smul' := h₂}.to_fun x,y = {to_fun := f, map_add' := h₁, map_smul' := h₂}.to_fun x,{to_fun := f, map_add' := h₁, map_smul' := h₂}.to_fun y) :
{to_linear_map := {to_fun := f, map_add' := h₁, map_smul' := h₂}, map_lie' := h₃} = f
def lie_hom.comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] [lie_ring L₂] [lie_algebra R L₂] [lie_ring L₃] [lie_algebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) :
L₁ →ₗ⁅R L₃

The composition of morphisms is a morphism.

Equations
theorem lie_hom.comp_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] [lie_ring L₂] [lie_algebra R L₂] [lie_ring L₃] [lie_algebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) (x : L₁) :
(f.comp g) x = f (g x)
@[simp, norm_cast]
theorem lie_hom.coe_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] [lie_ring L₂] [lie_algebra R L₂] [lie_ring L₃] [lie_algebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) :
(f.comp g) = f g
@[simp, norm_cast]
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_algebra R L₁] [lie_ring L₂] [lie_algebra R L₂] [lie_ring L₃] [lie_algebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) :
(f.comp g) = f.comp g
@[simp]
theorem lie_hom.comp_id {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₂] (f : L₁ →ₗ⁅R L₂) :
@[simp]
theorem lie_hom.id_comp {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₂] (f : L₁ →ₗ⁅R L₂) :
def lie_hom.inverse {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₂] (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
@[reducible]
def lie_ring_module.comp_lie_hom {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] [lie_ring L₂] [lie_algebra R L₂] [add_comm_group M] [lie_ring_module L₂ M] (f : L₁ →ₗ⁅R L₂) :

A Lie ring module may be pulled back along a morphism of Lie algebras.

See note [reducible non-instances].

Equations
theorem lie_ring_module.comp_lie_hom_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] [lie_ring L₂] [lie_algebra R L₂] [add_comm_group M] [lie_ring_module L₂ M] (f : L₁ →ₗ⁅R L₂) (x : L₁) (m : M) :
@[reducible]
def lie_module.comp_lie_hom {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] [lie_ring L₂] [lie_algebra R L₂] [add_comm_group M] [lie_ring_module L₂ M] (f : L₁ →ₗ⁅R L₂) [module R M] [lie_module R L₂ M] :
lie_module R L₁ M

A Lie module may be pulled back along a morphism of Lie algebras.

See note [reducible non-instances].

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

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.

Instances for lie_equiv
def lie_equiv.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₂] (f : L₁ ≃ₗ⁅R L₂) :
L₁ ≃ₗ[R] L₂

Consider an equivalence of Lie algebras as a linear equivalence.

Equations
@[protected, 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
@[protected, 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
@[protected, 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₂) (λ (_x : L₁ ≃ₗ⁅R L₂), L₁ → L₂)

see Note [function coercion]

Equations
@[simp, norm_cast]
theorem lie_equiv.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₂] (e : L₁ ≃ₗ⁅R L₂) :
@[simp, norm_cast]
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₂) :
@[simp]
theorem lie_equiv.to_linear_equiv_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₂) (g : L₂ → L₁) (h₁ : function.left_inverse g f.to_linear_map.to_fun) (h₂ : function.right_inverse g f.to_linear_map.to_fun) :
{to_lie_hom := f, inv_fun := g, left_inv := h₁, right_inv := h₂} = {to_fun := f.to_linear_map.to_fun, map_add' := _, map_smul' := _, inv_fun := g, left_inv := h₁, right_inv := h₂}
theorem lie_equiv.coe_linear_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₂] :
theorem lie_equiv.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₂] :
@[ext]
theorem lie_equiv.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
@[protected, 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
@[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
@[protected, 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
@[refl]
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
@[simp]
theorem lie_equiv.refl_apply {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (x : L₁) :
@[symm]
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
@[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
@[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
@[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
@[simp]
theorem lie_equiv.refl_symm {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] :
@[trans]
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
@[simp]
theorem lie_equiv.self_trans_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₂) :
@[simp]
theorem lie_equiv.symm_trans_self {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (e : L₁ ≃ₗ⁅R L₂) :
@[simp]
theorem lie_equiv.trans_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] (e₁ : L₁ ≃ₗ⁅R L₂) (e₂ : L₂ ≃ₗ⁅R L₃) (x : L₁) :
(e₁.trans e₂) x = e₂ (e₁ x)
@[simp]
theorem lie_equiv.symm_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₃) :
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
@[protected]
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₂) :
@[protected]
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₂) :
@[protected]
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₂) :
noncomputable def lie_equiv.of_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₂] (f : L₁ →ₗ⁅R L₂) (h₁ : function.injective f) (h₂ : function.surjective f) :
L₁ ≃ₗ⁅R L₂

A bijective morphism of Lie algebras yields an equivalence of Lie algebras.

Equations
@[simp]
theorem lie_equiv.of_bijective_to_lie_hom_to_linear_map_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) (h₂ : function.surjective f) (ᾰ : L₁) :
@[simp]
theorem lie_equiv.of_bijective_inv_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 : L₁ →ₗ⁅R L₂) (h₁ : function.injective f) (h₂ : function.surjective f) (ᾰ : L₂) :
@[simp]
theorem lie_equiv.of_bijective_to_lie_hom_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) (h₂ : function.surjective f) (ᾰ : L₁) :
((lie_equiv.of_bijective f h₁ h₂).to_lie_hom) = f ᾰ
structure lie_module_hom (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Type (max w w₁)

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

Instances for lie_module_hom
@[protected, instance]
def lie_module_hom.linear_map.has_coe {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Equations
@[protected, 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) (λ (_x : M →ₗ⁅R,L N), M → N)

see Note [function coercion]

Equations
@[simp, norm_cast]
theorem lie_module_hom.coe_to_linear_map {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (f : M →ₗ⁅R,L N) :
@[simp]
theorem lie_module_hom.map_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
@[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
@[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
@[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
@[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) :
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
@[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
def lie_module_hom.id {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :

The identity map is a morphism of Lie modules.

Equations
@[simp]
theorem lie_module_hom.coe_id {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] :
theorem lie_module_hom.id_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] (x : M) :
@[protected, instance]
def lie_module_hom.has_zero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :

The constant 0 map is a Lie module morphism.

Equations
@[simp, norm_cast]
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
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
@[protected, instance]
def lie_module_hom.has_one {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :

The identity map is a Lie module morphism.

Equations
@[protected, instance]
def lie_module_hom.inhabited {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Equations
theorem lie_module_hom.coe_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
@[ext]
theorem lie_module_hom.ext {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] {f g : M →ₗ⁅R,L N} (h : ∀ (m : M), f m = g m) :
f = g
theorem lie_module_hom.ext_iff {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] {f g : M →ₗ⁅R,L N} :
f = g ∀ (m : M), f m = g m
theorem lie_module_hom.congr_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] {f g : M →ₗ⁅R,L N} (h : f = g) (x : M) :
f x = g x
@[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 : L} {m : M}, f.to_fun x,m = x,f.to_fun m) :
@[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 →ₗ[R] N) (h : ∀ {x : L} {m : M}, f.to_fun x,m = x,f.to_fun m) :
@[simp, norm_cast]
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 : L} {m : M}, f.to_fun x,m = x,f.to_fun m) :
def lie_module_hom.comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (f : N →ₗ⁅R,L P) (g : M →ₗ⁅R,L N) :

The composition of Lie module morphisms is a morphism.

Equations
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)
@[simp, norm_cast]
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
@[simp, norm_cast]
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
def lie_module_hom.inverse {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (f : M →ₗ⁅R,L N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :

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

Equations
@[protected, 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] :
Equations
@[protected, 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] :
Equations
@[protected, 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] :
Equations
@[simp, norm_cast]
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
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
@[simp, norm_cast]
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
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
@[simp, norm_cast]
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) :
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
@[protected, instance]
def lie_module_hom.has_nsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Equations
@[simp, norm_cast]
theorem lie_module_hom.coe_nsmul {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] (n : ) (f : M →ₗ⁅R,L N) :
(n f) = n f
theorem lie_module_hom.nsmul_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] (n : ) (f : M →ₗ⁅R,L N) (m : M) :
(n f) m = n f m
@[protected, instance]
def lie_module_hom.has_zsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Equations
@[simp, norm_cast]
theorem lie_module_hom.coe_zsmul {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] (z : ) (f : M →ₗ⁅R,L N) :
(z f) = z f
theorem lie_module_hom.zsmul_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] (z : ) (f : M →ₗ⁅R,L N) (m : M) :
(z f) m = z f m
@[protected, 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] :
Equations
@[protected, instance]
def lie_module_hom.has_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] :
Equations
@[simp, norm_cast]
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
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
@[protected, 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] :
Equations
structure lie_module_equiv (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Type (max w w₁)

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

Instances for lie_module_equiv
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] (e : M ≃ₗ⁅R,L N) :

View an equivalence of Lie modules as a linear equivalence.

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

View an equivalence of Lie modules as a type level equivalence.

Equations
@[protected, 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
@[protected, instance]
def lie_module_equiv.has_coe_to_lie_module_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Equations
@[protected, instance]
def lie_module_equiv.has_coe_to_linear_equiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] :
Equations
@[protected, 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) (λ (_x : M ≃ₗ⁅R,L N), M → N)

see Note [function coercion]

Equations
theorem lie_module_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] (e : M ≃ₗ⁅R,L N) :
@[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 →ₗ⁅R,L N) (inv_fun : N → M) (h₁ : function.left_inverse inv_fun f.to_linear_map.to_fun) (h₂ : function.right_inverse inv_fun f.to_linear_map.to_fun) :
{to_lie_module_hom := f, inv_fun := inv_fun, left_inv := h₁, right_inv := h₂} = f
@[simp, norm_cast]
theorem lie_module_equiv.coe_to_lie_module_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) :
@[simp, norm_cast]
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) :
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] :
@[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₂
@[protected, instance]
def lie_module_equiv.has_one {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[simp]
theorem lie_module_equiv.one_apply {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (m : M) :
1 m = m
@[protected, instance]
def lie_module_equiv.inhabited {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[refl]
def lie_module_equiv.refl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :

Lie module equivalences are reflexive.

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

Lie module equivalences are syemmtric.

Equations
@[simp]
theorem lie_module_equiv.apply_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) (x : N) :
e ((e.symm) x) = x
@[simp]
theorem lie_module_equiv.symm_apply_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [lie_ring_module L M] [lie_ring_module L N] [lie_module R L M] [lie_module R L N] (e : M ≃ₗ⁅R,L N) (x : M) :
(e.symm) (e x) = x
@[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
@[trans]
def lie_module_equiv.trans {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (e₁ : M ≃ₗ⁅R,L N) (e₂ : N ≃ₗ⁅R,L P) :

Lie module equivalences are transitive.

Equations
@[simp]
theorem lie_module_equiv.trans_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P] [lie_module R L M] [lie_module R L N] [lie_module R L P] (e₁ : M ≃ₗ⁅R,L N) (e₂ : N ≃ₗ⁅R,L P) (m : M) :
(e₁.trans e₂) m = e₂ (e₁ m)
@[simp]
theorem lie_module_equiv.symm_trans {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) :
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
@[simp]
theorem lie_module_equiv.self_trans_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) :
@[simp]
theorem lie_module_equiv.symm_trans_self {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) :