Tensor Algebras #
Given a commutative semiring R, and an R-module M, we construct the tensor algebra of M.
This is the free R-algebra generated (R-linearly) by the module M.
Notation #
tensor_algebra R Mis the tensor algebra itself. It is endowed with an R-algebra structure.tensor_algebra.ι Ris the canonical R-linear mapM → tensor_algebra R M.- Given a linear map
f : M → Ato an R-algebraA,lift R fis the lift offto anR-algebra morphismtensor_algebra R M → A.
Theorems #
ι_comp_liftstates that the composition(lift R f) ∘ (ι R)is identical tof.lift_uniquestates that whenever an R-algebra morphismg : tensor_algebra R M → Ais given whose composition withι Risf, then one hasg = lift R f.hom_extis a variant oflift_uniquein the form of an extensionality theorem.lift_comp_ιis a combination ofι_comp_liftandlift_unique. It states that the lift of the composition of an algebra morphism withιis the algebra morphism itself.
Implementation details #
As noted above, the tensor algebra of M is constructed as the free R-algebra generated by M,
modulo the additional relations making the inclusion of M into an R-linear map.
inductive
tensor_algebra.rel
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
free_algebra R M → free_algebra R M → Prop
- add : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_monoid M] [_inst_3 : module R M] {a b : M}, tensor_algebra.rel R M (free_algebra.ι R (a + b)) (free_algebra.ι R a + free_algebra.ι R b)
- smul : ∀ (R : Type u_1) [_inst_1 : comm_semiring R] (M : Type u_2) [_inst_2 : add_comm_monoid M] [_inst_3 : module R M] {r : R} {a : M}, tensor_algebra.rel R M (free_algebra.ι R (r • a)) ((⇑(algebra_map R (free_algebra R M)) r) * free_algebra.ι R a)
An inductively defined relation on pre R M used to force the initial algebra structure on
the associated quotient.
@[protected, instance]
def
tensor_algebra.inhabited
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
inhabited (tensor_algebra R M)
def
tensor_algebra
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
Type (max u_1 u_2)
The tensor algebra of the module M over the commutative semiring R.
Equations
- tensor_algebra R M = ring_quot (tensor_algebra.rel R M)
@[protected, instance]
def
tensor_algebra.semiring
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
semiring (tensor_algebra R M)
@[protected, instance]
def
tensor_algebra.algebra
(R : Type u_1)
[comm_semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M] :
algebra R (tensor_algebra R M)
@[protected, instance]
def
tensor_algebra.ring
(M : Type u_2)
[add_comm_monoid M]
{S : Type u_1}
[comm_ring S]
[module S M] :
ring (tensor_algebra S M)
Equations
def
tensor_algebra.ι
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
M →ₗ[R] tensor_algebra R M
The canonical linear map M →ₗ[R] tensor_algebra R M.
Equations
- tensor_algebra.ι R = {to_fun := λ (m : M), ⇑(ring_quot.mk_alg_hom R (tensor_algebra.rel R M)) (free_algebra.ι R m), map_add' := _, map_smul' := _}
theorem
tensor_algebra.ring_quot_mk_alg_hom_free_algebra_ι_eq_ι
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(m : M) :
⇑(ring_quot.mk_alg_hom R (tensor_algebra.rel R M)) (free_algebra.ι R m) = ⇑(tensor_algebra.ι R) m
@[simp]
theorem
tensor_algebra.lift_symm_apply
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(F : tensor_algebra R M →ₐ[R] A) :
⇑((tensor_algebra.lift R).symm) F = F.to_linear_map.comp (tensor_algebra.ι R)
def
tensor_algebra.lift
(R : Type u_1)
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A] :
Given a linear map f : M → A where A is an R-algebra, lift R f is the unique lift
of f to a morphism of R-algebras tensor_algebra R M → A.
Equations
- tensor_algebra.lift R = {to_fun := ⇑(ring_quot.lift_alg_hom R) ∘ λ (f : M →ₗ[R] A), ⟨⇑(free_algebra.lift R) ⇑f, _⟩, inv_fun := λ (F : tensor_algebra R M →ₐ[R] A), F.to_linear_map.comp (tensor_algebra.ι R), left_inv := _, right_inv := _}
@[simp]
theorem
tensor_algebra.ι_comp_lift
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A) :
(⇑(tensor_algebra.lift R) f).to_linear_map.comp (tensor_algebra.ι R) = f
@[simp]
theorem
tensor_algebra.lift_ι_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A)
(x : M) :
⇑(⇑(tensor_algebra.lift R) f) (⇑(tensor_algebra.ι R) x) = ⇑f x
@[simp]
theorem
tensor_algebra.lift_unique
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A)
(g : tensor_algebra R M →ₐ[R] A) :
g.to_linear_map.comp (tensor_algebra.ι R) = f ↔ g = ⇑(tensor_algebra.lift R) f
@[simp]
theorem
tensor_algebra.lift_comp_ι
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
(g : tensor_algebra R M →ₐ[R] A) :
⇑(tensor_algebra.lift R) (g.to_linear_map.comp (tensor_algebra.ι R)) = g
@[ext]
theorem
tensor_algebra.hom_ext
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{A : Type u_3}
[semiring A]
[algebra R A]
{f g : tensor_algebra R M →ₐ[R] A}
(w : f.to_linear_map.comp (tensor_algebra.ι R) = g.to_linear_map.comp (tensor_algebra.ι R)) :
f = g
theorem
tensor_algebra.induction
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{C : tensor_algebra R M → Prop}
(h_grade0 : ∀ (r : R), C (⇑(algebra_map R (tensor_algebra R M)) r))
(h_grade1 : ∀ (x : M), C (⇑(tensor_algebra.ι R) x))
(h_mul : ∀ (a b : tensor_algebra R M), C a → C b → C (a * b))
(h_add : ∀ (a b : tensor_algebra R M), C a → C b → C (a + b))
(a : tensor_algebra R M) :
C a
If C holds for the algebra_map of r : R into tensor_algebra R M, the ι of x : M,
and is preserved under addition and muliplication, then it holds for all of tensor_algebra R M.
def
tensor_algebra.algebra_map_inv
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
tensor_algebra R M →ₐ[R] R
The left-inverse of algebra_map.
Equations
theorem
tensor_algebra.algebra_map_left_inverse
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
def
tensor_algebra.ι_inv
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
tensor_algebra R M →ₗ[R] M
The left-inverse of ι.
As an implementation detail, we implement this using triv_sq_zero_ext which has a suitable
algebra structure.
Equations
theorem
tensor_algebra.ι_left_inverse
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
def
free_algebra.to_tensor
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M] :
free_algebra R M →ₐ[R] tensor_algebra R M
The canonical image of the free_algebra in the tensor_algebra, which maps
free_algebra.ι R x to tensor_algebra.ι R x.
Equations
@[simp]
theorem
free_algebra.to_tensor_ι
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(m : M) :
⇑free_algebra.to_tensor (free_algebra.ι R m) = ⇑(tensor_algebra.ι R) m