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 #
FreeLieAlgebraFreeLieAlgebra.liftFreeLieAlgebra.ofFreeLieAlgebra.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
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)
Instances For
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)
The free Lie algebra on the type X with coefficients in the commutative ring R.
Equations
- FreeLieAlgebra R X = Quot (FreeLieAlgebra.Rel R X)
Instances For
instance
instInhabitedFreeLieAlgebra
(R : Type u)
(X : Type v)
[CommRing R]
:
Inhabited (FreeLieAlgebra R X)
Equations
- instInhabitedFreeLieAlgebra R X = Eq.mpr (_ : Inhabited (FreeLieAlgebra R X) = Inhabited (Quot (FreeLieAlgebra.Rel R X))) inferInstance
instance
FreeLieAlgebra.instSMulFreeLieAlgebra
(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
- One or more equations did not get rendered due to their size.
instance
FreeLieAlgebra.instIsCentralScalarFreeLieAlgebraInstSMulFreeLieAlgebraMulOppositeMonoidOp_leftToSMulToZeroToCommMonoidWithZeroToCommSemiringToSMulZeroClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddGroupWithOneToRingToDistribSMulToSMulToSemiringId
(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
- (_ : IsCentralScalar S (FreeLieAlgebra R X)) = (_ : IsCentralScalar S (FreeLieAlgebra R X))
instance
FreeLieAlgebra.instZeroFreeLieAlgebra
(R : Type u)
(X : Type v)
[CommRing R]
:
Zero (FreeLieAlgebra R X)
Equations
- FreeLieAlgebra.instZeroFreeLieAlgebra R X = { zero := Quot.mk (FreeLieAlgebra.Rel R X) 0 }
instance
FreeLieAlgebra.instAddFreeLieAlgebra
(R : Type u)
(X : Type v)
[CommRing R]
:
Add (FreeLieAlgebra R X)
Equations
- One or more equations did not get rendered due to their size.
instance
FreeLieAlgebra.instNegFreeLieAlgebra
(R : Type u)
(X : Type v)
[CommRing R]
:
Neg (FreeLieAlgebra R X)
Equations
- One or more equations did not get rendered due to their size.
instance
FreeLieAlgebra.instSubFreeLieAlgebra
(R : Type u)
(X : Type v)
[CommRing R]
:
Sub (FreeLieAlgebra R X)
Equations
- One or more equations did not get rendered due to their size.
instance
FreeLieAlgebra.instAddGroupFreeLieAlgebra
(R : Type u)
(X : Type v)
[CommRing R]
:
AddGroup (FreeLieAlgebra R X)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
FreeLieAlgebra.instAddCommGroupFreeLieAlgebra
(R : Type u)
(X : Type v)
[CommRing R]
:
AddCommGroup (FreeLieAlgebra R X)
Equations
- FreeLieAlgebra.instAddCommGroupFreeLieAlgebra R X = let src := inferInstance; let src_1 := inferInstance; AddCommGroup.mk (_ : ∀ (a b : FreeLieAlgebra R X), a + b = b + a)
instance
FreeLieAlgebra.instModuleFreeLieAlgebraToAddCommMonoidInstAddCommGroupFreeLieAlgebra
(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
- One or more equations did not get rendered due to their size.
instance
FreeLieAlgebra.instLieRingFreeLieAlgebra
(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
- One or more equations did not get rendered due to their size.
instance
FreeLieAlgebra.instLieAlgebraFreeLieAlgebraInstLieRingFreeLieAlgebra
(R : Type u)
(X : Type v)
[CommRing R]
:
LieAlgebra R (FreeLieAlgebra R X)
Equations
- FreeLieAlgebra.instLieAlgebraFreeLieAlgebraInstLieRingFreeLieAlgebra R X = LieAlgebra.mk (_ : ∀ (t : R) (x y : FreeLieAlgebra R X), ⁅x, t • y⁆ = t • ⁅x, y⁆)
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)
Instances For
def
FreeLieAlgebra.liftAux
(R : Type u)
{X : Type v}
[CommRing R]
{L : Type w}
[LieRing L]
[LieAlgebra R L]
(f : X → CommutatorRing L)
:
An auxiliary definition used to construct the equivalence lift below.
Equations
Instances For
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
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}
[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.
Instances For
@[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)
:
(AlgEquiv.symm (FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra R X)) 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.