mathlib3 documentation

algebra.free_non_unital_non_assoc_algebra

Free algebras #

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

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

Main definitions #

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 free_non_unital_non_assoc_algebra 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

source
@[reducible]
def free_non_unital_non_assoc_algebra (R : Type u) (X : Type v) [semiring R] :
Type (max u v)

The free non-unital, non-associative algebra on the type X with coefficients in R.

source
noncomputable def free_non_unital_non_assoc_algebra.of (R : Type u) {X : Type v} [semiring R] :
X → free_non_unital_non_assoc_algebra R X

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

Equations
source
noncomputable def free_non_unital_non_assoc_algebra.lift (R : Type u) {X : Type v} [semiring R] {A : Type w} [non_unital_non_assoc_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] :
(X → A) ≃ (free_non_unital_non_assoc_algebra R X →ₙₐ[R] A)

The functor X ↦ free_non_unital_non_assoc_algebra 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
source
@[simp]
theorem free_non_unital_non_assoc_algebra.lift_symm_apply (R : Type u) {X : Type v} [semiring R] {A : Type w} [non_unital_non_assoc_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] (F : free_non_unital_non_assoc_algebra R X →ₙₐ[R] A) :
⇑((free_non_unital_non_assoc_algebra.lift R).symm) F = ⇑F ∘ free_non_unital_non_assoc_algebra.of R
source
@[simp]
theorem free_non_unital_non_assoc_algebra.of_comp_lift (R : Type u) {X : Type v} [semiring R] {A : Type w} [non_unital_non_assoc_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] (f : X → A) :
⇑(⇑(free_non_unital_non_assoc_algebra.lift R) f) ∘ free_non_unital_non_assoc_algebra.of R = f
source
@[simp]
theorem free_non_unital_non_assoc_algebra.lift_unique (R : Type u) {X : Type v} [semiring R] {A : Type w} [non_unital_non_assoc_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] (f : X → A) (F : free_non_unital_non_assoc_algebra R X →ₙₐ[R] A) :
⇑F ∘ free_non_unital_non_assoc_algebra.of R = f ↔ F = ⇑(free_non_unital_non_assoc_algebra.lift R) f
source
@[simp]
theorem free_non_unital_non_assoc_algebra.lift_of_apply (R : Type u) {X : Type v} [semiring R] {A : Type w} [non_unital_non_assoc_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] (f : X → A) (x : X) :
⇑(⇑(free_non_unital_non_assoc_algebra.lift R) f) (free_non_unital_non_assoc_algebra.of R x) = f x
source
@[simp]
theorem free_non_unital_non_assoc_algebra.lift_comp_of (R : Type u) {X : Type v} [semiring R] {A : Type w} [non_unital_non_assoc_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] (F : free_non_unital_non_assoc_algebra R X →ₙₐ[R] A) :
⇑(free_non_unital_non_assoc_algebra.lift R) (⇑F ∘ free_non_unital_non_assoc_algebra.of R) = F
source
@[ext]
theorem free_non_unital_non_assoc_algebra.hom_ext (R : Type u) {X : Type v} [semiring R] {A : Type w} [non_unital_non_assoc_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] {F₁ F₂ : free_non_unital_non_assoc_algebra R X →ₙₐ[R] A} (h : ∀ (x : X), ⇑F₁ (free_non_unital_non_assoc_algebra.of R x) = ⇑F₂ (free_non_unital_non_assoc_algebra.of R x)) :
F₁ = F₂