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

## Main definitions #

• FreeLieAlgebra
• FreeLieAlgebra.lift
• FreeLieAlgebra.of
• FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra

## 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 NonUnitalNonAssocSemiring, 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.: LieSubalgebra.lieSpan R (FreeAlgebra R X) (Set.range (FreeAlgebra.ι 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 FreeLieAlgebra.Rel (R : Type u) (X : Type v) [] :

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

Instances For
theorem FreeLieAlgebra.Rel.addLeft {R : Type u} {X : Type v} [] (a : ) {b : } {c : } (h : ) :
FreeLieAlgebra.Rel R X (a + b) (a + c)
theorem FreeLieAlgebra.Rel.neg {R : Type u} {X : Type v} [] {a : } {b : } (h : ) :
theorem FreeLieAlgebra.Rel.subLeft {R : Type u} {X : Type v} [] (a : ) {b : } {c : } (h : ) :
FreeLieAlgebra.Rel R X (a - b) (a - c)
theorem FreeLieAlgebra.Rel.subRight {R : Type u} {X : Type v} [] {a : } {b : } (c : ) (h : ) :
FreeLieAlgebra.Rel R X (a - c) (b - c)
theorem FreeLieAlgebra.Rel.smulOfTower {R : Type u} {X : Type v} [] {S : Type u_1} [] [] [] (t : S) (a : ) (b : ) (h : ) :
FreeLieAlgebra.Rel R X (t a) (t b)
def FreeLieAlgebra (R : Type u) (X : Type v) [] :
Type (max u v)

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

Equations
Instances For
instance instInhabitedFreeLieAlgebra (R : Type u) (X : Type v) [] :
Equations
instance FreeLieAlgebra.instSMulFreeLieAlgebra (R : Type u) (X : Type v) [] {S : Type u_1} [] [] [] :
SMul S ()
Equations
• = { smul := fun (t : S) => Quot.map (fun (x : ) => t x) }
Equations
• =
instance FreeLieAlgebra.instZeroFreeLieAlgebra (R : Type u) (X : Type v) [] :
Zero ()
Equations
instance FreeLieAlgebra.instAddFreeLieAlgebra (R : Type u) (X : Type v) [] :
Equations
instance FreeLieAlgebra.instNegFreeLieAlgebra (R : Type u) (X : Type v) [] :
Neg ()
Equations
instance FreeLieAlgebra.instSubFreeLieAlgebra (R : Type u) (X : Type v) [] :
Sub ()
Equations
Equations
Equations
• = let __src := inferInstance; let __src_1 := inferInstance;
Equations
• One or more equations did not get rendered due to their size.

Note that here we turn the Mul coming from the NonUnitalNonAssocSemiring structure on lib R X into a Bracket on FreeLieAlgebra.

Equations
def FreeLieAlgebra.of (R : Type u) {X : Type v} [] :
X

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

Equations
Instances For
def FreeLieAlgebra.liftAux (R : Type u) {X : Type v} [] {L : Type w} [] [] (f : X) :

An auxiliary definition used to construct the equivalence lift below.

Equations
Instances For
theorem FreeLieAlgebra.liftAux_map_smul (R : Type u) {X : Type v} [] {L : Type w} [] [] (f : XL) (t : R) (a : ) :
() (t a) = t () a
theorem FreeLieAlgebra.liftAux_map_add (R : Type u) {X : Type v} [] {L : Type w} [] [] (f : XL) (a : ) (b : ) :
() (a + b) = () a + () b
theorem FreeLieAlgebra.liftAux_map_mul (R : Type u) {X : Type v} [] {L : Type w} [] [] (f : XL) (a : ) (b : ) :
() (a * b) = () a, () b
theorem FreeLieAlgebra.liftAux_spec (R : Type u) {X : Type v} [] {L : Type w} [] [] (f : XL) (a : ) (b : ) (h : ) :
() a = () b
def FreeLieAlgebra.mk (R : Type u) {X : Type v} [] :

The quotient map as a NonUnitalAlgHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def FreeLieAlgebra.lift (R : Type u) {X : Type v} [] {L : Type w} [] [] :
(XL) ( →ₗ⁅R L)

The functor X ↦ FreeLieAlgebra 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FreeLieAlgebra.lift_symm_apply (R : Type u) {X : Type v} [] {L : Type w} [] [] (F : →ₗ⁅R L) :
.symm F =
@[simp]
theorem FreeLieAlgebra.of_comp_lift {R : Type u} {X : Type v} [] {L : Type w} [] [] (f : XL) :
( f) = f
@[simp]
theorem FreeLieAlgebra.lift_unique {R : Type u} {X : Type v} [] {L : Type w} [] [] (f : XL) (g : →ₗ⁅R L) :
= f g = f
@[simp]
theorem FreeLieAlgebra.lift_of_apply {R : Type u} {X : Type v} [] {L : Type w} [] [] (f : XL) (x : X) :
( f) () = f x
@[simp]
theorem FreeLieAlgebra.lift_comp_of {R : Type u} {X : Type v} [] {L : Type w} [] [] (F : →ₗ⁅R L) :
() = F
theorem FreeLieAlgebra.hom_ext {R : Type u} {X : Type v} [] {L : Type w} [] [] {F₁ : →ₗ⁅R L} {F₂ : →ₗ⁅R L} (h : ∀ (x : X), F₁ () = F₂ ()) :
F₁ = F₂

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

Equations
• One or more equations did not get rendered due to their size.
Instances For