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 of this typeclass
@[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) :
@[reducible]
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.

@[protected, 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] :
@[protected]
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
@[protected, 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.max_triv_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
Instances for lie_module.max_triv_submodule
@[simp]
theorem lie_module.mem_max_triv_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) :
m lie_module.max_triv_submodule R L M ∀ (x : L), x,m = 0
@[protected, instance]
@[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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (I : lie_ideal R 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] [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} :
def lie_module.max_triv_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] [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,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] [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,L N) (m : (lie_module.max_triv_submodule R L 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] [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] (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] [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] (e : M ≃ₗ⁅R,L N) (m : (lie_module.max_triv_submodule R 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] [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] (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] [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] :

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

Equations
@[reducible]
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.

@[protected, instance]
@[simp]
theorem lie_algebra.ad_ker_eq_self_module_ker (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
@[simp]
theorem lie_algebra.self_module_ker_eq_center (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] :