# Documentation

Mathlib.Algebra.FreeAlgebra

# Free Algebras #

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

## Notation #

1. FreeAlgebra R X is the free algebra itself. It is endowed with an R-algebra structure.
2. FreeAlgebra.ι R is the function X → FreeAlgebra 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 FreeAlgebra 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 : FreeAlgebra 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. equivMonoidAlgebraFreeMonoid : FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)
6. An inductive principle induction.

## Implementation details #

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

1. We construct an inductive type FreeAlgebra.Pre R X, the terms of which should be thought of as representatives for the elements of FreeAlgebra 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 FreeAlgebra.Rel R X on FreeAlgebra.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 FreeAlgebra R X is the quotient of FreeAlgebra.Pre R X by the relation FreeAlgebra.Rel R X.
inductive FreeAlgebra.Pre (R : Type u_1) (X : Type u_2) :
Type (max u_1 u_2)
• of: {R : Type u_1} → {X : Type u_2} → X
• of_scalar: {R : Type u_1} → {X : Type u_2} → R
• add: {R : Type u_1} → {X : Type u_2} → → →
• mul: {R : Type u_1} → {X : Type u_2} → → →

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

Instances For
instance FreeAlgebra.Pre.instInhabitedPre (R : Type u_1) [] (X : Type u_2) :
def FreeAlgebra.Pre.hasCoeGenerator (R : Type u_1) (X : Type u_2) :
Coe X ()

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

Instances For
def FreeAlgebra.Pre.hasCoeSemiring (R : Type u_1) (X : Type u_2) :
Coe R ()

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

Instances For
def FreeAlgebra.Pre.hasMul (R : Type u_1) (X : Type u_2) :
Mul ()

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

Instances For
def FreeAlgebra.Pre.hasAdd (R : Type u_1) (X : Type u_2) :

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

Instances For
def FreeAlgebra.Pre.hasZero (R : Type u_1) [] (X : Type u_2) :
Zero ()

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

Instances For
def FreeAlgebra.Pre.hasOne (R : Type u_1) [] (X : Type u_2) :
One ()

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

Instances For
def FreeAlgebra.Pre.hasSmul (R : Type u_1) (X : Type u_2) :
SMul R ()

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

Instances For
def FreeAlgebra.liftFun (R : Type u_1) [] (X : Type u_2) {A : Type u_3} [] [Algebra R A] (f : XA) :
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 FreeAlgebra.lift.

Equations
Instances For
inductive FreeAlgebra.Rel (R : Type u_1) [] (X : Type u_2) :
Prop

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

Instances For
def FreeAlgebra (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.

Instances For

Define the basic operations

instance FreeAlgebra.instSMul (R : Type u_1) [] (X : Type u_2) {A : Type u_3} [] [Algebra R A] :
SMul R ()
instance FreeAlgebra.instZero (R : Type u_1) [] (X : Type u_2) :
Zero ()
instance FreeAlgebra.instOne (R : Type u_1) [] (X : Type u_2) :
One ()
instance FreeAlgebra.instAdd (R : Type u_1) [] (X : Type u_2) :
instance FreeAlgebra.instMul (R : Type u_1) [] (X : Type u_2) :
Mul ()

Build the semiring structure. We do this one piece at a time as this is convenient for proving the nsmul fields.

instance FreeAlgebra.instMonoidWithZero (R : Type u_1) [] (X : Type u_2) :
instance FreeAlgebra.instDistrib (R : Type u_1) [] (X : Type u_2) :
instance FreeAlgebra.instAddCommMonoid (R : Type u_1) [] (X : Type u_2) :
instance FreeAlgebra.instSemiringFreeAlgebra (R : Type u_1) [] (X : Type u_2) :
instance FreeAlgebra.instAlgebra (R : Type u_1) [] (X : Type u_2) {A : Type u_3} [] [Algebra R A] :
Algebra R ()
instance FreeAlgebra.instIsScalarTowerFreeAlgebraInstSMulInstSMul (X : Type u_2) {R : Type u_3} {S : Type u_4} {A : Type u_5} [] [] [] [SMul R S] [Algebra R A] [Algebra S A] [] :
instance FreeAlgebra.instSMulCommClassFreeAlgebraInstSMulInstSMul (X : Type u_2) {R : Type u_3} {S : Type u_4} {A : Type u_5} [] [] [] [Algebra R A] [Algebra S A] [] :
@[irreducible]
def FreeAlgebra.ι (R : Type u_3) [] {X : Type u_4} :
X

The canonical function X → FreeAlgebra R X.

Instances For
theorem FreeAlgebra.ι_def (R : Type u_3) [] {X : Type u_4} (m : X) :
= Quot.mk () ()
@[simp]
theorem FreeAlgebra.quot_mk_eq_ι (R : Type u_1) [] {X : Type u_2} (m : X) :
Quot.mk () () =
@[irreducible]
def FreeAlgebra.lift (R : Type u_1) [] {X : Type u_2} {A : Type u_3} [] [Algebra R A] :
(XA) ( →ₐ[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 FreeAlgebra R X → A.

Instances For
@[simp]
theorem FreeAlgebra.liftAux_eq (R : Type u_1) [] {X : Type u_2} {A : Type u_3} [] [Algebra R A] (f : XA) :
= ↑() f
@[simp]
theorem FreeAlgebra.lift_symm_apply (R : Type u_1) [] {X : Type u_2} {A : Type u_3} [] [Algebra R A] (F : →ₐ[R] A) :
().symm F = F
@[simp]
theorem FreeAlgebra.ι_comp_lift {R : Type u_1} [] {X : Type u_2} {A : Type u_3} [] [Algebra R A] (f : XA) :
↑(↑() f) = f
@[simp]
theorem FreeAlgebra.lift_ι_apply {R : Type u_1} [] {X : Type u_2} {A : Type u_3} [] [Algebra R A] (f : XA) (x : X) :
↑(↑() f) () = f x
@[simp]
theorem FreeAlgebra.lift_unique {R : Type u_1} [] {X : Type u_2} {A : Type u_3} [] [Algebra R A] (f : XA) (g : →ₐ[R] A) :
g = 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 FreeAlgebra.lift_comp_ι {R : Type u_1} [] {X : Type u_2} {A : Type u_3} [] [Algebra R A] (g : →ₐ[R] A) :
↑() (g ) = g
theorem FreeAlgebra.hom_ext {R : Type u_1} [] {X : Type u_2} {A : Type u_3} [] [Algebra R A] {f : →ₐ[R] A} {g : →ₐ[R] A} (w : f = g ) :
f = g

See note [partially-applied ext lemmas].

noncomputable def FreeAlgebra.equivMonoidAlgebraFreeMonoid {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.

Instances For
instance FreeAlgebra.instNontrivialFreeAlgebra {R : Type u_1} [] {X : Type u_2} [] :
def FreeAlgebra.algebraMapInv {R : Type u_1} [] {X : Type u_2} :

The left-inverse of algebraMap.

Instances For
theorem FreeAlgebra.algebraMap_leftInverse {R : Type u_1} [] {X : Type u_2} :
Function.LeftInverse FreeAlgebra.algebraMapInv ↑(algebraMap R ())
@[simp]
theorem FreeAlgebra.algebraMap_inj {R : Type u_1} [] {X : Type u_2} (x : R) (y : R) :
↑(algebraMap R ()) x = ↑(algebraMap R ()) y x = y
@[simp]
theorem FreeAlgebra.algebraMap_eq_zero_iff {R : Type u_1} [] {X : Type u_2} (x : R) :
↑(algebraMap R ()) x = 0 x = 0
@[simp]
theorem FreeAlgebra.algebraMap_eq_one_iff {R : Type u_1} [] {X : Type u_2} (x : R) :
↑(algebraMap R ()) x = 1 x = 1
theorem FreeAlgebra.ι_injective {R : Type u_1} [] {X : Type u_2} [] :
@[simp]
theorem FreeAlgebra.ι_inj {R : Type u_1} [] {X : Type u_2} [] (x : X) (y : X) :
= x = y
@[simp]
theorem FreeAlgebra.ι_ne_algebraMap {R : Type u_1} [] {X : Type u_2} [] (x : X) (r : R) :
↑(algebraMap R ()) r
@[simp]
theorem FreeAlgebra.ι_ne_zero {R : Type u_1} [] {X : Type u_2} [] (x : X) :
0
@[simp]
theorem FreeAlgebra.ι_ne_one {R : Type u_1} [] {X : Type u_2} [] (x : X) :
1
theorem FreeAlgebra.induction (R : Type u_1) [] (X : Type u_2) {C : Prop} (h_grade0 : (r : R) → C (↑(algebraMap R ()) r)) (h_grade1 : (x : X) → C ()) (h_mul : (a b : ) → C aC bC (a * b)) (h_add : (a b : ) → C aC bC (a + b)) (a : ) :
C a

An induction principle for the free algebra.

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

@[simp]
theorem FreeAlgebra.adjoin_range_ι (R : Type u_1) [] (X : Type u_2) :
theorem Algebra.adjoin_range_eq_range_freeAlgebra_lift (R : Type u_1) [] (X : Type u_2) {A : Type u_3} [] [Algebra R A] (f : XA) :
= AlgHom.range (↑() f)

Noncommutative version of Algebra.adjoin_range_eq_range_aeval.

theorem Algebra.adjoin_eq_range_freeAlgebra_lift (R : Type u_1) [] {A : Type u_3} [] [Algebra R A] (s : Set A) :
= AlgHom.range (↑() Subtype.val)

Noncommutative version of Algebra.adjoin_range_eq_range.