mathlib documentation

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.

Main definitions #

Tags #

lie algebra, abelian, commutative, center

@[class]
structure lie_module.is_trivial (L : Type v) (M : Type w) [has_bracket L 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) [has_bracket L M] [has_zero M] [lie_module.is_trivial L M] (x : L) (m : M) :
def is_lie_abelian (L : Type v) [has_bracket L L] [has_zero L] :
Prop

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

@[instance]
def lie_ideal.is_lie_abelian_of_trivial (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) [h : lie_module.is_trivial L 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₂] [lie_algebra R L₁] [lie_algebra R 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₂] [lie_algebra R L₁] [lie_algebra R 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₂] [lie_algebra R L₁] [lie_algebra R L₂] (e : L₁ ≃ₗ⁅R L₂) :
theorem lie_algebra.is_lie_abelian_bot (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
def lie_module.ker (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 kernel of the action of a Lie algebra L on a Lie module M as a Lie ideal in L.

Equations
@[simp]
theorem lie_module.mem_ker (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 : L) :
x lie_module.ker R L M ∀ (m : M), x,m = 0
def lie_module.maximal_trivial_submodule (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :

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

Equations
@[simp]
theorem lie_module.mem_maximal_trivial_submodule (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (m : M) :
def lie_algebra.center (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R 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.

@[instance]
theorem lie_algebra.center_eq_adjoint_kernel (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
theorem lie_algebra.abelian_of_le_center (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) (h : I lie_algebra.center R L) :
@[simp]
theorem lie_submodule.trivial_lie_oper_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I : lie_ideal R L) [lie_module.is_trivial L M] :