mathlib3 documentation

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.
source
inductive free_algebra.pre (R : Type u_1) [comm_semiring R] (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
source
@[protected, instance]
def free_algebra.pre.inhabited (R : Type u_1) [comm_semiring R] (X : Type u_2) :
inhabited (free_algebra.pre R X)
Equations
source
def free_algebra.pre.has_coe_generator (R : Type u_1) [comm_semiring R] (X : Type u_2) :
has_coe X (free_algebra.pre R X)

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

Equations
source
def free_algebra.pre.has_coe_semiring (R : Type u_1) [comm_semiring R] (X : Type u_2) :
has_coe R (free_algebra.pre R X)

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

Equations
source
def free_algebra.pre.has_mul (R : Type u_1) [comm_semiring R] (X : Type u_2) :
has_mul (free_algebra.pre R X)

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

Equations
source
def free_algebra.pre.has_add (R : Type u_1) [comm_semiring R] (X : Type u_2) :
has_add (free_algebra.pre R X)

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

Equations
source
def free_algebra.pre.has_zero (R : Type u_1) [comm_semiring R] (X : Type u_2) :
has_zero (free_algebra.pre R X)

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

Equations
source
def free_algebra.pre.has_one (R : Type u_1) [comm_semiring R] (X : Type u_2) :
has_one (free_algebra.pre R X)

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

Equations
source
def free_algebra.pre.has_smul (R : Type u_1) [comm_semiring R] (X : Type u_2) :
has_smul R (free_algebra.pre R X)

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

Equations
source
def free_algebra.lift_fun (R : Type u_1) [comm_semiring R] (X : Type u_2) {A : Type u_3} [semiring A] [algebra R A] (f : X → A) :
free_algebra.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 free_algebra.lift.

Equations
source
inductive free_algebra.rel (R : Type u_1) [comm_semiring R] (X : Type u_2) :
free_algebra.pre R X → free_algebra.pre R X → Prop

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

source
def free_algebra (R : Type u_1) [comm_semiring R] (X : Type u_2) :
Type (max u_1 u_2)

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

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

The canonical function X → free_algebra R X.

Equations
source
@[simp]
theorem free_algebra.quot_mk_eq_ι (R : Type u_1) [comm_semiring R] {X : Type u_2} (m : X) :
quot.mk (free_algebra.rel R X) ↑m = free_algebra.ι R m
source
@[irreducible]
def free_algebra.lift (R : Type u_1) [comm_semiring R] {X : Type u_2} {A : Type u_3} [semiring A] [algebra R A] :
(X → A) ≃ (free_algebra 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 free_algebra R X → A.

Equations
source
@[simp]
theorem free_algebra.lift_aux_eq (R : Type u_1) [comm_semiring R] {X : Type u_2} {A : Type u_3} [semiring A] [algebra R A] (f : X → A) :
lift_aux R f = ⇑(free_algebra.lift R) f
source
@[simp]
theorem free_algebra.lift_symm_apply (R : Type u_1) [comm_semiring R] {X : Type u_2} {A : Type u_3} [semiring A] [algebra R A] (F : free_algebra R X →ₐ[R] A) :
⇑((free_algebra.lift R).symm) F = ⇑F ∘ free_algebra.ι R
source
@[simp]
theorem free_algebra.ι_comp_lift {R : Type u_1} [comm_semiring R] {X : Type u_2} {A : Type u_3} [semiring A] [algebra R A] (f : X → A) :
⇑(⇑(free_algebra.lift R) f) ∘ free_algebra.ι R = f
source
@[simp]
theorem free_algebra.lift_ι_apply {R : Type u_1} [comm_semiring R] {X : Type u_2} {A : Type u_3} [semiring A] [algebra R A] (f : X → A) (x : X) :
⇑(⇑(free_algebra.lift R) f) (free_algebra.ι R x) = f x
source
@[simp]
theorem free_algebra.lift_unique {R : Type u_1} [comm_semiring R] {X : Type u_2} {A : Type u_3} [semiring A] [algebra R A] (f : X → A) (g : free_algebra R X →ₐ[R] A) :
⇑g ∘ free_algebra.ι R = f ↔ g = ⇑(free_algebra.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.

source
@[simp]
theorem free_algebra.lift_comp_ι {R : Type u_1} [comm_semiring R] {X : Type u_2} {A : Type u_3} [semiring A] [algebra R A] (g : free_algebra R X →ₐ[R] A) :
⇑(free_algebra.lift R) (⇑g ∘ free_algebra.ι R) = g
source
@[ext]
theorem free_algebra.hom_ext {R : Type u_1} [comm_semiring R] {X : Type u_2} {A : Type u_3} [semiring A] [algebra R A] {f g : free_algebra R X →ₐ[R] A} (w : ⇑f ∘ free_algebra.ι R = ⇑g ∘ free_algebra.ι R) :
f = g

See note [partially-applied ext lemmas].

source
noncomputable def free_algebra.equiv_monoid_algebra_free_monoid {R : Type u_1} [comm_semiring R] {X : Type u_2} :
free_algebra R X ≃ₐ[R] monoid_algebra R (free_monoid 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
source
@[protected, instance]
def free_algebra.nontrivial {R : Type u_1} [comm_semiring R] {X : Type u_2} [nontrivial R] :
nontrivial (free_algebra R X)
source
def free_algebra.algebra_map_inv {R : Type u_1} [comm_semiring R] {X : Type u_2} :
free_algebra R X →ₐ[R] R

The left-inverse of algebra_map.

Equations
source
theorem free_algebra.algebra_map_left_inverse {R : Type u_1} [comm_semiring R] {X : Type u_2} :
function.left_inverse ⇑free_algebra.algebra_map_inv ⇑(algebra_map R (free_algebra R X))
source
@[simp]
theorem free_algebra.algebra_map_inj {R : Type u_1} [comm_semiring R] {X : Type u_2} (x y : R) :
⇑(algebra_map R (free_algebra R X)) x = ⇑(algebra_map R (free_algebra R X)) y ↔ x = y
source
@[simp]
theorem free_algebra.algebra_map_eq_zero_iff {R : Type u_1} [comm_semiring R] {X : Type u_2} (x : R) :
⇑(algebra_map R (free_algebra R X)) x = 0 ↔ x = 0
source
@[simp]
theorem free_algebra.algebra_map_eq_one_iff {R : Type u_1} [comm_semiring R] {X : Type u_2} (x : R) :
⇑(algebra_map R (free_algebra R X)) x = 1 ↔ x = 1
source
theorem free_algebra.ι_injective {R : Type u_1} [comm_semiring R] {X : Type u_2} [nontrivial R] :
function.injective (free_algebra.ι R)
source
@[simp]
theorem free_algebra.ι_inj {R : Type u_1} [comm_semiring R] {X : Type u_2} [nontrivial R] (x y : X) :
free_algebra.ι R x = free_algebra.ι R y ↔ x = y
source
@[simp]
theorem free_algebra.ι_ne_algebra_map {R : Type u_1} [comm_semiring R] {X : Type u_2} [nontrivial R] (x : X) (r : R) :
free_algebra.ι R x ≠ ⇑(algebra_map R (free_algebra R X)) r
source
@[simp]
theorem free_algebra.ι_ne_zero {R : Type u_1} [comm_semiring R] {X : Type u_2} [nontrivial R] (x : X) :
free_algebra.ι R x ≠ 0
source
@[simp]
theorem free_algebra.ι_ne_one {R : Type u_1} [comm_semiring R] {X : Type u_2} [nontrivial R] (x : X) :
free_algebra.ι R x ≠ 1
source
theorem free_algebra.induction (R : Type u_1) [comm_semiring R] (X : Type u_2) {C : free_algebra R X → Prop} (h_grade0 : ∀ (r : R), C (⇑(algebra_map R (free_algebra R X)) r)) (h_grade1 : ∀ (x : X), C (free_algebra.ι R x)) (h_mul : ∀ (a b : free_algebra R X), C a → C b → C (a * b)) (h_add : ∀ (a b : free_algebra R X), C a → C b → C (a + b)) (a : free_algebra R 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.