algebra.lie.free

Free Lie algebras #

Given a commutative ring R and a type X we construct the free Lie algebra on X with coefficients in R together with its universal property.

Implementation details #

Quotient of free non-unital, non-associative algebra #

We follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3 and construct the free Lie algebra as a quotient of the free non-unital, non-associative algebra. Since we do not currently have definitions of ideals, lattices of ideals, and quotients for non_unital_non_assoc_semiring, we construct our quotient using the low-level quot function on an inductively-defined relation.

Alternative construction (needs PBW) #

An alternative construction of the free Lie algebra on X is to start with the free unital associative algebra on X, regard it as a Lie algebra via the ring commutator, and take its smallest Lie subalgebra containing X. I.e.: lie_subalgebra.lie_span R (free_algebra R X) (set.range (free_algebra.ι R)).

However with this definition there does not seem to be an easy proof that the required universal property holds, and I don't know of a proof that avoids invoking the Poincaré–Birkhoff–Witt theorem. A related MathOverflow question is this one.

Tags #

lie algebra, free algebra, non-unital, non-associative, universal property, forgetful functor, adjoint functor

inductive free_lie_algebra.rel (R : Type u) (X : Type v) [comm_ring R] :
• lie_self : ∀ {R : Type u} {X : Type v} [_inst_1 : (a : , (a * a) 0
• leibniz_lie : ∀ {R : Type u} {X : Type v} [_inst_1 : (a b c : , (a * b * c) ((a * b) * c + b * a * c)
• smul : ∀ {R : Type u} {X : Type v} [_inst_1 : (t : R) {a b : , a b (t a) (t b)
• add_right : ∀ {R : Type u} {X : Type v} [_inst_1 : {a b : (c : , a b (a + c) (b + c)
• mul_left : ∀ {R : Type u} {X : Type v} [_inst_1 : (a : {b c : , b c (a * b) (a * c)
• mul_right : ∀ {R : Type u} {X : Type v} [_inst_1 : {a b : (c : , a b (a * c) (b * c)

The quotient of lib R X by the equivalence relation generated by this relation will give us the free Lie algebra.

theorem free_lie_algebra.rel.add_left {R : Type u} {X : Type v} [comm_ring R] {b c : X} (h : b c) :
(a + b) (a + c)
theorem free_lie_algebra.rel.neg {R : Type u} {X : Type v} [comm_ring R] {a b : X} (h : a b) :
(-a) (-b)
theorem free_lie_algebra.rel.sub_left {R : Type u} {X : Type v} [comm_ring R] {b c : X} (h : b c) :
(a - b) (a - c)
theorem free_lie_algebra.rel.sub_right {R : Type u} {X : Type v} [comm_ring R] {a b : X} (h : a b) :
(a - c) (b - c)
theorem free_lie_algebra.rel.smul_of_tower {R : Type u} {X : Type v} [comm_ring R] {S : Type u_1} [monoid S] [ R] [ R] (t : S) (a b : X) (h : a b) :
(t a) (t b)
def free_lie_algebra (R : Type u) (X : Type v) [comm_ring R] :
Type (max u v)

The free Lie algebra on the type X with coefficients in the commutative ring R.

Equations
• = quot X)
@[protected, instance]
def free_lie_algebra.inhabited (R : Type u) (X : Type v) [comm_ring R] :
@[protected, instance]
noncomputable def free_lie_algebra.has_scalar (R : Type u) (X : Type v) [comm_ring R] {S : Type u_1} [monoid S] [ R] [ R] :
X)
Equations
@[protected, instance]
def free_lie_algebra.is_central_scalar (R : Type u) (X : Type v) [comm_ring R] {S : Type u_1} [monoid S] [ R] [ R] [ R] :
@[protected, instance]
noncomputable def free_lie_algebra.has_zero (R : Type u) (X : Type v) [comm_ring R] :
Equations
@[protected, instance]
noncomputable def free_lie_algebra.has_add (R : Type u) (X : Type v) [comm_ring R] :
Equations
@[protected, instance]
noncomputable def free_lie_algebra.has_neg (R : Type u) (X : Type v) [comm_ring R] :
Equations
@[protected, instance]
noncomputable def free_lie_algebra.has_sub (R : Type u) (X : Type v) [comm_ring R] :
Equations
@[protected, instance]
noncomputable def free_lie_algebra.add_group (R : Type u) (X : Type v) [comm_ring R] :
Equations
@[protected, instance]
noncomputable def free_lie_algebra.add_comm_semigroup (R : Type u) (X : Type v) [comm_ring R] :
Equations
@[protected, instance]
noncomputable def free_lie_algebra.add_comm_group (R : Type u) (X : Type v) [comm_ring R] :
Equations
@[protected, instance]
noncomputable def free_lie_algebra.module (R : Type u) (X : Type v) [comm_ring R] {S : Type u_1} [semiring S] [ R] [ R] :
X)
Equations
@[protected, instance]
noncomputable def free_lie_algebra.lie_ring (R : Type u) (X : Type v) [comm_ring R] :

Note that here we turn the has_mul coming from the non_unital_non_assoc_semiring structure on lib R X into a has_bracket on free_lie_algebra.

Equations
@[protected, instance]
noncomputable def free_lie_algebra.lie_algebra (R : Type u) (X : Type v) [comm_ring R] :
X)
Equations
noncomputable def free_lie_algebra.of (R : Type u) {X : Type v} [comm_ring R] :
X →

The embedding of X into the free Lie algebra of X with coefficients in the commutative ring R.

Equations
• = λ (x : X), quot.mk X)
noncomputable def free_lie_algebra.lift_aux (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (f : X → L) :

An auxiliary definition used to construct the equivalence lift below.

Equations
theorem free_lie_algebra.lift_aux_map_smul (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (f : X → L) (t : R)  :
(t a) = t a
theorem free_lie_algebra.lift_aux_map_add (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (f : X → L) (a b : X) :
(a + b) = a + b
theorem free_lie_algebra.lift_aux_map_mul (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (f : X → L) (a b : X) :
(a * b) = a, b
theorem free_lie_algebra.lift_aux_spec (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (f : X → L) (a b : X) (h : a b) :
a = b
noncomputable def free_lie_algebra.mk (R : Type u) {X : Type v} [comm_ring R] :

The quotient map as a non_unital_alg_hom.

Equations
noncomputable def free_lie_algebra.lift (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] :
(X → L) X →ₗ⁅R L)

The functor X ↦ free_lie_algebra R X from the category of types to the category of Lie algebras over R is adjoint to the forgetful functor in the other direction.

Equations
@[simp]
theorem free_lie_algebra.lift_symm_apply (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (F : →ₗ⁅R L) :
.symm) F =
@[simp]
theorem free_lie_algebra.of_comp_lift {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (f : X → L) :
= f
@[simp]
theorem free_lie_algebra.lift_unique {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (f : X → L) (g : →ₗ⁅R L) :
= f g =
@[simp]
theorem free_lie_algebra.lift_of_apply {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (f : X → L) (x : X) :
f) x) = f x
@[simp]
theorem free_lie_algebra.lift_comp_of {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] (F : →ₗ⁅R L) :
= F
@[ext]
theorem free_lie_algebra.hom_ext {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [ L] {F₁ F₂ : →ₗ⁅R L} (h : ∀ (x : X), F₁ x) = F₂ x)) :
F₁ = F₂
@[simp]
theorem free_lie_algebra.universal_enveloping_equiv_free_algebra_apply (R : Type u) (X : Type v) [comm_ring R] (ᾰ : X)) :
@[simp]
theorem free_lie_algebra.universal_enveloping_equiv_free_algebra_symm_apply (R : Type u) (X : Type v) [comm_ring R] (ᾰ : X) :
noncomputable def free_lie_algebra.universal_enveloping_equiv_free_algebra (R : Type u) (X : Type v) [comm_ring R] :

The universal enveloping algebra of the free Lie algebra is just the free unital associative algebra.

Equations