mathlibdocumentation

algebra.lie.abelian

Trivial Lie modules and Abelian Lie algebras #

The action of a Lie algebra L on a module M is trivial if ⁅x, m⁆ = 0 for all x ∈ L and m ∈ M. In the special case that M = L with the adjoint action, triviality corresponds to the concept of an Abelian Lie algebra.

In this file we define these concepts and provide some related definitions and results.

Tags #

lie algebra, abelian, commutative, center

@[class]
structure lie_module.is_trivial (L : Type v) (M : Type w) [ M] [has_zero M] :
Prop
• trivial : ∀ (x : L) (m : M), x,m = 0

A Lie (ring) module is trivial iff all brackets vanish.

Instances
@[simp]
theorem trivial_lie_zero (L : Type v) (M : Type w) [ M] [has_zero M] (x : L) (m : M) :
def is_lie_abelian (L : Type v) [ L] [has_zero L] :
Prop

A Lie algebra is Abelian iff it is trivial as a Lie module over itself.

@[protected, instance]
def lie_ideal.is_lie_abelian_of_trivial (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) [h : I] :
theorem function.injective.is_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [ L₁] [ L₂] {f : L₁ →ₗ⁅R L₂} (h₁ : function.injective f) (h₂ : is_lie_abelian L₂) :
theorem function.surjective.is_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [ L₁] [ L₂] {f : L₁ →ₗ⁅R L₂} (h₁ : function.surjective f) (h₂ : is_lie_abelian L₁) :
theorem lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [ L₁] [ L₂] (e : L₁ ≃ₗ⁅R L₂) :
theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [ring A] :
theorem lie_algebra.is_lie_abelian_bot (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
@[protected]
def lie_module.ker (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
L

The kernel of the action of a Lie algebra L on a Lie module M as a Lie ideal in L.

Equations
@[protected, simp]
theorem lie_module.mem_ker (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (x : L) :
x M ∀ (m : M), x,m = 0
def lie_module.max_triv_submodule (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
M

The largest submodule of a Lie module M on which the Lie algebra L acts trivially.

Equations
@[simp]
theorem lie_module.mem_max_triv_submodule (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (m : M) :
∀ (x : L), x,m = 0
@[protected, instance]
def lie_module.max_triv_submodule.is_trivial (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_module.ideal_oper_max_triv_submodule_eq_bot (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (I : L) :
theorem lie_module.le_max_triv_iff_bracket_eq_bot (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} :
theorem lie_module.trivial_iff_le_maximal_trivial (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
theorem lie_module.is_trivial_iff_max_triv_eq_top (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
def lie_module.max_triv_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : M →ₗ⁅R,L N) :

max_triv_submodule is functorial.

Equations
@[simp, norm_cast]
theorem lie_module.coe_max_triv_hom_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : M →ₗ⁅R,L N) (m : ) :
m) = f m
def lie_module.max_triv_equiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (e : M ≃ₗ⁅R,L N) :

The maximal trivial submodules of Lie-equivalent Lie modules are Lie-equivalent.

Equations
@[simp, norm_cast]
theorem lie_module.coe_max_triv_equiv_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (e : M ≃ₗ⁅R,L N) (m : ) :
m) = e m
@[simp]
theorem lie_module.max_triv_equiv_of_refl_eq_refl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_module.max_triv_equiv_of_equiv_symm_eq_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (e : M ≃ₗ⁅R,L N) :
def lie_module.max_triv_linear_map_equiv_lie_module_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] :

A linear map between two Lie modules is a morphism of Lie modules iff the Lie algebra action on it is trivial.

Equations
@[simp]
theorem lie_module.coe_max_triv_linear_map_equiv_lie_module_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : (M →ₗ[R] N))) :
@[simp]
theorem lie_module.coe_max_triv_linear_map_equiv_lie_module_hom_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : M →ₗ⁅R,L N) :
@[simp]
theorem lie_module.coe_linear_map_max_triv_linear_map_equiv_lie_module_hom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : (M →ₗ[R] N))) :
@[simp]
theorem lie_module.coe_linear_map_max_triv_linear_map_equiv_lie_module_hom_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : M →ₗ⁅R,L N) :
def lie_algebra.center (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
L

The center of a Lie algebra is the set of elements that commute with everything. It can be viewed as the maximal trivial submodule of the Lie algebra as a Lie module over itself via the adjoint representation.

@[protected, instance]
def lie_algebra.center.is_lie_abelian (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
@[simp]
theorem lie_algebra.ad_ker_eq_self_module_ker (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
L).ker = L
@[simp]
theorem lie_algebra.self_module_ker_eq_center (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
L =
theorem lie_algebra.abelian_of_le_center (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) (h : I ) :
theorem lie_algebra.is_lie_abelian_iff_center_eq_top (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
@[simp]
theorem lie_submodule.trivial_lie_oper_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I : L)  :
theorem lie_submodule.lie_abelian_iff_lie_self_eq_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) :