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

source

class LieModule.IsTrivial (L : Type v) (M : Type w) [Bracket L M] [Zero M] :

Prop

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

trivial : ∀ (x : L) (m : M), ⁅x, m⁆ = 0

Instances

source

@[simp]

theorem trivial_lie_zero (L : Type v) (M : Type w) [Bracket L M] [Zero M] [LieModule.IsTrivial L M] (x : L) (m : M) :

⁅x, m⁆ = 0

source

instance LieModule.instIsTrivialOfSubsingleton {L : Type u_1} {M : Type u_2} [LieRing L] [AddCommGroup M] [LieRingModule L M] [Subsingleton L] :

LieModule.IsTrivial L M

Equations

⋯ = ⋯

source

instance LieModule.instIsTrivialOfSubsingleton' {L : Type u_1} {M : Type u_2} [LieRing L] [AddCommGroup M] [LieRingModule L M] [Subsingleton M] :

LieModule.IsTrivial L M

Equations

⋯ = ⋯

source

@[reducible, inline]

abbrev IsLieAbelian (L : Type v) [Bracket L L] [Zero L] :

Prop

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

Equations

IsLieAbelian L = LieModule.IsTrivial L L

Instances For

source

instance LieIdeal.isLieAbelian_of_trivial (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [h : LieModule.IsTrivial L ↥I] :

IsLieAbelian ↥I

Equations

⋯ = ⋯

source

theorem Function.Injective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂} (h₁ : Function.Injective ⇑f) :

IsLieAbelian L₂ → IsLieAbelian L₁

source

theorem Function.Surjective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂} (h₁ : Function.Surjective ⇑f) (h₂ : IsLieAbelian L₁) :

IsLieAbelian L₂

source

theorem lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

IsLieAbelian L₁ ↔ IsLieAbelian L₂

source

theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] :

(Std.Commutative fun (x1 x2 : A) => x1 * x2) ↔ IsLieAbelian A

source

def LieModule.ker (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LieIdeal R L

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

Equations

LieModule.ker R L M = (LieModule.toEnd R L M).ker

Instances For

source

@[simp]

theorem LieModule.mem_ker (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) :

x ∈ LieModule.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0

source

def LieModule.maxTrivSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LieSubmodule R L M

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

Equations

LieModule.maxTrivSubmodule R L M = { carrier := {m : M | ∀ (x : L), ⁅x, m⁆ = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }

Instances For

source

@[simp]

theorem LieModule.mem_maxTrivSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (m : M) :

m ∈ LieModule.maxTrivSubmodule R L M ↔ ∀ (x : L), ⁅x, m⁆ = 0

source

instance LieModule.instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LieModule.IsTrivial L ↥(LieModule.maxTrivSubmodule R L M)

Equations

⋯ = ⋯

source

@[simp]

theorem LieModule.ideal_oper_maxTrivSubmodule_eq_bot (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) :

⁅I, LieModule.maxTrivSubmodule R L M⁆ = ⊥

source

theorem LieModule.le_max_triv_iff_bracket_eq_bot (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L M} :

N ≤ LieModule.maxTrivSubmodule R L M ↔ ⁅⊤, N⁆ = ⊥

source

theorem LieModule.trivial_iff_le_maximal_trivial (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :

LieModule.IsTrivial L ↥N ↔ N ≤ LieModule.maxTrivSubmodule R L M

source

theorem LieModule.isTrivial_iff_max_triv_eq_top (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LieModule.IsTrivial L M ↔ LieModule.maxTrivSubmodule R L M = ⊤

source

def LieModule.maxTrivHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) :

↥(LieModule.maxTrivSubmodule R L M) →ₗ⁅R,L⁆ ↥(LieModule.maxTrivSubmodule R L N)

maxTrivSubmodule is functorial.

Equations

LieModule.maxTrivHom f = { toFun := fun (m : ↥(LieModule.maxTrivSubmodule R L M)) => ⟨f ↑m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieModule.coe_maxTrivHom_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (m : ↥(LieModule.maxTrivSubmodule R L M)) :

↑((LieModule.maxTrivHom f) m) = f ↑m

source

def LieModule.maxTrivEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L⁆ N) :

↥(LieModule.maxTrivSubmodule R L M) ≃ₗ⁅R,L⁆ ↥(LieModule.maxTrivSubmodule R L N)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem LieModule.coe_maxTrivEquiv_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L⁆ N) (m : ↥(LieModule.maxTrivSubmodule R L M)) :

↑((LieModule.maxTrivEquiv e) m) = e ↑m

source

@[simp]

theorem LieModule.maxTrivEquiv_of_refl_eq_refl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LieModule.maxTrivEquiv LieModuleEquiv.refl = LieModuleEquiv.refl

source

@[simp]

theorem LieModule.maxTrivEquiv_of_equiv_symm_eq_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L⁆ N) :

(LieModule.maxTrivEquiv e).symm = LieModule.maxTrivEquiv e.symm

source

def LieModule.maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] :

↥(LieModule.maxTrivSubmodule R L (M →ₗ[R] N)) ≃ₗ[R] M →ₗ⁅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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem LieModule.coe_maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : ↥(LieModule.maxTrivSubmodule R L (M →ₗ[R] N))) :

⇑(LieModule.maxTrivLinearMapEquivLieModuleHom f) = ⇑↑f

source

@[simp]

theorem LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) :

⇑↑(LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = ⇑f

source

@[simp]

theorem LieModule.coe_linearMap_maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : ↥(LieModule.maxTrivSubmodule R L (M →ₗ[R] N))) :

↑(LieModule.maxTrivLinearMapEquivLieModuleHom f) = ↑f

source

@[simp]

theorem LieModule.coe_linearMap_maxTrivLinearMapEquivLieModuleHom_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) :

↑(LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = ↑f

source

@[reducible, inline]

abbrev LieAlgebra.center (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

LieIdeal 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.

Equations

LieAlgebra.center R L = LieModule.maxTrivSubmodule R L L

Instances For

source

instance LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

IsLieAbelian ↥(LieAlgebra.center R L)

Equations

⋯ = ⋯

source

@[simp]

theorem LieAlgebra.ad_ker_eq_self_module_ker (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

(LieAlgebra.ad R L).ker = LieModule.ker R L L

source

@[simp]

theorem LieAlgebra.self_module_ker_eq_center (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

LieModule.ker R L L = LieAlgebra.center R L

source

theorem LieAlgebra.abelian_of_le_center (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (h : I ≤ LieAlgebra.center R L) :

IsLieAbelian ↥I

source

theorem LieAlgebra.isLieAbelian_iff_center_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

IsLieAbelian L ↔ LieAlgebra.center R L = ⊤

source

theorem LieModule.commute_toEnd_of_mem_center_left {R : Type u} {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} (hx : x ∈ LieAlgebra.center R L) (y : L) :

Commute ((LieModule.toEnd R L M) x) ((LieModule.toEnd R L M) y)

source

theorem LieModule.commute_toEnd_of_mem_center_right {R : Type u} {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} (hx : x ∈ LieAlgebra.center R L) (y : L) :

Commute ((LieModule.toEnd R L M) y) ((LieModule.toEnd R L M) x)

source

@[simp]

theorem LieSubmodule.trivial_lie_oper_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (I : LieIdeal R L) [LieModule.IsTrivial L M] :

⁅I, N⁆ = ⊥

source

theorem LieSubmodule.lie_abelian_iff_lie_self_eq_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

IsLieAbelian ↥I ↔ ⁅I, I⁆ = ⊥

source

theorem lie_eq_self_of_isAtom_of_ne_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {I : LieIdeal R L} (hN : IsAtom N) (h : ⁅I, N⁆ ≠ ⊥) :

⁅I, N⁆ = N

source

theorem lie_eq_self_of_isAtom_of_nonabelian {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (hI : IsAtom I) (h : ¬IsLieAbelian ↥I) :

⁅I, I⁆ = I

HepLean Documentation

Mathlib.Algebra.Lie.Abelian

Trivial Lie modules and Abelian Lie algebras #

Main definitions #

Tags #