# mathlib3documentation

algebra.free_algebra

# Free Algebras #

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

Given a commutative semiring R, and a type X, we construct the free unital, associative R-algebra on X.

## Notation #

1. free_algebra R X is the free algebra itself. It is endowed with an R-algebra structure.
2. free_algebra.ι R is the function X → free_algebra R X.
3. Given a function f : X → A to an R-algebra A, lift R f is the lift of f to an R-algebra morphism free_algebra R X → A.

## Theorems #

1. ι_comp_lift states that the composition (lift R f) ∘ (ι R) is identical to f.
2. lift_unique states that whenever an R-algebra morphism g : free_algebra R X → A is given whose composition with ι R is f, then one has g = lift R f.
3. hom_ext is a variant of lift_unique in the form of an extensionality theorem.
4. lift_comp_ι is a combination of ι_comp_lift and lift_unique. It states that the lift of the composition of an algebra morphism with ι is the algebra morphism itself.
5. equiv_monoid_algebra_free_monoid : free_algebra R X ≃ₐ[R] monoid_algebra R (free_monoid X)
6. An inductive principle induction.

## Implementation details #

We construct the free algebra on X as a quotient of an inductive type free_algebra.pre by an inductively defined relation free_algebra.rel. Explicitly, the construction involves three steps:

1. We construct an inductive type free_algebra.pre R X, the terms of which should be thought of as representatives for the elements of free_algebra R X. It is the free type with maps from R and X, and with two binary operations add and mul.
2. We construct an inductive relation free_algebra.rel R X on free_algebra.pre R X. This is the smallest relation for which the quotient is an R-algebra where addition resp. multiplication are induced by add resp. mul from 1., and for which the map from R is the structure map for the algebra.
3. The free algebra free_algebra R X is the quotient of free_algebra.pre R X by the relation free_algebra.rel R X.
inductive free_algebra.pre (R : Type u_1) (X : Type u_2) :
Type (max u_1 u_2)

This inductive type is used to express representatives of the free algebra.

Instances for free_algebra.pre
@[protected, instance]
def free_algebra.pre.inhabited (R : Type u_1) (X : Type u_2) :
Equations
def free_algebra.pre.has_coe_generator (R : Type u_1) (X : Type u_2) :
X)

Coercion from X to pre R X. Note: Used for notation only.

Equations
def free_algebra.pre.has_coe_semiring (R : Type u_1) (X : Type u_2) :
X)

Coercion from R to pre R X. Note: Used for notation only.

Equations
def free_algebra.pre.has_mul (R : Type u_1) (X : Type u_2) :

Multiplication in pre R X defined as pre.mul. Note: Used for notation only.

Equations
def free_algebra.pre.has_add (R : Type u_1) (X : Type u_2) :

Addition in pre R X defined as pre.add. Note: Used for notation only.

Equations
def free_algebra.pre.has_zero (R : Type u_1) (X : Type u_2) :

Zero in pre R X defined as the image of 0 from R. Note: Used for notation only.

Equations
def free_algebra.pre.has_one (R : Type u_1) (X : Type u_2) :

One in pre R X defined as the image of 1 from R. Note: Used for notation only.

Equations
def free_algebra.pre.has_smul (R : Type u_1) (X : Type u_2) :
X)

Scalar multiplication defined as multiplication by the image of elements from R. Note: Used for notation only.

Equations
• = {smul := λ (r : R) (m : X),
def free_algebra.lift_fun (R : Type u_1) (X : Type u_2) {A : Type u_3} [semiring A] [ A] (f : X A) :
A

Given a function from X to an R-algebra A, lift_fun provides a lift of f to a function from pre R X to A. This is mainly used in the construction of free_algebra.lift.

Equations
inductive free_algebra.rel (R : Type u_1) (X : Type u_2) :
Prop
• add_scalar : {R : Type u_1} [_inst_1 : {X : Type u_2} {r s : R}, (r + s) (r + s)
• mul_scalar : {R : Type u_1} [_inst_1 : {X : Type u_2} {r s : R}, (r * s) (r * s)
• central_scalar : {R : Type u_1} [_inst_1 : {X : Type u_2} {r : R} {a : X}, (r * a) (a * r)
• add_assoc : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b c : X}, (a + b + c) (a + (b + c))
• add_comm : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b : X}, (a + b) (b + a)
• zero_add : {R : Type u_1} [_inst_1 : {X : Type u_2} {a : X}, (0 + a) a
• mul_assoc : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b c : X}, (a * b * c) (a * (b * c))
• one_mul : {R : Type u_1} [_inst_1 : {X : Type u_2} {a : X}, (1 * a) a
• mul_one : {R : Type u_1} [_inst_1 : {X : Type u_2} {a : X}, (a * 1) a
• left_distrib : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b c : X}, (a * (b + c)) (a * b + a * c)
• right_distrib : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b c : X}, ((a + b) * c) (a * c + b * c)
• zero_mul : {R : Type u_1} [_inst_1 : {X : Type u_2} {a : X}, (0 * a) 0
• mul_zero : {R : Type u_1} [_inst_1 : {X : Type u_2} {a : X}, (a * 0) 0
• add_compat_left : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b c : X}, a b (a + c) (b + c)
• add_compat_right : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b c : X}, a b (c + a) (c + b)
• mul_compat_left : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b c : X}, a b (a * c) (b * c)
• mul_compat_right : {R : Type u_1} [_inst_1 : {X : Type u_2} {a b c : X}, a b (c * a) (c * b)

An inductively defined relation on pre R X used to force the initial algebra structure on the associated quotient.

def free_algebra (R : Type u_1) (X : Type u_2) :
Type (max u_1 u_2)

The free algebra for the type X over the commutative semiring R.

Equations
• X = quot X)
Instances for free_algebra
@[protected, instance]
def free_algebra.semiring (R : Type u_1) (X : Type u_2) :
Equations
@[protected, instance]
def free_algebra.inhabited (R : Type u_1) (X : Type u_2) :
Equations
@[protected, instance]
def free_algebra.has_smul (R : Type u_1) (X : Type u_2) :
X)
Equations
@[protected, instance]
def free_algebra.algebra (R : Type u_1) (X : Type u_2) :
X)
Equations
@[protected, instance]
def free_algebra.ring (X : Type u_2) {S : Type u_1} [comm_ring S] :
ring X)
Equations
@[irreducible]
def free_algebra.ι (R : Type u_1) {X : Type u_2} :
X X

The canonical function X → free_algebra R X.

Equations
• = λ (m : X), quot.mk X) m
@[simp]
theorem free_algebra.quot_mk_eq_ι (R : Type u_1) {X : Type u_2} (m : X) :
quot.mk X) m =
@[irreducible]
def free_algebra.lift (R : Type u_1) {X : Type u_2} {A : Type u_3} [semiring A] [ A] :
(X A) X →ₐ[R] A)

Given a function f : X → A where A is an R-algebra, lift R f is the unique lift of f to a morphism of R-algebras free_algebra R X → A.

Equations
@[simp]
theorem free_algebra.lift_aux_eq (R : Type u_1) {X : Type u_2} {A : Type u_3} [semiring A] [ A] (f : X A) :
lift_aux R f = f
@[simp]
theorem free_algebra.lift_symm_apply (R : Type u_1) {X : Type u_2} {A : Type u_3} [semiring A] [ A] (F : X →ₐ[R] A) :
.symm) F =
@[simp]
theorem free_algebra.ι_comp_lift {R : Type u_1} {X : Type u_2} {A : Type u_3} [semiring A] [ A] (f : X A) :
( f) = f
@[simp]
theorem free_algebra.lift_ι_apply {R : Type u_1} {X : Type u_2} {A : Type u_3} [semiring A] [ A] (f : X A) (x : X) :
( f) x) = f x
@[simp]
theorem free_algebra.lift_unique {R : Type u_1} {X : Type u_2} {A : Type u_3} [semiring A] [ A] (f : X A) (g : X →ₐ[R] A) :
= f g = f

Since we have set the basic definitions as @[irreducible], from this point onwards one should only use the universal properties of the free algebra, and consider the actual implementation as a quotient of an inductive type as completely hidden.

@[simp]
theorem free_algebra.lift_comp_ι {R : Type u_1} {X : Type u_2} {A : Type u_3} [semiring A] [ A] (g : X →ₐ[R] A) :
(g = g
@[ext]
theorem free_algebra.hom_ext {R : Type u_1} {X : Type u_2} {A : Type u_3} [semiring A] [ A] {f g : X →ₐ[R] A} (w : = ) :
f = g
noncomputable def free_algebra.equiv_monoid_algebra_free_monoid {R : Type u_1} {X : Type u_2} :

The free algebra on X is "just" the monoid algebra on the free monoid on X.

This would be useful when constructing linear maps out of a free algebra, for example.

Equations
@[protected, instance]
def free_algebra.nontrivial {R : Type u_1} {X : Type u_2} [nontrivial R] :
def free_algebra.algebra_map_inv {R : Type u_1} {X : Type u_2} :
X →ₐ[R] R

The left-inverse of algebra_map.

Equations
theorem free_algebra.algebra_map_left_inverse {R : Type u_1} {X : Type u_2} :
@[simp]
theorem free_algebra.algebra_map_inj {R : Type u_1} {X : Type u_2} (x y : R) :
X)) x = X)) y x = y
@[simp]
theorem free_algebra.algebra_map_eq_zero_iff {R : Type u_1} {X : Type u_2} (x : R) :
X)) x = 0 x = 0
@[simp]
theorem free_algebra.algebra_map_eq_one_iff {R : Type u_1} {X : Type u_2} (x : R) :
X)) x = 1 x = 1
theorem free_algebra.ι_injective {R : Type u_1} {X : Type u_2} [nontrivial R] :
@[simp]
theorem free_algebra.ι_inj {R : Type u_1} {X : Type u_2} [nontrivial R] (x y : X) :
= x = y
@[simp]
theorem free_algebra.ι_ne_algebra_map {R : Type u_1} {X : Type u_2} [nontrivial R] (x : X) (r : R) :
X)) r
@[simp]
theorem free_algebra.ι_ne_zero {R : Type u_1} {X : Type u_2} [nontrivial R] (x : X) :
0
@[simp]
theorem free_algebra.ι_ne_one {R : Type u_1} {X : Type u_2} [nontrivial R] (x : X) :
1
theorem free_algebra.induction (R : Type u_1) (X : Type u_2) {C : X Prop} (h_grade0 : (r : R), C ( X)) r)) (h_grade1 : (x : X), C x)) (h_mul : (a b : X), C a C b C (a * b)) (h_add : (a b : X), C a C b C (a + b)) (a : X) :
C a

An induction principle for the free algebra.

If C holds for the algebra_map of r : R into free_algebra R X, the ι of x : X, and is preserved under addition and muliplication, then it holds for all of free_algebra R X.