mathlib documentation

algebra.free_algebra

Free Algebras #

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

At this stage we set the basic definitions as @[irreducible], so 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.

Of course, one still has the option to locally make these definitions semireducible if so desired, and Lean is still willing in some circumstances to do unification based on the underlying definition.

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.