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 → FreeAlgebra.Pre R X
• ofScalar: {R : Type u_1} → {X : Type u_2} → R → FreeAlgebra.Pre R X
• add: {R : Type u_1} → {X : Type u_2} → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X
• mul: {R : Type u_1} → {X : Type u_2} → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X

instance FreeAlgebra.Pre.instInhabited (R : Type u_1) [CommSemiring R] (X : Type u_2) : Inhabited (FreeAlgebra.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 (FreeAlgebra.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 (FreeAlgebra.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 (FreeAlgebra.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 (FreeAlgebra.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 (FreeAlgebra.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 (FreeAlgebra.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 (FreeAlgebra.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) : FreeAlgebra.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) : FreeAlgebra.Pre R X → FreeAlgebra.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} [inst : CommSemiring R] {X : Type u_2} {r s : R}, FreeAlgebra.Rel R X (FreeAlgebra.Pre.ofScalar (r + s)) (FreeAlgebra.Pre.ofScalar r + FreeAlgebra.Pre.ofScalar s)
• mul_scalar: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {r s : R}, FreeAlgebra.Rel R X (FreeAlgebra.Pre.ofScalar (r * s)) (FreeAlgebra.Pre.ofScalar r * FreeAlgebra.Pre.ofScalar s)
• central_scalar: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {r : R} {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (FreeAlgebra.Pre.ofScalar r * a) (a * FreeAlgebra.Pre.ofScalar r)
• add_assoc: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b c : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a + b + c) (a + (b + c))
• add_comm: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a + b) (b + a)
• zero_add: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (0 + a) a
• mul_assoc: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b c : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a * b * c) (a * (b * c))
• one_mul: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (1 * a) a
• mul_one: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a * 1) a
• left_distrib: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b c : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a * (b + c)) (a * b + a * c)
• right_distrib: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b c : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X ((a + b) * c) (a * c + b * c)
• zero_mul: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (0 * a) 0
• mul_zero: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a * 0) 0
• add_compat_left: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b c : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X a b → FreeAlgebra.Rel R X (a + c) (b + c)
• add_compat_right: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b c : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X a b → FreeAlgebra.Rel R X (c + a) (c + b)
• mul_compat_left: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b c : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X a b → FreeAlgebra.Rel R X (a * c) (b * c)
• mul_compat_right: ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {a b c : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X a b → FreeAlgebra.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)

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

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

• FreeAlgebra.instMonoidWithZero R X = MonoidWithZero.mk ⋯ ⋯

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

Equations

• FreeAlgebra.instDistrib R X = Distrib.mk ⋯ ⋯

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

Equations

• FreeAlgebra.instAddCommMonoid R X = AddCommMonoid.mk ⋯

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

Equations

• FreeAlgebra.instSemiring R X = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

Equations

• FreeAlgebra.instRing X = Algebra.semiringToRing S

@[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.ι = FreeAlgebra.wrapped✝.1

theorem FreeAlgebra.ι_def (R : Type u_3) [CommSemiring R] {X : Type u_4} (m : X) : 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 (FreeAlgebra.Rel R X) (FreeAlgebra.Pre.of m) = FreeAlgebra.ι 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 = (FreeAlgebra.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) : (FreeAlgebra.lift R).symm F = ⇑F ∘ FreeAlgebra.ι 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) : ⇑((FreeAlgebra.lift R) f) ∘ FreeAlgebra.ι 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) : ((FreeAlgebra.lift R) f) (FreeAlgebra.ι 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 ∘ FreeAlgebra.ι R = f ↔ g = (FreeAlgebra.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) : (FreeAlgebra.lift R) (⇑g ∘ FreeAlgebra.ι 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 : FreeAlgebra R X →ₐ[R] A} {g : FreeAlgebra R X →ₐ[R] A} (w : ⇑f ∘ FreeAlgebra.ι R = ⇑g ∘ FreeAlgebra.ι R) : f = g

See note [partially-applied ext lemmas].

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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 ⇑FreeAlgebra.algebraMapInv ⇑(algebraMap R (FreeAlgebra R X))

@[simp]

theorem FreeAlgebra.algebraMap_inj {R : Type u_1} [CommSemiring R] {X : Type u_2} (x : R) (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 (FreeAlgebra.ι R)

@[simp]

theorem FreeAlgebra.ι_inj {R : Type u_1} [CommSemiring R] {X : Type u_2} [Nontrivial R] (x : X) (y : X) : FreeAlgebra.ι R x = FreeAlgebra.ι 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) : FreeAlgebra.ι 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) : FreeAlgebra.ι R x ≠ 0

@[simp]

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

theorem FreeAlgebra.induction (R : Type u_1) [CommSemiring R] (X : Type u_2) {C : FreeAlgebra R X → Prop} (h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)) (h_grade1 : ∀ (x : X), C (FreeAlgebra.ι R x)) (h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)) (h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)) (a : FreeAlgebra R X) : 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 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 (FreeAlgebra.ι 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) : Algebra.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) : Algebra.adjoin R s = ((FreeAlgebra.lift R) Subtype.val).range

Noncommutative version of Algebra.adjoin_range_eq_range.