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)

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

• of {R : Type u_1} {X : Type u_2} : X → Pre R X
• ofScalar {R : Type u_1} {X : Type u_2} : R → Pre R X
• add {R : Type u_1} {X : Type u_2} : Pre R X → Pre R X → Pre R X
• mul {R : Type u_1} {X : Type u_2} : Pre R X → Pre R X → Pre R X

instance FreeAlgebra.Pre.instInhabited (R : Type u_1) [CommSemiring R] (X : Type u_2) : Inhabited (Pre R X)

Equations

• FreeAlgebra.Pre.instInhabited R X = { default := FreeAlgebra.Pre.ofScalar 0 }

def FreeAlgebra.Pre.hasCoeGenerator (R : Type u_1) (X : Type u_2) : Coe X (Pre R X)

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

Equations

• FreeAlgebra.Pre.hasCoeGenerator R X = { coe := FreeAlgebra.Pre.of }

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

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

Equations

• FreeAlgebra.Pre.hasCoeSemiring R X = { coe := FreeAlgebra.Pre.ofScalar }

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

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

Equations

• FreeAlgebra.Pre.hasMul R X = { mul := FreeAlgebra.Pre.mul }

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

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

Equations

• FreeAlgebra.Pre.hasAdd R X = { add := FreeAlgebra.Pre.add }

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

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

Equations

• FreeAlgebra.Pre.hasZero R X = { zero := FreeAlgebra.Pre.ofScalar 0 }

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

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

Equations

• FreeAlgebra.Pre.hasOne R X = { one := FreeAlgebra.Pre.ofScalar 1 }

def FreeAlgebra.Pre.hasSMul (R : Type u_1) (X : Type u_2) : SMul R (Pre R X)

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

Equations

• FreeAlgebra.Pre.hasSMul R X = { smul := fun (r : R) (m : FreeAlgebra.Pre R X) => (FreeAlgebra.Pre.ofScalar r).mul m }

def FreeAlgebra.liftFun (R : Type u_1) [CommSemiring R] (X : Type u_2) {A : Type u_3} [Semiring A] [Algebra R A] (f : X → A) : Pre R X → 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

• FreeAlgebra.liftFun R X f (FreeAlgebra.Pre.of t) = f t
• FreeAlgebra.liftFun R X f (a.add b) = FreeAlgebra.liftFun R X f a + FreeAlgebra.liftFun R X f b
• FreeAlgebra.liftFun R X f (a.mul b) = FreeAlgebra.liftFun R X f a * FreeAlgebra.liftFun R X f b
• FreeAlgebra.liftFun R X f (FreeAlgebra.Pre.ofScalar c) = (algebraMap R A) c

inductive FreeAlgebra.Rel (R : Type u_1) [CommSemiring R] (X : Type u_2) : Pre R X → Pre R X → Prop

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

• add_scalar {R : Type u_1} [CommSemiring R] {X : Type u_2} {r s : R} : Rel R X (Pre.ofScalar (r + s)) (Pre.ofScalar r + Pre.ofScalar s)
• mul_scalar {R : Type u_1} [CommSemiring R] {X : Type u_2} {r s : R} : Rel R X (Pre.ofScalar (r * s)) (Pre.ofScalar r * Pre.ofScalar s)
• central_scalar {R : Type u_1} [CommSemiring R] {X : Type u_2} {r : R} {a : Pre R X} : Rel R X (Pre.ofScalar r * a) (a * Pre.ofScalar r)
• add_assoc {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b c : Pre R X} : Rel R X (a + b + c) (a + (b + c))
• add_comm {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b : Pre R X} : Rel R X (a + b) (b + a)
• zero_add {R : Type u_1} [CommSemiring R] {X : Type u_2} {a : Pre R X} : Rel R X (0 + a) a
• mul_assoc {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b c : Pre R X} : Rel R X (a * b * c) (a * (b * c))
• one_mul {R : Type u_1} [CommSemiring R] {X : Type u_2} {a : Pre R X} : Rel R X (1 * a) a
• mul_one {R : Type u_1} [CommSemiring R] {X : Type u_2} {a : Pre R X} : Rel R X (a * 1) a
• left_distrib {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b c : Pre R X} : Rel R X (a * (b + c)) (a * b + a * c)
• right_distrib {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b c : Pre R X} : Rel R X ((a + b) * c) (a * c + b * c)
• zero_mul {R : Type u_1} [CommSemiring R] {X : Type u_2} {a : Pre R X} : Rel R X (0 * a) 0
• mul_zero {R : Type u_1} [CommSemiring R] {X : Type u_2} {a : Pre R X} : Rel R X (a * 0) 0
• add_compat_left {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b c : Pre R X} : Rel R X a b → Rel R X (a + c) (b + c)
• add_compat_right {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b c : Pre R X} : Rel R X a b → Rel R X (c + a) (c + b)
• mul_compat_left {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b c : Pre R X} : Rel R X a b → Rel R X (a * c) (b * c)
• mul_compat_right {R : Type u_1} [CommSemiring R] {X : Type u_2} {a b c : Pre R X} : Rel R X a b → Rel R X (c * a) (c * b)

def FreeAlgebra (R : Type u_1) [CommSemiring R] (X : Type u_2) : Type (max u_1 u_2)

If α is a type, and R is a commutative semiring, then FreeAlgebra R α is the free (unital, associative) R-algebra generated by α. This is an R-algebra equipped with a function FreeAlgebra.ι R : α → FreeAlgebra 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 FreeAlgebra.ι R and a unique R-algebra homomorphism FreeAlgebra.lift R f : FreeAlgebra R α →ₐ[R] A.

A typical element of FreeAlgebra R α is an R-linear combination of formal 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) + (a * b * b + 3) is a "typical" element of FreeAlgebra R α. In particular if α is empty then FreeAlgebra R α is isomorphic to R, and if α has one term t then FreeAlgebra R α is isomorphic to the polynomial ring R[t]. If α has two or more terms then FreeAlgebra R α is not commutative. One can think of FreeAlgebra R α as the free non-commutative polynomial ring with coefficients in R and variables indexed by α.

Equations

• FreeAlgebra R X = Quot (FreeAlgebra.Rel R X)

Define the basic operations

instance FreeAlgebra.instSMul (R : Type u_1) [CommSemiring R] (X : Type u_2) {A : Type u_3} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X)

Equations

• FreeAlgebra.instSMul R X = { smul := fun (r : R) => Quot.map (HMul.hMul (FreeAlgebra.Pre.ofScalar ((algebraMap R A) r))) ⋯ }

instance FreeAlgebra.instZero (R : Type u_1) [CommSemiring R] (X : Type u_2) : Zero (FreeAlgebra R X)

Equations

• FreeAlgebra.instZero R X = { zero := Quot.mk (FreeAlgebra.Rel R X) 0 }

instance FreeAlgebra.instOne (R : Type u_1) [CommSemiring R] (X : Type u_2) : One (FreeAlgebra R X)

Equations

• FreeAlgebra.instOne R X = { one := Quot.mk (FreeAlgebra.Rel R X) 1 }

instance FreeAlgebra.instAdd (R : Type u_1) [CommSemiring R] (X : Type u_2) : Add (FreeAlgebra R X)

Equations

• FreeAlgebra.instAdd R X = { add := Quot.map₂ HAdd.hAdd ⋯ ⋯ }

instance FreeAlgebra.instMul (R : Type u_1) [CommSemiring R] (X : Type u_2) : Mul (FreeAlgebra R X)

Equations

• FreeAlgebra.instMul R X = { mul := Quot.map₂ HMul.hMul ⋯ ⋯ }

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) [CommSemiring R] (X : Type u_2) : MonoidWithZero (FreeAlgebra R X)

Equations

• One or more equations did not get rendered due to their size.

instance FreeAlgebra.instDistrib (R : Type u_1) [CommSemiring R] (X : Type u_2) : Distrib (FreeAlgebra R X)

Equations

• FreeAlgebra.instDistrib R X = { toMul := FreeAlgebra.instMul R X, toAdd := FreeAlgebra.instAdd R X, left_distrib := ⋯, right_distrib := ⋯ }

instance FreeAlgebra.instAddCommMonoid (R : Type u_1) [CommSemiring R] (X : Type u_2) : AddCommMonoid (FreeAlgebra R X)

Equations

• One or more equations did not get rendered due to their size.

instance FreeAlgebra.instSemiring (R : Type u_1) [CommSemiring R] (X : Type u_2) : Semiring (FreeAlgebra R X)

Equations

• One or more equations did not get rendered due to their size.

instance FreeAlgebra.instInhabited (R : Type u_1) [CommSemiring R] (X : Type u_2) : Inhabited (FreeAlgebra R X)

Equations

• FreeAlgebra.instInhabited R X = { default := 0 }

instance FreeAlgebra.instAlgebra (R : Type u_1) [CommSemiring R] (X : Type u_2) {A : Type u_3} [CommSemiring A] [Algebra R A] : Algebra R (FreeAlgebra A X)

Equations

• One or more equations did not get rendered due to their size.

instance FreeAlgebra.instIsScalarTower (X : Type u_2) {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring A] [SMul R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] : IsScalarTower R S (FreeAlgebra A X)

instance FreeAlgebra.instSMulCommClass (X : Type u_2) {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A] [Algebra S A] : SMulCommClass R S (FreeAlgebra A X)

instance FreeAlgebra.instRing (X : Type u_2) {S : Type u_3} [CommRing S] : Ring (FreeAlgebra S X)

Equations

• FreeAlgebra.instRing X = Algebra.semiringToRing S

theorem FreeAlgebra.ι_def (R : Type u_3) [CommSemiring R] {X : Type u_4} (m : X) : ι R m = Quot.mk (Rel R X) (Pre.of m)

@[irreducible]

def FreeAlgebra.ι (R : Type u_3) [CommSemiring R] {X : Type u_4} : X → FreeAlgebra R X

The canonical function X → FreeAlgebra R X.

Equations

• FreeAlgebra.ι R m = Quot.mk (FreeAlgebra.Rel R X) (FreeAlgebra.Pre.of m)

@[simp]

theorem FreeAlgebra.quot_mk_eq_ι (R : Type u_1) [CommSemiring R] {X : Type u_2} (m : X) : Quot.mk (Rel R X) (Pre.of m) = ι R m

@[irreducible]

def FreeAlgebra.lift (R : Type u_1) [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] : (X → A) ≃ (FreeAlgebra R 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 FreeAlgebra R X → A.

Equations

• FreeAlgebra.lift R = { toFun := FreeAlgebra.liftAux✝ R, invFun := fun (F : FreeAlgebra R X →ₐ[R] A) => ⇑F ∘ FreeAlgebra.ι R, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FreeAlgebra.liftAux_eq (R : Type u_1) [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (f : X → A) : FreeAlgebra.liftAux✝ R f = (lift R) f

@[simp]

theorem FreeAlgebra.lift_symm_apply (R : Type u_1) [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (F : FreeAlgebra R X →ₐ[R] A) : (lift R).symm F = ⇑F ∘ ι R

@[simp]

theorem FreeAlgebra.ι_comp_lift {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (f : X → A) : ⇑((lift R) f) ∘ ι R = f

@[simp]

theorem FreeAlgebra.lift_ι_apply {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (f : X → A) (x : X) : ((lift R) f) (ι R x) = f x

@[simp]

theorem FreeAlgebra.lift_unique {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (f : X → A) (g : FreeAlgebra R X →ₐ[R] A) : ⇑g ∘ ι R = f ↔ g = (lift R) 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} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (g : FreeAlgebra R X →ₐ[R] A) : (lift R) (⇑g ∘ ι R) = g

theorem FreeAlgebra.hom_ext {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] {f g : FreeAlgebra R X →ₐ[R] A} (w : ⇑f ∘ ι R = ⇑g ∘ ι R) : f = g

See note [partially-applied ext lemmas].

theorem FreeAlgebra.hom_ext_iff {R : Type u_1} [CommSemiring R] {X : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] {f g : FreeAlgebra R X →ₐ[R] A} : f = g ↔ ⇑f ∘ ι R = ⇑g ∘ ι R

noncomputable def FreeAlgebra.equivMonoidAlgebraFreeMonoid {R : Type u_1} [CommSemiring R] {X : Type u_2} : FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)

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

• One or more equations did not get rendered due to their size.

instance FreeAlgebra.instNontrivial {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] : Nontrivial (FreeAlgebra R X)

FreeAlgebra R X is nontrivial when R is.

instance FreeAlgebra.instNoZeroDivisors {R : Type u_1} [CommSemiring R] {X : Type u_2} [NoZeroDivisors R] : NoZeroDivisors (FreeAlgebra R X)

FreeAlgebra R X has no zero-divisors when R has no zero-divisors.

instance FreeAlgebra.instIsDomain {R : Type u_4} {X : Type u_5} [CommRing R] [IsDomain R] : IsDomain (FreeAlgebra R X)

FreeAlgebra R X is a domain when R is an integral domain.

def FreeAlgebra.algebraMapInv {R : Type u_1} [CommSemiring R] {X : Type u_2} : FreeAlgebra R X →ₐ[R] R

The left-inverse of algebraMap.

Equations

• FreeAlgebra.algebraMapInv = (FreeAlgebra.lift R) 0

theorem FreeAlgebra.algebraMap_leftInverse {R : Type u_1} [CommSemiring R] {X : Type u_2} : Function.LeftInverse ⇑algebraMapInv ⇑(algebraMap R (FreeAlgebra R X))

@[simp]

theorem FreeAlgebra.algebraMap_inj {R : Type u_1} [CommSemiring R] {X : Type u_2} (x y : R) : (algebraMap R (FreeAlgebra R X)) x = (algebraMap R (FreeAlgebra R X)) y ↔ x = y

@[simp]

theorem FreeAlgebra.algebraMap_eq_zero_iff {R : Type u_1} [CommSemiring R] {X : Type u_2} (x : R) : (algebraMap R (FreeAlgebra R X)) x = 0 ↔ x = 0

@[simp]

theorem FreeAlgebra.algebraMap_eq_one_iff {R : Type u_1} [CommSemiring R] {X : Type u_2} (x : R) : (algebraMap R (FreeAlgebra R X)) x = 1 ↔ x = 1

theorem FreeAlgebra.ι_injective {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] : Function.Injective (ι R)

@[simp]

theorem FreeAlgebra.ι_inj {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x y : X) : ι R x = ι R y ↔ x = y

@[simp]

theorem FreeAlgebra.ι_ne_algebraMap {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x : X) (r : R) : ι R x ≠ (algebraMap R (FreeAlgebra R X)) r

@[simp]

theorem FreeAlgebra.ι_ne_zero {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x : X) : ι R x ≠ 0

@[simp]

theorem FreeAlgebra.ι_ne_one {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x : X) : ι R x ≠ 1

theorem FreeAlgebra.induction (R : Type u_1) [CommSemiring R] (X : Type u_2) {motive : FreeAlgebra R X → Prop} (grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)) (grade1 : ∀ (x : X), motive (ι R x)) (mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)) (add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)) (a : FreeAlgebra R X) : motive 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 multiplication, then it holds for all of FreeAlgebra R X.

@[simp]

theorem FreeAlgebra.adjoin_range_ι (R : Type u_1) [CommSemiring R] (X : Type u_2) : Algebra.adjoin R (Set.range (ι R)) = ⊤

theorem Algebra.adjoin_range_eq_range_freeAlgebra_lift (R : Type u_1) [CommSemiring R] (X : Type u_2) {A : Type u_3} [Semiring A] [Algebra R A] (f : X → A) : adjoin R (Set.range f) = ((FreeAlgebra.lift R) f).range

Noncommutative version of Algebra.adjoin_range_eq_range_aeval.

theorem Algebra.adjoin_eq_range_freeAlgebra_lift (R : Type u_1) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] (s : Set A) : adjoin R s = ((FreeAlgebra.lift R) Subtype.val).range

Noncommutative version of Algebra.adjoin_range_eq_range.