Free algebras

Given a semiring R and a type X, we construct the free non-unital, non-associative algebra on X with coefficients in R, together with its universal property. The construction is valuable because it can be used to build free algebras with more structure, e.g., free Lie algebras.

Note that elsewhere we have a construction of the free unital, associative algebra. This is called FreeAlgebra.

Main definitions

• FreeNonUnitalNonAssocAlgebra
• FreeNonUnitalNonAssocAlgebra.lift
• FreeNonUnitalNonAssocAlgebra.of

Implementation details

We construct the free algebra as the magma algebra, with coefficients in R, of the free magma on X. However we regard this as an implementation detail and thus deliberately omit the lemmas of_apply and lift_apply, and we mark FreeNonUnitalNonAssocAlgebra and lift as irreducible once we have established the universal property.

Tags

free algebra, non-unital, non-associative, free magma, magma algebra, universal property, forgetful functor, adjoint functor

@[reducible, inline]

abbrev FreeNonUnitalNonAssocAlgebra (R : Type u) (X : Type v) [Semiring R] : Type (max u v)

If α is a type, and R is a semiring, then FreeNonUnitalNonAssocAlgebra R α is the free non-unital non-associative R-algebra generated by α. This is an R-algebra equipped with a function FreeNonUnitalNonAssocAlgebra.of R : α → FreeNonUnitalNonAssocAlgebra R α which has the following universal property: if A is any R-algebra, and f : α → A is any function, then this function is the composite of FreeNonUnitalNonAssocAlgebra.of R and a unique non-unital R-algebra homomorphism FreeNonUnitalNonAssocAlgebra.lift R f : FreeNonUnitalNonAssocAlgebra R α →ₙₐ[R] A.

A typical element of FreeNonUnitalNonAssocAlgebra R α is an R-linear combination of nonempty formal (non-commutative, non-associative) products of elements of α. For example if x and y are terms of type α and a, b are terms of type R then (3 * a * a) • (x * (y * x)) + (2 * b + 1) • (y * x) is a "typical" element of FreeNonUnitalNonAssocAlgebra R α.

Equations

• FreeNonUnitalNonAssocAlgebra R X = MonoidAlgebra R (FreeMagma X)

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

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

Equations

• FreeNonUnitalNonAssocAlgebra.of R = ⇑(MonoidAlgebra.ofMagma R (FreeMagma X)) ∘ FreeMagma.of

def FreeNonUnitalNonAssocAlgebra.lift (R : Type u) {X : Type v} [Semiring R] {A : Type w} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : (X → A) ≃ (FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A)

The functor X ↦ FreeNonUnitalNonAssocAlgebra R X from the category of types to the category of non-unital, non-associative algebras over R is adjoint to the forgetful functor in the other direction.

Equations

• FreeNonUnitalNonAssocAlgebra.lift R = FreeMagma.lift.trans (MonoidAlgebra.liftMagma R)

@[simp]

theorem FreeNonUnitalNonAssocAlgebra.lift_symm_apply (R : Type u) {X : Type v} [Semiring R] {A : Type w} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) : (lift R).symm F = ⇑F ∘ of R

@[simp]

theorem FreeNonUnitalNonAssocAlgebra.of_comp_lift (R : Type u) {X : Type v} [Semiring R] {A : Type w} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (f : X → A) : ⇑((lift R) f) ∘ of R = f

@[simp]

theorem FreeNonUnitalNonAssocAlgebra.lift_unique (R : Type u) {X : Type v} [Semiring R] {A : Type w} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (f : X → A) (F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) : ⇑F ∘ of R = f ↔ F = (lift R) f

@[simp]

theorem FreeNonUnitalNonAssocAlgebra.lift_of_apply (R : Type u) {X : Type v} [Semiring R] {A : Type w} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (f : X → A) (x : X) : ((lift R) f) (of R x) = f x

@[simp]

theorem FreeNonUnitalNonAssocAlgebra.lift_comp_of (R : Type u) {X : Type v} [Semiring R] {A : Type w} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) : (lift R) (⇑F ∘ of R) = F

theorem FreeNonUnitalNonAssocAlgebra.hom_ext (R : Type u) {X : Type v} [Semiring R] {A : Type w} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {F₁ F₂ : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A} (h : ∀ (x : X), F₁ (of R x) = F₂ (of R x)) : F₁ = F₂

theorem FreeNonUnitalNonAssocAlgebra.hom_ext_iff {R : Type u} {X : Type v} [Semiring R] {A : Type w} [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {F₁ F₂ : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A} : F₁ = F₂ ↔ ∀ (x : X), F₁ (of R x) = F₂ (of R x)