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) [CommRing R] : FreeNonUnitalNonAssocAlgebra R X → FreeNonUnitalNonAssocAlgebra R X → Prop

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

• lie_self: ∀ {R : Type u} {X : Type v} [inst : CommRing R] (a : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel R X (a * a) 0
• leibniz_lie: ∀ {R : Type u} {X : Type v} [inst : CommRing R] (a b c : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel R X (a * (b * c)) (a * b * c + b * (a * c))
• smul: ∀ {R : Type u} {X : Type v} [inst : CommRing R] (t : R) {a b : FreeNonUnitalNonAssocAlgebra R X}, FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (t • a) (t • b)
• add_right: ∀ {R : Type u} {X : Type v} [inst : CommRing R] {a b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (a + c) (b + c)
• mul_left: ∀ {R : Type u} {X : Type v} [inst : CommRing R] (a : FreeNonUnitalNonAssocAlgebra R X) {b c : FreeNonUnitalNonAssocAlgebra R X}, FreeLieAlgebra.Rel R X b c → FreeLieAlgebra.Rel R X (a * b) (a * c)
• mul_right: ∀ {R : Type u} {X : Type v} [inst : CommRing R] {a b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (a * c) (b * c)

theorem FreeLieAlgebra.Rel.addLeft {R : Type u} {X : Type v} [CommRing R] (a : FreeNonUnitalNonAssocAlgebra R X) {b : FreeNonUnitalNonAssocAlgebra R X} {c : FreeNonUnitalNonAssocAlgebra R X} (h : FreeLieAlgebra.Rel R X b c) : FreeLieAlgebra.Rel R X (a + b) (a + c)

theorem FreeLieAlgebra.Rel.neg {R : Type u} {X : Type v} [CommRing R] {a : FreeNonUnitalNonAssocAlgebra R X} {b : FreeNonUnitalNonAssocAlgebra R X} (h : FreeLieAlgebra.Rel R X a b) : FreeLieAlgebra.Rel R X (-a) (-b)

theorem FreeLieAlgebra.Rel.subLeft {R : Type u} {X : Type v} [CommRing R] (a : FreeNonUnitalNonAssocAlgebra R X) {b : FreeNonUnitalNonAssocAlgebra R X} {c : FreeNonUnitalNonAssocAlgebra R X} (h : FreeLieAlgebra.Rel R X b c) : FreeLieAlgebra.Rel R X (a - b) (a - c)

theorem FreeLieAlgebra.Rel.subRight {R : Type u} {X : Type v} [CommRing R] {a : FreeNonUnitalNonAssocAlgebra R X} {b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X) (h : FreeLieAlgebra.Rel R X a b) : FreeLieAlgebra.Rel R X (a - c) (b - c)

theorem FreeLieAlgebra.Rel.smulOfTower {R : Type u} {X : Type v} [CommRing R] {S : Type u_1} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (t : S) (a : FreeNonUnitalNonAssocAlgebra R X) (b : FreeNonUnitalNonAssocAlgebra R X) (h : FreeLieAlgebra.Rel R X a b) : FreeLieAlgebra.Rel R X (t • a) (t • b)

def FreeLieAlgebra (R : Type u) (X : Type v) [CommRing R] : Type (max u v)

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

Equations

• FreeLieAlgebra R X = Quot (FreeLieAlgebra.Rel R X)

instance instInhabitedFreeLieAlgebra (R : Type u) (X : Type v) [CommRing R] : Inhabited (FreeLieAlgebra R X)

Equations

• instInhabitedFreeLieAlgebra R X = ⋯.mpr inferInstance

instance FreeLieAlgebra.instSMulOfIsScalarTower (R : Type u) (X : Type v) [CommRing R] {S : Type u_1} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] : SMul S (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instSMulOfIsScalarTower R X = { smul := fun (t : S) => Quot.map (fun (x : FreeNonUnitalNonAssocAlgebra R X) => t • x) ⋯ }

instance FreeLieAlgebra.instIsCentralScalar (R : Type u) (X : Type v) [CommRing R] {S : Type u_1} [Monoid S] [DistribMulAction S R] [DistribMulAction Sᵐᵒᵖ R] [IsScalarTower S R R] [IsCentralScalar S R] : IsCentralScalar S (FreeLieAlgebra R X)

Equations

• ⋯ = ⋯

instance FreeLieAlgebra.instZero (R : Type u) (X : Type v) [CommRing R] : Zero (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instZero R X = { zero := Quot.mk (FreeLieAlgebra.Rel R X) 0 }

instance FreeLieAlgebra.instAdd (R : Type u) (X : Type v) [CommRing R] : Add (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instAdd R X = { add := Quot.map₂ (fun (x x_1 : FreeNonUnitalNonAssocAlgebra R X) => x + x_1) ⋯ ⋯ }

instance FreeLieAlgebra.instNeg (R : Type u) (X : Type v) [CommRing R] : Neg (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instNeg R X = { neg := Quot.map Neg.neg ⋯ }

instance FreeLieAlgebra.instSub (R : Type u) (X : Type v) [CommRing R] : Sub (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instSub R X = { sub := Quot.map₂ Sub.sub ⋯ ⋯ }

instance FreeLieAlgebra.instAddGroup (R : Type u) (X : Type v) [CommRing R] : AddGroup (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instAddGroup R X = Function.Surjective.addGroup (Quot.mk (FreeLieAlgebra.Rel R X)) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance FreeLieAlgebra.instAddCommSemigroup (R : Type u) (X : Type v) [CommRing R] : AddCommSemigroup (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instAddCommSemigroup R X = Function.Surjective.addCommSemigroup (Quot.mk (FreeLieAlgebra.Rel R X)) ⋯ ⋯

instance FreeLieAlgebra.instAddCommGroup (R : Type u) (X : Type v) [CommRing R] : AddCommGroup (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instAddCommGroup R X = let __src := inferInstance; let __src_1 := inferInstance; AddCommGroup.mk ⋯

instance FreeLieAlgebra.instModuleOfIsScalarTower (R : Type u) (X : Type v) [CommRing R] {S : Type u_1} [Semiring S] [Module S R] [IsScalarTower S R R] : Module S (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instModuleOfIsScalarTower R X = Function.Surjective.module S { toFun := Quot.mk (FreeLieAlgebra.Rel R X), map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance FreeLieAlgebra.instLieRing (R : Type u) (X : Type v) [CommRing R] : LieRing (FreeLieAlgebra R X)

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

Equations

• FreeLieAlgebra.instLieRing R X = LieRing.mk ⋯ ⋯ ⋯ ⋯

instance FreeLieAlgebra.instLieAlgebra (R : Type u) (X : Type v) [CommRing R] : LieAlgebra R (FreeLieAlgebra R X)

Equations

• FreeLieAlgebra.instLieAlgebra R X = LieAlgebra.mk ⋯

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

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

Equations

• FreeLieAlgebra.of R x = Quot.mk (FreeLieAlgebra.Rel R X) (FreeNonUnitalNonAssocAlgebra.of R x)

def FreeLieAlgebra.liftAux (R : Type u) {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : X → CommutatorRing L) : FreeNonUnitalNonAssocAlgebra R X →ₛₙₐ[MonoidHom.id R] CommutatorRing L

An auxiliary definition used to construct the equivalence lift below.

Equations

• FreeLieAlgebra.liftAux R f = (FreeNonUnitalNonAssocAlgebra.lift R) f

theorem FreeLieAlgebra.liftAux_map_smul (R : Type u) {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : X → L) (t : R) (a : FreeNonUnitalNonAssocAlgebra R X) : (FreeLieAlgebra.liftAux R f) (t • a) = t • (FreeLieAlgebra.liftAux R f) a

theorem FreeLieAlgebra.liftAux_map_add (R : Type u) {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : X → L) (a : FreeNonUnitalNonAssocAlgebra R X) (b : FreeNonUnitalNonAssocAlgebra R X) : (FreeLieAlgebra.liftAux R f) (a + b) = (FreeLieAlgebra.liftAux R f) a + (FreeLieAlgebra.liftAux R f) b

theorem FreeLieAlgebra.liftAux_map_mul (R : Type u) {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : X → L) (a : FreeNonUnitalNonAssocAlgebra R X) (b : FreeNonUnitalNonAssocAlgebra R X) : (FreeLieAlgebra.liftAux R f) (a * b) = ⁅(FreeLieAlgebra.liftAux R f) a, (FreeLieAlgebra.liftAux R f) b⁆

theorem FreeLieAlgebra.liftAux_spec (R : Type u) {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : X → L) (a : FreeNonUnitalNonAssocAlgebra R X) (b : FreeNonUnitalNonAssocAlgebra R X) (h : FreeLieAlgebra.Rel R X a b) : (FreeLieAlgebra.liftAux R f) a = (FreeLieAlgebra.liftAux R f) b

def FreeLieAlgebra.mk (R : Type u) {X : Type v} [CommRing R] : FreeNonUnitalNonAssocAlgebra R X →ₛₙₐ[MonoidHom.id R] CommutatorRing (FreeLieAlgebra R X)

The quotient map as a NonUnitalAlgHom.

Equations

• FreeLieAlgebra.mk R = { toFun := Quot.mk (FreeLieAlgebra.Rel R X), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

def FreeLieAlgebra.lift (R : Type u) {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] : (X → L) ≃ (FreeLieAlgebra R X →ₗ⁅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.

@[simp]

theorem FreeLieAlgebra.lift_symm_apply (R : Type u) {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (F : FreeLieAlgebra R X →ₗ⁅R⁆ L) : (FreeLieAlgebra.lift R).symm F = ⇑F ∘ FreeLieAlgebra.of R

@[simp]

theorem FreeLieAlgebra.of_comp_lift {R : Type u} {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : X → L) : ⇑((FreeLieAlgebra.lift R) f) ∘ FreeLieAlgebra.of R = f

@[simp]

theorem FreeLieAlgebra.lift_unique {R : Type u} {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : X → L) (g : FreeLieAlgebra R X →ₗ⁅R⁆ L) : ⇑g ∘ FreeLieAlgebra.of R = f ↔ g = (FreeLieAlgebra.lift R) f

@[simp]

theorem FreeLieAlgebra.lift_of_apply {R : Type u} {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : X → L) (x : X) : ((FreeLieAlgebra.lift R) f) (FreeLieAlgebra.of R x) = f x

@[simp]

theorem FreeLieAlgebra.lift_comp_of {R : Type u} {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (F : FreeLieAlgebra R X →ₗ⁅R⁆ L) : (FreeLieAlgebra.lift R) (⇑F ∘ FreeLieAlgebra.of R) = F

theorem FreeLieAlgebra.hom_ext {R : Type u} {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] {F₁ : FreeLieAlgebra R X →ₗ⁅R⁆ L} {F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L} (h : ∀ (x : X), F₁ (FreeLieAlgebra.of R x) = F₂ (FreeLieAlgebra.of R x)) : F₁ = F₂

@[simp]

theorem FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply (R : Type u) (X : Type v) [CommRing R] (a : FreeAlgebra R X) : (FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra R X).symm a = ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ FreeLieAlgebra.of R)) a

@[simp]

theorem FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply (R : Type u) (X : Type v) [CommRing R] (a : UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) : (FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra R X) a = ((UniversalEnvelopingAlgebra.lift R) ((FreeLieAlgebra.lift R) (FreeAlgebra.ι R))) a

def FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra (R : Type u) (X : Type v) [CommRing R] : UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) ≃ₐ[R] FreeAlgebra R X

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.