Commit 2020-08-02 11:46 8c1e2da7

feat(linear_algebra/tensor_algebra): Tensor algebras (#3531) This PR constructs the tensor algebra of a module over a commutative ring. The main components are:

1. The construction of the tensor algebra: tensor_algebra R M for a module M over a commutative ring R.
2. The linear map univ R M from M to tensor_algebra R M.
3. Given a linear map ffrom Mto an R-algebra A, the lift of f to tensor_algebra R M is denoted lift R M f.
4. A theorem univ_comp_lift asserting that the composition of univ R M with lift R M fis f.
5. A theorem lift_unique asserting the uniqueness of lift R M fwith respect to property 4.