mathlib3 documentation

algebra.lie.free

Free Lie algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

free_non_unital_non_assoc_algebra R X → free_non_unital_non_assoc_algebra R X → Prop

lie_self : ∀ {R : Type u} {X : Type v} [_inst_1 : comm_ring R] (a : free_non_unital_non_assoc_algebra R X), free_lie_algebra.rel R X (a * a) 0
leibniz_lie : ∀ {R : Type u} {X : Type v} [_inst_1 : comm_ring R] (a b c : free_non_unital_non_assoc_algebra R X), free_lie_algebra.rel R X (a * (b * c)) (a * b * c + b * (a * c))
smul : ∀ {R : Type u} {X : Type v} [_inst_1 : comm_ring R] (t : R) {a b : free_non_unital_non_assoc_algebra R X}, free_lie_algebra.rel R X a b → free_lie_algebra.rel R X (t • a) (t • b)
add_right : ∀ {R : Type u} {X : Type v} [_inst_1 : comm_ring R] {a b : free_non_unital_non_assoc_algebra R X} (c : free_non_unital_non_assoc_algebra R X), free_lie_algebra.rel R X a b → free_lie_algebra.rel R X (a + c) (b + c)
mul_left : ∀ {R : Type u} {X : Type v} [_inst_1 : comm_ring R] (a : free_non_unital_non_assoc_algebra R X) {b c : free_non_unital_non_assoc_algebra R X}, free_lie_algebra.rel R X b c → free_lie_algebra.rel R X (a * b) (a * c)
mul_right : ∀ {R : Type u} {X : Type v} [_inst_1 : comm_ring R] {a b : free_non_unital_non_assoc_algebra R X} (c : free_non_unital_non_assoc_algebra R X), free_lie_algebra.rel R X a b → free_lie_algebra.rel R X (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] (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) :

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)

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

free_lie_algebra R X = quot (free_lie_algebra.rel R X)

Instances for free_lie_algebra

@[protected, instance]

def free_lie_algebra.inhabited (R : Type u) (X : Type v) [comm_ring R] :

inhabited (free_lie_algebra R X)

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

has_smul S (free_lie_algebra R X)

Equations

free_lie_algebra.has_smul R X = {smul := λ (t : S), quot.map (has_smul.smul t) _}

@[protected, instance]

def free_lie_algebra.is_central_scalar (R : Type u) (X : Type v) [comm_ring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] [distrib_mul_action Sᵐᵒᵖ R] [is_scalar_tower S R R] [is_central_scalar S R] :

is_central_scalar S (free_lie_algebra R X)

@[protected, instance]

noncomputable def free_lie_algebra.has_zero (R : Type u) (X : Type v) [comm_ring R] :

has_zero (free_lie_algebra R X)

Equations

free_lie_algebra.has_zero R X = {zero := quot.mk (free_lie_algebra.rel R X) 0}

@[protected, instance]

noncomputable def free_lie_algebra.has_add (R : Type u) (X : Type v) [comm_ring R] :

has_add (free_lie_algebra R X)

Equations

free_lie_algebra.has_add R X = {add := quot.map₂ has_add.add _ _}

@[protected, instance]

noncomputable def free_lie_algebra.has_neg (R : Type u) (X : Type v) [comm_ring R] :

has_neg (free_lie_algebra R X)

Equations

free_lie_algebra.has_neg R X = {neg := quot.map has_neg.neg _}

@[protected, instance]

noncomputable def free_lie_algebra.has_sub (R : Type u) (X : Type v) [comm_ring R] :

has_sub (free_lie_algebra R X)

Equations

free_lie_algebra.has_sub R X = {sub := quot.map₂ has_sub.sub _ _}

@[protected, instance]

noncomputable def free_lie_algebra.add_group (R : Type u) (X : Type v) [comm_ring R] :

add_group (free_lie_algebra R X)

Equations

free_lie_algebra.add_group R X = function.surjective.add_group (quot.mk (free_lie_algebra.rel R X)) _ _ _ _ _ _ _

@[protected, instance]

noncomputable def free_lie_algebra.add_comm_semigroup (R : Type u) (X : Type v) [comm_ring R] :

add_comm_semigroup (free_lie_algebra R X)

Equations

free_lie_algebra.add_comm_semigroup R X = function.surjective.add_comm_semigroup (quot.mk (free_lie_algebra.rel R X)) _ _

@[protected, instance]

noncomputable def free_lie_algebra.add_comm_group (R : Type u) (X : Type v) [comm_ring R] :

add_comm_group (free_lie_algebra R X)

Equations

free_lie_algebra.add_comm_group R X = {add := add_group.add (free_lie_algebra.add_group R X), add_assoc := _, zero := add_group.zero (free_lie_algebra.add_group R X), zero_add := _, add_zero := _, nsmul := add_group.nsmul (free_lie_algebra.add_group R X), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (free_lie_algebra.add_group R X), sub := add_group.sub (free_lie_algebra.add_group R X), sub_eq_add_neg := _, zsmul := add_group.zsmul (free_lie_algebra.add_group R X), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

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

module S (free_lie_algebra R X)

Equations

free_lie_algebra.module R X = function.surjective.module S {to_fun := quot.mk (free_lie_algebra.rel R X), map_zero' := _, map_add' := _} _ _

@[protected, instance]

noncomputable def free_lie_algebra.lie_ring (R : Type u) (X : Type v) [comm_ring R] :

lie_ring (free_lie_algebra R X)

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

free_lie_algebra.lie_ring R X = {to_add_comm_group := free_lie_algebra.add_comm_group R X _inst_1, to_has_bracket := {bracket := quot.map₂ has_mul.mul _ _}, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}

@[protected, instance]

noncomputable def free_lie_algebra.lie_algebra (R : Type u) (X : Type v) [comm_ring R] :

lie_algebra R (free_lie_algebra R X)

Equations

free_lie_algebra.lie_algebra R X = {to_module := free_lie_algebra.module R X _, lie_smul := _}

@[irreducible]

noncomputable def free_lie_algebra.of (R : Type u) {X : Type v} [comm_ring R] :

X → free_lie_algebra R X

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

Equations

free_lie_algebra.of R = λ (x : X), quot.mk (free_lie_algebra.rel R X) (free_non_unital_non_assoc_algebra.of R x)

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

free_non_unital_non_assoc_algebra R X →ₙₐ[R] commutator_ring L

An auxiliary definition used to construct the equivalence lift below.

Equations

free_lie_algebra.lift_aux R f = ⇑(free_non_unital_non_assoc_algebra.lift R) f

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

⇑(free_lie_algebra.lift_aux R f) (t • a) = t • ⇑(free_lie_algebra.lift_aux R f) a

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

⇑(free_lie_algebra.lift_aux R f) (a + b) = ⇑(free_lie_algebra.lift_aux R f) a + ⇑(free_lie_algebra.lift_aux R f) b

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

⇑(free_lie_algebra.lift_aux R f) (a * b) = ⁅⇑(free_lie_algebra.lift_aux R f) a, ⇑(free_lie_algebra.lift_aux R f) b⁆

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

⇑(free_lie_algebra.lift_aux R f) a = ⇑(free_lie_algebra.lift_aux R f) b

def free_lie_algebra.mk (R : Type u) {X : Type v} [comm_ring R] :

free_non_unital_non_assoc_algebra R X →ₙₐ[R] commutator_ring (free_lie_algebra R X)

The quotient map as a non_unital_alg_hom.

Equations

free_lie_algebra.mk R = {to_fun := quot.mk (free_lie_algebra.rel R X), map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _}

@[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

free_lie_algebra.lift R = {to_fun := λ (f : X → L), {to_linear_map := {to_fun := λ (c : free_lie_algebra R X), quot.lift_on c ⇑(free_lie_algebra.lift_aux R f) _, map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := λ (F : free_lie_algebra R X →ₗ⁅R⁆ L), ⇑F ∘ free_lie_algebra.of R, left_inv := _, right_inv := _}

@[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) :

⇑((free_lie_algebra.lift R).symm) F = ⇑F ∘ free_lie_algebra.of R

@[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) :

⇑(⇑(free_lie_algebra.lift R) f) ∘ free_lie_algebra.of R = f

@[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) :

⇑g ∘ free_lie_algebra.of R = f ↔ g = ⇑(free_lie_algebra.lift R) f

@[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) :

⇑(⇑(free_lie_algebra.lift R) f) (free_lie_algebra.of R 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] [lie_algebra R L] (F : free_lie_algebra R X →ₗ⁅R⁆ L) :

⇑(free_lie_algebra.lift R) (⇑F ∘ free_lie_algebra.of R) = F

@[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₂

@[simp]

theorem free_lie_algebra.universal_enveloping_equiv_free_algebra_apply (R : Type u) (X : Type v) [comm_ring R] (ᾰ : universal_enveloping_algebra R (free_lie_algebra R X)) :

⇑(free_lie_algebra.universal_enveloping_equiv_free_algebra R X) ᾰ = ⇑(⇑(universal_enveloping_algebra.lift R) (⇑(free_lie_algebra.lift R) (free_algebra.ι R))) ᾰ

@[simp]

theorem free_lie_algebra.universal_enveloping_equiv_free_algebra_symm_apply (R : Type u) (X : Type v) [comm_ring R] (ᾰ : free_algebra R X) :

⇑((free_lie_algebra.universal_enveloping_equiv_free_algebra R X).symm) ᾰ = ⇑(⇑(free_algebra.lift R) (⇑(universal_enveloping_algebra.ι R) ∘ free_lie_algebra.of R)) ᾰ

noncomputable def free_lie_algebra.universal_enveloping_equiv_free_algebra (R : Type u) (X : Type v) [comm_ring R] :

universal_enveloping_algebra R (free_lie_algebra R X) ≃ₐ[R] free_algebra R X

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

Equations

free_lie_algebra.universal_enveloping_equiv_free_algebra R X = alg_equiv.of_alg_hom (⇑(universal_enveloping_algebra.lift R) (⇑(free_lie_algebra.lift R) (free_algebra.ι R))) (⇑(free_algebra.lift R) (⇑(universal_enveloping_algebra.ι R) ∘ free_lie_algebra.of R)) _ _