mathlib documentation

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.

Main definitions #

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] :

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] (a : free_non_unital_non_assoc_algebra R X) {b c : free_non_unital_non_assoc_algebra R X} (h : free_lie_algebra.rel R X b c) :
free_lie_algebra.rel R X (a + b) (a + c)
theorem free_lie_algebra.rel.neg {R : Type u} {X : Type v} [comm_ring R] {a b : free_non_unital_non_assoc_algebra R X} (h : free_lie_algebra.rel R X a b) :
theorem free_lie_algebra.rel.sub_left {R : Type u} {X : Type v} [comm_ring R] (a : free_non_unital_non_assoc_algebra R X) {b c : free_non_unital_non_assoc_algebra R X} (h : free_lie_algebra.rel R X b c) :
free_lie_algebra.rel R X (a - b) (a - c)
theorem free_lie_algebra.rel.sub_right {R : Type u} {X : Type v} [comm_ring R] {a b : free_non_unital_non_assoc_algebra R X} (c : free_non_unital_non_assoc_algebra R X) (h : free_lie_algebra.rel R X a b) :
free_lie_algebra.rel R X (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] [distrib_mul_action S R] [is_scalar_tower S R R] (t : S) (a b : free_non_unital_non_assoc_algebra R X) (h : free_lie_algebra.rel R X a b) :
free_lie_algebra.rel R X (t a) (t b)
@[protected, instance]
def free_lie_algebra.inhabited (R : Type u) (X : Type v) [comm_ring R] :
@[protected, instance]
noncomputable def free_lie_algebra.has_smul (R : Type u) (X : Type v) [comm_ring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] :
Equations
@[protected, instance]
@[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.module (R : Type u) (X : Type v) [comm_ring R] {S : Type u_1} [semiring S] [module S R] [is_scalar_tower S R R] :
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] :
Equations
@[irreducible]
noncomputable def free_lie_algebra.of (R : Type u) {X : Type v} [comm_ring R] :

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

Equations
noncomputable def free_lie_algebra.lift_aux (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (f : X → commutator_ring 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] [lie_algebra R L] (f : X → L) (t : R) (a : free_non_unital_non_assoc_algebra R X) :
theorem free_lie_algebra.lift_aux_map_add (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (f : X → L) (a b : free_non_unital_non_assoc_algebra R X) :
theorem free_lie_algebra.lift_aux_map_mul (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (f : X → L) (a b : free_non_unital_non_assoc_algebra R X) :
theorem free_lie_algebra.lift_aux_spec (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (f : X → L) (a b : free_non_unital_non_assoc_algebra R X) (h : free_lie_algebra.rel R X a b) :

The quotient map as a non_unital_alg_hom.

Equations
@[irreducible]
noncomputable def free_lie_algebra.lift (R : Type u) {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] :
(X → L) (free_lie_algebra R 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] [lie_algebra R L] (F : free_lie_algebra R X →ₗ⁅R L) :
@[simp]
theorem free_lie_algebra.of_comp_lift {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (f : X → L) :
@[simp]
theorem free_lie_algebra.lift_unique {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (f : X → L) (g : free_lie_algebra R X →ₗ⁅R L) :
@[simp]
theorem free_lie_algebra.lift_of_apply {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (f : X → L) (x : X) :
@[simp]
theorem free_lie_algebra.lift_comp_of {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (F : free_lie_algebra R X →ₗ⁅R L) :
@[ext]
theorem free_lie_algebra.hom_ext {R : Type u} {X : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] {F₁ F₂ : free_lie_algebra R X →ₗ⁅R L} (h : ∀ (x : X), F₁ (free_lie_algebra.of R x) = F₂ (free_lie_algebra.of R x)) :
F₁ = F₂