Documentation

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

Instances For
    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
    Instances For
      Equations
      instance FreeLieAlgebra.instSMulOfIsScalarTower (R : Type u) (X : Type v) [CommRing R] {S : Type u_1} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] :
      Equations
      instance FreeLieAlgebra.instZero (R : Type u) (X : Type v) [CommRing R] :
      Equations
      instance FreeLieAlgebra.instAdd (R : Type u) (X : Type v) [CommRing R] :
      Equations
      instance FreeLieAlgebra.instNeg (R : Type u) (X : Type v) [CommRing R] :
      Equations
      instance FreeLieAlgebra.instSub (R : Type u) (X : Type v) [CommRing R] :
      Equations
      instance FreeLieAlgebra.instModuleOfIsScalarTower (R : Type u) (X : Type v) [CommRing R] {S : Type u_1} [Semiring S] [Module S R] [IsScalarTower S R R] :
      Equations

      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} [CommRing R] :
      XFreeLieAlgebra R X

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

      Equations
      Instances For

        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 : XL) (t : R) (a : FreeNonUnitalNonAssocAlgebra R X) :

          The quotient map as a NonUnitalAlgHom.

          Equations
          Instances For
            def FreeLieAlgebra.lift (R : Type u) {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] :
            (XL) (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) :
              @[simp]
              theorem FreeLieAlgebra.of_comp_lift {R : Type u} {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : XL) :
              @[simp]
              theorem FreeLieAlgebra.lift_unique {R : Type u} {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : XL) (g : FreeLieAlgebra R X →ₗ⁅R L) :
              @[simp]
              theorem FreeLieAlgebra.lift_of_apply {R : Type u} {X : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (f : XL) (x : 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) :
              theorem FreeLieAlgebra.hom_ext_iff {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} :
              F₁ = F₂ ∀ (x : X), F₁ (FreeLieAlgebra.of R x) = F₂ (FreeLieAlgebra.of R x)
              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₂

              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